| Back: | ⟨a, b | aababaa=a⟩ |
|---|
Completion settings:
Axiom: aababaa=a.
Referenced by [3].
Axiom: aa=c.
Defines rule #1.
Referenced by [3], [4], [6], [9], [10], [11], [12].
Overlap of [1] aababaa=a with [2] aa=c:
Critical pair: cbabaa=a.
Reduce LHS:
| [2] | cbab(aa) |
| ⇒ cbabc |
Defines rule #8.
Referenced by [5], [6], [7], [9], [10].
Overlap of [2] aa=c with [2] aa=c:
Critical pair: ac=ca.
Flip LHS and RHS.
Defines rule #2.
Referenced by [6], [7], [10], [11].
Overlap of [3] cbabc=a with [3] cbabc=a:
Critical pair: cbaba=ababc.
Defines rule #7.
Overlap of [3] cbabc=a with [4] ca=ac:
Critical pair: cbabac=aa.
Reduce LHS:
| [5] | (cbaba)c |
| ⇒ ababcc |
Reduce RHS:
| [2] | (aa) |
| ⇒ c |
Referenced by [7].
Overlap of [6] ababcc=c with [3] cbabc=a:
Critical pair: ababca=cbabc.
Reduce LHS:
| [4] | abab(ca) |
| ⇒ ababac |
Reduce RHS:
| [3] | (cbabc) |
| ⇒ a |
Referenced by [8].
Overlap of [5] cbaba=ababc with [7] ababac=a:
Critical pair: cba=ababcbac.
Flip LHS and RHS.
Overlap of [2] aa=c with [8] ababcbac=cba:
Critical pair: acba=cbabcbac.
Reduce RHS:
| [3] | (cbabc)bac |
| ⇒ abac |
Flip LHS and RHS.
Defines rule #3.
Referenced by [11].
Overlap of [4] ca=ac with [8] ababcbac=cba:
Critical pair: ccba=acbabcbac.
Reduce RHS:
| [3] | a(cbabc)bac |
| [2] | ⇒ (aa)bac |
| ⇒ cbac |
Flip LHS and RHS.
Defines rule #5.
Overlap of [9] abac=acba with [4] ca=ac:
Critical pair: abaac=acbaa.
Reduce LHS:
| [2] | ab(aa)c |
| ⇒ abcc |
Reduce RHS:
| [2] | acb(aa) |
| ⇒ acbc |
Defines rule #4.
Referenced by [12].
Overlap of [2] aa=c with [11] abcc=acbc:
Critical pair: aacbc=cbcc.
Reduce LHS:
| [2] | (aa)cbc |
| ⇒ ccbc |
Flip LHS and RHS.
Defines rule #6.