| Back: | ⟨a, b | aabaaabba=ba⟩ |
|---|
Completion settings:
Axiom: aabaaabba=ba.
Referenced by [3], [4], [5], [10].
Axiom: bbba=c.
Referenced by [3], [4], [5], [6], [11].
Overlap of [1] aabaaabba=ba with [1] aabaaabba=ba:
Critical pair: aabaaabbba=baabaaabba.
Reduce LHS:
| [2] | aabaaa(bbba) |
| ⇒ aabaaac |
Reduce RHS:
| [1] | b(aabaaabba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [9], [10], [11].
Overlap of [2] bbba=c with [1] aabaaabba=ba:
Critical pair: bbbba=cabaaabba.
Reduce LHS:
| [2] | b(bbba) |
| ⇒ bc |
Reduce RHS:
| [3] | cabaaa(bba) |
| ⇒ cabaaaaabaaac |
Flip LHS and RHS.
Defines rule #8.
Overlap of [3] bba=aabaaac with [1] aabaaabba=ba:
Critical pair: bbba=aabaaacabaaabba.
Reduce LHS:
| [2] | (bbba) |
| ⇒ c |
Reduce RHS:
| [3] | aabaaacabaaa(bba) |
| [4] | ⇒ aabaaa(cabaaaaabaaac) |
| ⇒ aabaaabc |
Flip LHS and RHS.
Defines rule #4.
Overlap of [2] bbba=c with [5] aabaaabc=c:
Critical pair: bbbc=cabaaabc.
Referenced by [9].
Overlap of [4] cabaaaaabaaac=bc with [4] cabaaaaabaaac=bc:
Critical pair: cabaaaaabaaabc=bcabaaaaabaaac.
Reduce LHS:
| [5] | cabaaa(aabaaabc) |
| ⇒ cabaaac |
Reduce RHS:
| [4] | b(cabaaaaabaaac) |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [8].
Overlap of [5] aabaaabc=c with [4] cabaaaaabaaac=bc:
Critical pair: aabaaabbc=cabaaaaabaaac.
Reduce LHS:
| [7] | aabaaa(bbc) |
| ⇒ aabaaacabaaac |
Reduce RHS:
| [4] | (cabaaaaabaaac) |
| ⇒ bc |
Defines rule #6.
Referenced by [9].
Overlap of [3] bba=aabaaac with [8] aabaaacabaaac=bc:
Critical pair: bbbc=aabaaacabaaacabaaac.
Reduce LHS:
| [6] | (bbbc) |
| ⇒ cabaaabc |
Reduce RHS:
| [8] | (aabaaacabaaac)abaaac |
| ⇒ bcabaaac |
Defines rule #7.
Overlap of [1] aabaaabba=ba with [3] bba=aabaaac:
Critical pair: aabaaaaabaaac=ba.
Defines rule #5.
Overlap of [2] bbba=c with [3] bba=aabaaac:
Critical pair: baabaaac=c.
Defines rule #3.