| Back: | ⟨a, b | aba=bb, babb=ab⟩ |
|---|
Completion settings:
Axiom: aba=bb.
Referenced by [3], [4], [5], [8], [11].
Axiom: babb=ab.
Referenced by [4], [7], [9], [10].
Overlap of [1] aba=bb with [1] aba=bb:
Critical pair: abbb=bbba.
Referenced by [6].
Overlap of [1] aba=bb with [2] babb=ab:
Critical pair: aab=bbbb.
Overlap of [4] aab=bbbb with [1] aba=bb:
Critical pair: abb=bbbba.
Simplify [3] abbb=bbba.
Reduce LHS:
| [5] | (abb)b |
| ⇒ bbbbab |
Referenced by [7], [8], [9], [10].
Overlap of [2] babb=ab with [6] bbbbab=bbba:
Critical pair: babbba=abbbab.
Reduce LHS:
| [2] | (babb)ba |
| [5] | ⇒ (abb)a |
| ⇒ bbbbaa |
Reduce RHS:
| [5] | (abb)bab |
| [6] | ⇒ (bbbbab)ab |
| [4] | ⇒ bbb(aab) |
| ⇒ bbbbbbb |
Referenced by [11].
Overlap of [6] bbbbab=bbba with [1] aba=bb:
Critical pair: bbbbbb=bbbaa.
Flip LHS and RHS.
Overlap of [5] abb=bbbba with [8] bbbaa=bbbbbb:
Critical pair: abbbbbb=bbbbabaa.
Reduce LHS:
| [5] | (abb)bbbb |
| [6] | ⇒ (bbbbab)bbb |
| [2] | ⇒ bb(babb)b |
| [2] | ⇒ b(babb) |
| ⇒ bab |
Reduce RHS:
| [6] | (bbbbab)aa |
| [8] | ⇒ (bbbaa)a |
| ⇒ bbbbbba |
Referenced by [10].
Overlap of [2] babb=ab with [9] bab=bbbbbba:
Critical pair: bbbbbbab=ab.
Reduce LHS:
| [6] | bb(bbbbab) |
| ⇒ bbbbba |
Flip LHS and RHS.
Defines rule #2.
Referenced by [11].
Overlap of [1] aba=bb with [10] ab=bbbbba:
Critical pair: bbbbbaa=bb.
Reduce LHS:
| [7] | b(bbbbaa) |
| ⇒ bbbbbbbb |
Defines rule #1.
Referenced by [12].
Overlap of [11] bbbbbbbb=bb with [8] bbbaa=bbbbbb:
Critical pair: bbbbbbbbbbb=bbaa.
Reduce LHS:
| [11] | (bbbbbbbb)bbb |
| ⇒ bbbbb |
Flip LHS and RHS.
Defines rule #3.