| Back: | ⟨a, b | abaaaabba=ba⟩ |
|---|
Completion settings:
Axiom: abaaaabba=ba.
Referenced by [3], [4], [5], [10].
Axiom: bbba=c.
Referenced by [3], [4], [5], [6], [11].
Overlap of [1] abaaaabba=ba with [1] abaaaabba=ba:
Critical pair: abaaaabbba=babaaaabba.
Reduce LHS:
| [2] | abaaaa(bbba) |
| ⇒ abaaaac |
Reduce RHS:
| [1] | b(abaaaabba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [9], [10], [11].
Overlap of [2] bbba=c with [1] abaaaabba=ba:
Critical pair: bbbba=cbaaaabba.
Reduce LHS:
| [2] | b(bbba) |
| ⇒ bc |
Reduce RHS:
| [3] | cbaaaa(bba) |
| ⇒ cbaaaaabaaaac |
Flip LHS and RHS.
Defines rule #8.
Overlap of [3] bba=abaaaac with [1] abaaaabba=ba:
Critical pair: bbba=abaaaacbaaaabba.
Reduce LHS:
| [2] | (bbba) |
| ⇒ c |
Reduce RHS:
| [3] | abaaaacbaaaa(bba) |
| [4] | ⇒ abaaaa(cbaaaaabaaaac) |
| ⇒ abaaaabc |
Flip LHS and RHS.
Defines rule #4.
Overlap of [2] bbba=c with [5] abaaaabc=c:
Critical pair: bbbc=cbaaaabc.
Referenced by [9].
Overlap of [4] cbaaaaabaaaac=bc with [4] cbaaaaabaaaac=bc:
Critical pair: cbaaaaabaaaabc=bcbaaaaabaaaac.
Reduce LHS:
| [5] | cbaaaa(abaaaabc) |
| ⇒ cbaaaac |
Reduce RHS:
| [4] | b(cbaaaaabaaaac) |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [8].
Overlap of [5] abaaaabc=c with [4] cbaaaaabaaaac=bc:
Critical pair: abaaaabbc=cbaaaaabaaaac.
Reduce LHS:
| [7] | abaaaa(bbc) |
| ⇒ abaaaacbaaaac |
Reduce RHS:
| [4] | (cbaaaaabaaaac) |
| ⇒ bc |
Defines rule #6.
Referenced by [9].
Overlap of [3] bba=abaaaac with [8] abaaaacbaaaac=bc:
Critical pair: bbbc=abaaaacbaaaacbaaaac.
Reduce LHS:
| [6] | (bbbc) |
| ⇒ cbaaaabc |
Reduce RHS:
| [8] | (abaaaacbaaaac)baaaac |
| ⇒ bcbaaaac |
Defines rule #7.
Overlap of [1] abaaaabba=ba with [3] bba=abaaaac:
Critical pair: abaaaaabaaaac=ba.
Defines rule #5.
Overlap of [2] bbba=c with [3] bba=abaaaac:
Critical pair: babaaaac=c.
Defines rule #3.