| Back: | ⟨a, b | aaabbaaaab=a⟩ |
|---|
Completion settings:
Axiom: aaabbaaaab=a.
Referenced by [3].
Axiom: aaaab=c.
Overlap of [1] aaabbaaaab=a with [2] aaaab=c:
Critical pair: aaabbc=a.
Overlap of [2] aaaab=c with [3] aaabbc=a:
Critical pair: aa=cbc.
Defines rule #3.
Overlap of [4] aa=cbc with [4] aa=cbc:
Critical pair: acbc=cbca.
Defines rule #2.
Referenced by [8].
Overlap of [2] aaaab=c with [4] aa=cbc:
Critical pair: cbcaab=c.
Reduce LHS:
| [4] | cbc(aa)b |
| ⇒ cbccbcb |
Defines rule #4.
Referenced by [8], [9], [10], [11], [13], [15].
Overlap of [3] aaabbc=a with [4] aa=cbc:
Critical pair: cbcabbc=a.
Defines rule #9.
Referenced by [10], [11], [12], [14], [16].
Overlap of [5] acbc=cbca with [6] cbccbcb=c:
Critical pair: ac=cbcacbcb.
Reduce RHS:
| [5] | cbc(acbc)b |
| ⇒ cbccbcab |
Flip LHS and RHS.
Defines rule #8.
Referenced by [15], [16], [17].
Overlap of [6] cbccbcb=c with [6] cbccbcb=c:
Critical pair: cbccbc=cccbcb.
Flip LHS and RHS.
Defines rule #1.
Overlap of [6] cbccbcb=c with [7] cbcabbc=a:
Critical pair: cbccba=ccabbc.
Flip LHS and RHS.
Defines rule #7.
Overlap of [7] cbcabbc=a with [6] cbccbcb=c:
Critical pair: cbcabbc=abccbcb.
Reduce LHS:
| [7] | (cbcabbc) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #10.
Referenced by [13], [14], [17].
Overlap of [7] cbcabbc=a with [7] cbcabbc=a:
Critical pair: cbcabba=abcabbc.
Flip LHS and RHS.
Defines rule #14.
Overlap of [11] abccbcb=a with [6] cbccbcb=c:
Critical pair: abccbc=accbcb.
Flip LHS and RHS.
Defines rule #6.
Overlap of [11] abccbcb=a with [7] cbcabbc=a:
Critical pair: abccba=acabbc.
Flip LHS and RHS.
Defines rule #12.
Overlap of [6] cbccbcb=c with [8] cbccbcab=ac:
Critical pair: cbccbac=cccbcab.
Flip LHS and RHS.
Defines rule #5.
Overlap of [7] cbcabbc=a with [8] cbccbcab=ac:
Critical pair: cbcabbac=abccbcab.
Flip LHS and RHS.
Defines rule #13.
Overlap of [11] abccbcb=a with [8] cbccbcab=ac:
Critical pair: abccbac=accbcab.
Flip LHS and RHS.
Defines rule #11.