| Back: | ⟨a, b | aaabaabba=ba⟩ |
|---|
Completion settings:
Axiom: aaabaabba=ba.
Referenced by [3], [4], [5], [10].
Axiom: bbba=c.
Referenced by [3], [4], [5], [6], [11].
Overlap of [1] aaabaabba=ba with [1] aaabaabba=ba:
Critical pair: aaabaabbba=baaabaabba.
Reduce LHS:
| [2] | aaabaa(bbba) |
| ⇒ aaabaac |
Reduce RHS:
| [1] | b(aaabaabba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [9], [10], [11].
Overlap of [2] bbba=c with [1] aaabaabba=ba:
Critical pair: bbbba=caabaabba.
Reduce LHS:
| [2] | b(bbba) |
| ⇒ bc |
Reduce RHS:
| [3] | caabaa(bba) |
| ⇒ caabaaaaabaac |
Flip LHS and RHS.
Defines rule #8.
Overlap of [3] bba=aaabaac with [1] aaabaabba=ba:
Critical pair: bbba=aaabaacaabaabba.
Reduce LHS:
| [2] | (bbba) |
| ⇒ c |
Reduce RHS:
| [3] | aaabaacaabaa(bba) |
| [4] | ⇒ aaabaa(caabaaaaabaac) |
| ⇒ aaabaabc |
Flip LHS and RHS.
Defines rule #4.
Overlap of [2] bbba=c with [5] aaabaabc=c:
Critical pair: bbbc=caabaabc.
Referenced by [9].
Overlap of [4] caabaaaaabaac=bc with [4] caabaaaaabaac=bc:
Critical pair: caabaaaaabaabc=bcaabaaaaabaac.
Reduce LHS:
| [5] | caabaa(aaabaabc) |
| ⇒ caabaac |
Reduce RHS:
| [4] | b(caabaaaaabaac) |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [8].
Overlap of [5] aaabaabc=c with [4] caabaaaaabaac=bc:
Critical pair: aaabaabbc=caabaaaaabaac.
Reduce LHS:
| [7] | aaabaa(bbc) |
| ⇒ aaabaacaabaac |
Reduce RHS:
| [4] | (caabaaaaabaac) |
| ⇒ bc |
Defines rule #6.
Referenced by [9].
Overlap of [3] bba=aaabaac with [8] aaabaacaabaac=bc:
Critical pair: bbbc=aaabaacaabaacaabaac.
Reduce LHS:
| [6] | (bbbc) |
| ⇒ caabaabc |
Reduce RHS:
| [8] | (aaabaacaabaac)aabaac |
| ⇒ bcaabaac |
Defines rule #7.
Overlap of [1] aaabaabba=ba with [3] bba=aaabaac:
Critical pair: aaabaaaaabaac=ba.
Defines rule #5.
Overlap of [2] bbba=c with [3] bba=aaabaac:
Critical pair: baaabaac=c.
Defines rule #3.