| Back: | ⟨a, b | aaaababba=ba⟩ |
|---|
Completion settings:
Axiom: aaaababba=ba.
Referenced by [3], [4], [5], [10].
Axiom: bbba=c.
Referenced by [3], [4], [5], [6], [11].
Overlap of [1] aaaababba=ba with [1] aaaababba=ba:
Critical pair: aaaababbba=baaaababba.
Reduce LHS:
| [2] | aaaaba(bbba) |
| ⇒ aaaabac |
Reduce RHS:
| [1] | b(aaaababba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [9], [10], [11].
Overlap of [2] bbba=c with [1] aaaababba=ba:
Critical pair: bbbba=caaababba.
Reduce LHS:
| [2] | b(bbba) |
| ⇒ bc |
Reduce RHS:
| [3] | caaaba(bba) |
| ⇒ caaabaaaaabac |
Flip LHS and RHS.
Defines rule #8.
Overlap of [3] bba=aaaabac with [1] aaaababba=ba:
Critical pair: bbba=aaaabacaaababba.
Reduce LHS:
| [2] | (bbba) |
| ⇒ c |
Reduce RHS:
| [3] | aaaabacaaaba(bba) |
| [4] | ⇒ aaaaba(caaabaaaaabac) |
| ⇒ aaaababc |
Flip LHS and RHS.
Defines rule #4.
Overlap of [2] bbba=c with [5] aaaababc=c:
Critical pair: bbbc=caaababc.
Referenced by [9].
Overlap of [4] caaabaaaaabac=bc with [4] caaabaaaaabac=bc:
Critical pair: caaabaaaaababc=bcaaabaaaaabac.
Reduce LHS:
| [5] | caaaba(aaaababc) |
| ⇒ caaabac |
Reduce RHS:
| [4] | b(caaabaaaaabac) |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [8].
Overlap of [5] aaaababc=c with [4] caaabaaaaabac=bc:
Critical pair: aaaababbc=caaabaaaaabac.
Reduce LHS:
| [7] | aaaaba(bbc) |
| ⇒ aaaabacaaabac |
Reduce RHS:
| [4] | (caaabaaaaabac) |
| ⇒ bc |
Defines rule #6.
Referenced by [9].
Overlap of [3] bba=aaaabac with [8] aaaabacaaabac=bc:
Critical pair: bbbc=aaaabacaaabacaaabac.
Reduce LHS:
| [6] | (bbbc) |
| ⇒ caaababc |
Reduce RHS:
| [8] | (aaaabacaaabac)aaabac |
| ⇒ bcaaabac |
Defines rule #7.
Overlap of [1] aaaababba=ba with [3] bba=aaaabac:
Critical pair: aaaabaaaaabac=ba.
Defines rule #5.
Overlap of [2] bbba=c with [3] bba=aaaabac:
Critical pair: baaaabac=c.
Defines rule #3.