| Back: | ⟨a, b | abaaabbba=ba⟩ |
|---|
Completion settings:
Axiom: abaaabbba=ba.
Referenced by [3], [4], [5], [13].
Axiom: bbbba=c.
Overlap of [1] abaaabbba=ba with [1] abaaabbba=ba:
Critical pair: abaaabbbba=babaaabbba.
Reduce LHS:
| [2] | abaaa(bbbba) |
| ⇒ abaaac |
Reduce RHS:
| [1] | b(abaaabbba) |
| ⇒ bba |
Flip LHS and RHS.
Defines rule #1.
Referenced by [4], [5], [6], [7], [8], [13], [14].
Overlap of [2] bbbba=c with [1] abaaabbba=ba:
Critical pair: bbbbba=cbaaabbba.
Reduce LHS:
| [2] | b(bbbba) |
| ⇒ bc |
Reduce RHS:
| [3] | cbaaab(bba) |
| ⇒ cbaaababaaac |
Flip LHS and RHS.
Defines rule #7.
Referenced by [5], [7], [8], [9], [10], [11].
Overlap of [3] bba=abaaac with [1] abaaabbba=ba:
Critical pair: bbba=abaaacbaaabbba.
Reduce LHS:
| [3] | b(bba) |
| ⇒ babaaac |
Reduce RHS:
| [3] | abaaacbaaab(bba) |
| [4] | ⇒ abaaa(cbaaababaaac) |
| ⇒ abaaabc |
Flip LHS and RHS.
Defines rule #3.
Overlap of [3] bba=abaaac with [5] abaaabc=babaaac:
Critical pair: bbbabaaac=abaaacbaaabc.
Reduce LHS:
| [3] | b(bba)baaac |
| ⇒ babaaacbaaac |
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] cbaaababaaac=bc with [4] cbaaababaaac=bc:
Critical pair: cbaaababaaabc=bcbaaababaaac.
Reduce LHS:
| [5] | cbaaab(abaaabc) |
| [3] | ⇒ cbaaa(bba)baaac |
| ⇒ cbaaaabaaacbaaac |
Reduce RHS:
| [4] | b(cbaaababaaac) |
| ⇒ bbc |
Overlap of [5] abaaabc=babaaac with [4] cbaaababaaac=bc:
Critical pair: abaaabbc=babaaacbaaababaaac.
Reduce RHS:
| [4] | babaaa(cbaaababaaac) |
| [5] | ⇒ b(abaaabc) |
| [3] | ⇒ (bba)baaac |
| ⇒ abaaacbaaac |
Referenced by [9], [10], [12].
Overlap of [8] abaaabbc=abaaacbaaac with [4] cbaaababaaac=bc:
Critical pair: abaaabbbc=abaaacbaaacbaaababaaac.
Reduce RHS:
| [4] | abaaacbaaa(cbaaababaaac) |
| [6] | ⇒ (abaaacbaaabc) |
| ⇒ babaaacbaaac |
Referenced by [12].
Overlap of [4] cbaaababaaac=bc with [7] cbaaaabaaacbaaac=bbc:
Critical pair: cbaaababaaabbc=bcbaaaabaaacbaaac.
Reduce LHS:
| [8] | cbaaab(abaaabbc) |
| [4] | ⇒ (cbaaababaaac)baaac |
| ⇒ bcbaaac |
Reduce RHS:
| [7] | b(cbaaaabaaacbaaac) |
| ⇒ bbbc |
Flip LHS and RHS.
Referenced by [11].
Overlap of [10] bbbc=bcbaaac with [4] cbaaababaaac=bc:
Critical pair: bbbbc=bcbaaacbaaababaaac.
Reduce LHS:
| [10] | b(bbbc) |
| ⇒ bbcbaaac |
Reduce RHS:
| [4] | bcbaaa(cbaaababaaac) |
| ⇒ bcbaaabc |
Flip LHS and RHS.
Referenced by [12].
Overlap of [8] abaaabbc=abaaacbaaac with [11] bcbaaabc=bbcbaaac:
Critical pair: abaaabbbcbaaac=abaaacbaaacbaaabc.
Reduce LHS:
| [9] | (abaaabbbc)baaac |
| ⇒ babaaacbaaacbaaac |
Flip LHS and RHS.
Referenced by [16].
Overlap of [1] abaaabbba=ba with [3] bba=abaaac:
Critical pair: abaaababaaac=ba.
Defines rule #6.
Overlap of [2] bbbba=c with [3] bba=abaaac:
Critical pair: bbabaaac=c.
Reduce LHS:
| [3] | (bba)baaac |
| ⇒ abaaacbaaac |
Defines rule #4.
Referenced by [15], [16], [17].
Overlap of [7] cbaaaabaaacbaaac=bbc with [14] abaaacbaaac=c:
Critical pair: cbaaac=bbc.
Flip LHS and RHS.
Defines rule #2.
Simplify [12] abaaacbaaacbaaabc=babaaacbaaacbaaac.
Reduce RHS:
| [14] | b(abaaacbaaac)baaac |
| ⇒ bcbaaac |
Referenced by [17].
Overlap of [16] abaaacbaaacbaaabc=bcbaaac with [14] abaaacbaaac=c:
Critical pair: cbaaabc=bcbaaac.
Defines rule #5.