| Back: | ⟨a, b | aaabbba=baa⟩ |
|---|
Completion settings:
Axiom: aaabbba=baa.
Referenced by [4].
Axiom: bbb=c.
Defines rule #10.
Referenced by [4], [5], [6], [8].
Axiom: caa=d.
Defines rule #4.
Referenced by [6], [7], [8], [9], [10], [11].
Overlap of [1] aaabbba=baa with [2] bbb=c:
Critical pair: aaaca=baa.
Flip LHS and RHS.
Defines rule #7.
Overlap of [2] bbb=c with [2] bbb=c:
Critical pair: bc=cb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [7].
Overlap of [2] bbb=c with [4] baa=aaaca:
Critical pair: bbaaaca=caa.
Reduce LHS:
| [4] | b(baa)aca |
| [4] | ⇒ (baa)acaaca |
| [3] | ⇒ aaa(caa)caaca |
| [3] | ⇒ aaad(caa)ca |
| ⇒ aaaddca |
Reduce RHS:
| [3] | (caa) |
| ⇒ d |
Defines rule #2.
Referenced by [9], [10], [11].
Overlap of [5] cb=bc with [4] baa=aaaca:
Critical pair: caaaca=bcaa.
Reduce LHS:
| [3] | (caa)aca |
| ⇒ daca |
Reduce RHS:
| [3] | b(caa) |
| ⇒ bd |
Flip LHS and RHS.
Defines rule #6.
Referenced by [8].
Overlap of [2] bbb=c with [7] bd=daca:
Critical pair: bbdaca=cd.
Reduce LHS:
| [7] | b(bd)aca |
| [7] | ⇒ (bd)acaaca |
| [3] | ⇒ da(caa)caaca |
| [3] | ⇒ dad(caa)ca |
| ⇒ daddca |
Flip LHS and RHS.
Defines rule #3.
Overlap of [3] caa=d with [6] aaaddca=d:
Critical pair: cad=daaddca.
Defines rule #5.
Overlap of [4] baa=aaaca with [6] aaaddca=d:
Critical pair: bad=aaacaaaddca.
Reduce RHS:
| [3] | aaa(caa)addca |
| ⇒ aaadaddca |
Defines rule #8.
Overlap of [6] aaaddca=d with [3] caa=d:
Critical pair: aaaddd=da.
Defines rule #1.