| Back: | ⟨a, b | aaabbbba=baa⟩ |
|---|
Completion settings:
Axiom: aaabbbba=baa.
Referenced by [4].
Axiom: bbbb=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] aaabbbba=baa with [2] bbbb=c:
Critical pair: aaaca=baa.
Flip LHS and RHS.
Defines rule #7.
Overlap of [2] bbbb=c with [2] bbbb=c:
Critical pair: bc=cb.
Flip LHS and RHS.
Defines rule #9.
Referenced by [7].
Overlap of [2] bbbb=c with [4] baa=aaaca:
Critical pair: bbbaaaca=caa.
Reduce LHS:
| [4] | bb(baa)aca |
| [4] | ⇒ b(baa)acaaca |
| [4] | ⇒ (baa)acaacaaca |
| [3] | ⇒ aaa(caa)caacaaca |
| [3] | ⇒ aaad(caa)caaca |
| [3] | ⇒ aaadd(caa)ca |
| ⇒ aaadddca |
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] bbbb=c with [7] bd=daca:
Critical pair: bbbdaca=cd.
Reduce LHS:
| [7] | bb(bd)aca |
| [7] | ⇒ b(bd)acaaca |
| [7] | ⇒ (bd)acaacaaca |
| [3] | ⇒ da(caa)caacaaca |
| [3] | ⇒ dad(caa)caaca |
| [3] | ⇒ dadd(caa)ca |
| ⇒ dadddca |
Flip LHS and RHS.
Defines rule #3.
Overlap of [3] caa=d with [6] aaadddca=d:
Critical pair: cad=daadddca.
Defines rule #5.
Overlap of [4] baa=aaaca with [6] aaadddca=d:
Critical pair: bad=aaacaaadddca.
Reduce RHS:
| [3] | aaa(caa)adddca |
| ⇒ aaadadddca |
Defines rule #8.
Overlap of [6] aaadddca=d with [3] caa=d:
Critical pair: aaadddd=da.
Defines rule #1.