| Back: | ⟨a, b | ababbbbba=ba⟩ |
|---|
Completion settings:
Axiom: ababbbbba=ba.
Referenced by [3], [4], [5], [8].
Axiom: bbbbbba=c.
Overlap of [1] ababbbbba=ba with [1] ababbbbba=ba:
Critical pair: ababbbbbba=bababbbbba.
Reduce LHS:
| [2] | aba(bbbbbba) |
| ⇒ abac |
Reduce RHS:
| [1] | b(ababbbbba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [6], [7], [8], [9].
Overlap of [2] bbbbbba=c with [1] ababbbbba=ba:
Critical pair: bbbbbbba=cbabbbbba.
Reduce LHS:
| [2] | b(bbbbbba) |
| ⇒ bc |
Reduce RHS:
| [3] | cbabbb(bba) |
| [3] | ⇒ cbab(bba)bac |
| ⇒ cbababacbac |
Flip LHS and RHS.
Defines rule #7.
Overlap of [3] bba=abac with [1] ababbbbba=ba:
Critical pair: bbba=abacbabbbbba.
Reduce LHS:
| [3] | b(bba) |
| ⇒ babac |
Reduce RHS:
| [3] | abacbabbb(bba) |
| [3] | ⇒ abacbab(bba)bac |
| [4] | ⇒ aba(cbababacbac) |
| ⇒ ababc |
Flip LHS and RHS.
Defines rule #3.
Referenced by [6].
Overlap of [3] bba=abac with [5] ababc=babac:
Critical pair: bbbabac=abacbabc.
Reduce LHS:
| [3] | b(bba)bac |
| ⇒ babacbac |
Flip LHS and RHS.
Referenced by [7].
Overlap of [4] cbababacbac=bc with [4] cbababacbac=bc:
Critical pair: cbababacbabc=bcbababacbac.
Reduce LHS:
| [6] | cbab(abacbabc) |
| [3] | ⇒ cba(bba)bacbac |
| ⇒ cbaabacbacbac |
Reduce RHS:
| [4] | b(cbababacbac) |
| ⇒ bbc |
Referenced by [10].
Overlap of [1] ababbbbba=ba with [3] bba=abac:
Critical pair: ababbbabac=ba.
Reduce LHS:
| [3] | abab(bba)bac |
| ⇒ abababacbac |
Defines rule #6.
Overlap of [2] bbbbbba=c with [3] bba=abac:
Critical pair: bbbbabac=c.
Reduce LHS:
| [3] | bb(bba)bac |
| [3] | ⇒ (bba)bacbac |
| ⇒ abacbacbac |
Defines rule #5.
Referenced by [10].
Overlap of [7] cbaabacbacbac=bbc with [9] abacbacbac=c:
Critical pair: cbac=bbc.
Flip LHS and RHS.
Defines rule #2.
Referenced by [11].
Overlap of [10] bbc=cbac with [4] cbababacbac=bc:
Critical pair: bbbc=cbacbababacbac.
Reduce LHS:
| [10] | b(bbc) |
| ⇒ bcbac |
Reduce RHS:
| [4] | cba(cbababacbac) |
| ⇒ cbabc |
Flip LHS and RHS.
Defines rule #4.