| Back: | ⟨a, b | ababaabba=1⟩ |
|---|
Completion settings:
Axiom: ababaabba=1.
Referenced by [3].
Axiom: baab=c.
Defines rule #5.
Referenced by [3], [4], [5], [6], [7].
Overlap of [1] ababaabba=1 with [2] baab=c:
Critical pair: abacba=1.
Referenced by [5], [6], [8], [9], [10].
Overlap of [2] baab=c with [2] baab=c:
Critical pair: baac=caab.
Referenced by [14].
Overlap of [2] baab=c with [3] abacba=1:
Critical pair: ba=cacba.
Flip LHS and RHS.
Referenced by [7].
Overlap of [3] abacba=1 with [2] baab=c:
Critical pair: abacc=ab.
Referenced by [8].
Overlap of [5] cacba=ba with [2] baab=c:
Critical pair: cacc=baab.
Reduce RHS:
| [2] | (baab) |
| ⇒ c |
Referenced by [11].
Overlap of [3] abacba=1 with [6] abacc=ab:
Critical pair: abacbab=bacc.
Reduce LHS:
| [3] | (abacba)b |
| ⇒ b |
Flip LHS and RHS.
Overlap of [3] abacba=1 with [8] bacc=b:
Critical pair: abacb=cc.
Referenced by [10].
Overlap of [3] abacba=1 with [9] abacb=cc:
Critical pair: cca=1.
Defines rule #2.
Referenced by [11], [12], [15], [16], [17], [18].
Overlap of [7] cacc=c with [10] cca=1:
Critical pair: cac=cca.
Reduce RHS:
| [10] | (cca) |
| ⇒ 1 |
Referenced by [13].
Overlap of [8] bacc=b with [10] cca=1:
Critical pair: bac=bca.
Referenced by [14].
Overlap of [11] cac=1 with [11] cac=1:
Critical pair: ca=ac.
Flip LHS and RHS.
Defines rule #1.
Referenced by [14], [15], [17].
Overlap of [4] baac=caab with [13] ac=ca:
Critical pair: baca=caab.
Reduce LHS:
| [12] | (bac)a |
| ⇒ bcaa |
Overlap of [14] bcaa=caab with [13] ac=ca:
Critical pair: bcaca=caabc.
Reduce LHS:
| [13] | bc(ac)a |
| [10] | ⇒ b(cca)a |
| ⇒ ba |
Flip LHS and RHS.
Overlap of [10] cca=1 with [15] caabc=ba:
Critical pair: cba=abc.
Flip LHS and RHS.
Referenced by [18].
Overlap of [15] caabc=ba with [14] bcaa=caab:
Critical pair: caacaab=baaa.
Reduce LHS:
| [13] | ca(ac)aab |
| [13] | ⇒ c(ac)aaab |
| [10] | ⇒ (cca)aaab |
| ⇒ aaab |
Flip LHS and RHS.
Defines rule #4.
Overlap of [10] cca=1 with [16] abc=cba:
Critical pair: cccba=bc.
Flip LHS and RHS.
Defines rule #3.