| Back: | ⟨a, b | aaabaa=baaba⟩ |
|---|
Completion settings:
Axiom: aaabaa=baaba.
Referenced by [3].
Axiom: aaba=c.
Defines rule #2.
Referenced by [3], [4], [6], [7], [8], [10].
Simplify [1] aaabaa=baaba.
Reduce RHS:
| [2] | b(aaba) |
| ⇒ bc |
Referenced by [4].
Overlap of [3] aaabaa=bc with [2] aaba=c:
Critical pair: aca=bc.
Defines rule #1.
Referenced by [5], [7], [8], [9], [11].
Overlap of [4] aca=bc with [4] aca=bc:
Critical pair: acbc=bcca.
Defines rule #4.
Overlap of [2] aaba=c with [2] aaba=c:
Critical pair: aabc=caba.
Defines rule #3.
Referenced by [9], [10], [12].
Overlap of [2] aaba=c with [4] aca=bc:
Critical pair: aabbc=cca.
Defines rule #6.
Referenced by [13].
Overlap of [4] aca=bc with [2] aaba=c:
Critical pair: acc=bcaba.
Flip LHS and RHS.
Defines rule #5.
Referenced by [10], [11], [12], [13], [14].
Overlap of [4] aca=bc with [6] aabc=caba:
Critical pair: accaba=bcabc.
Defines rule #8.
Overlap of [6] aabc=caba with [8] bcaba=acc:
Critical pair: aaacc=cabaaba.
Reduce RHS:
| [2] | cab(aaba) |
| ⇒ cabc |
Defines rule #7.
Referenced by [14].
Overlap of [8] bcaba=acc with [4] aca=bc:
Critical pair: bcabbc=accca.
Defines rule #9.
Overlap of [8] bcaba=acc with [6] aabc=caba:
Critical pair: bcabcaba=accabc.
Reduce LHS:
| [8] | bca(bcaba) |
| ⇒ bcaacc |
Defines rule #10.
Overlap of [8] bcaba=acc with [7] aabbc=cca:
Critical pair: bcabcca=accabbc.
Flip LHS and RHS.
Defines rule #11.
Overlap of [8] bcaba=acc with [10] aaacc=cabc:
Critical pair: bcabcabc=accaacc.
Defines rule #12.