| Back: | ⟨a, b | aa=1, abbabba=b⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #4.
Referenced by [3], [4], [6], [10].
Axiom: abbabba=b.
Overlap of [1] aa=1 with [2] abbabba=b:
Critical pair: ab=bbabba.
Flip LHS and RHS.
Referenced by [9].
Overlap of [2] abbabba=b with [1] aa=1:
Critical pair: abbabb=ba.
Overlap of [2] abbabba=b with [2] abbabba=b:
Critical pair: abbb=bbba.
Flip LHS and RHS.
Defines rule #3.
Referenced by [7], [8], [9], [11].
Overlap of [1] aa=1 with [4] abbabb=ba:
Critical pair: aba=bbabb.
Defines rule #5.
Overlap of [4] abbabb=ba with [5] bbba=abbb:
Critical pair: abbababbb=babba.
Reduce LHS:
| [6] | abb(aba)bbb |
| [5] | ⇒ ab(bbba)bbbbb |
| [6] | ⇒ (aba)bbbbbbbb |
| ⇒ bbabbbbbbbbbb |
Flip LHS and RHS.
Referenced by [9].
Overlap of [6] aba=bbabb with [4] abbabb=ba:
Critical pair: abba=bbabbbbabb.
Reduce RHS:
| [5] | bbab(bbba)bb |
| [6] | ⇒ bb(aba)bbbbb |
| [5] | ⇒ b(bbba)bbbbbbb |
| ⇒ babbbbbbbbbb |
Defines rule #6.
Simplify [3] bbabba=ab.
Reduce LHS:
| [7] | b(babba) |
| [5] | ⇒ (bbba)bbbbbbbbbb |
| ⇒ abbbbbbbbbbbbb |
Referenced by [10].
Overlap of [1] aa=1 with [9] abbbbbbbbbbbbb=ab:
Critical pair: aab=bbbbbbbbbbbbb.
Reduce LHS:
| [1] | (aa)b |
| ⇒ b |
Flip LHS and RHS.
Defines rule #1.
Referenced by [11].
Overlap of [10] bbbbbbbbbbbbb=b with [5] bbba=abbb:
Critical pair: bbbbbbbbbbabbb=ba.
Reduce LHS:
| [5] | bbbbbbb(bbba)bbb |
| [5] | ⇒ bbbb(bbba)bbbbbb |
| [5] | ⇒ b(bbba)bbbbbbbbb |
| ⇒ babbbbbbbbbbbb |
Defines rule #2.