| Back: | ⟨a, b | aabb=ba, baba=1⟩ |
|---|
Completion settings:
Axiom: aabb=ba.
Defines rule #1.
Referenced by [3], [4], [6], [10], [11], [12].
Axiom: baba=1.
Defines rule #5.
Referenced by [3], [4], [5], [6], [7], [9].
Overlap of [1] aabb=ba with [2] baba=1:
Critical pair: aab=baaba.
Flip LHS and RHS.
Overlap of [2] baba=1 with [1] aabb=ba:
Critical pair: babba=abb.
Defines rule #9.
Overlap of [2] baba=1 with [3] baaba=aab:
Critical pair: baaab=aba.
Overlap of [5] baaab=aba with [1] aabb=ba:
Critical pair: baba=abab.
Reduce LHS:
| [2] | (baba) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #2.
Referenced by [8].
Overlap of [5] baaab=aba with [2] baba=1:
Critical pair: baaa=abaaba.
Reduce RHS:
| [3] | a(baaba) |
| ⇒ aaab |
Defines rule #3.
Overlap of [5] baaab=aba with [6] abab=1:
Critical pair: baa=abaab.
Flip LHS and RHS.
Overlap of [2] baba=1 with [8] abaab=baa:
Critical pair: bbaa=ab.
Defines rule #6.
Referenced by [11].
Overlap of [8] abaab=baa with [1] aabb=ba:
Critical pair: abba=baab.
Flip LHS and RHS.
Defines rule #4.
Referenced by [12].
Overlap of [9] bbaa=ab with [1] aabb=ba:
Critical pair: bbba=abbb.
Defines rule #7.
Overlap of [10] baab=abba with [1] aabb=ba:
Critical pair: bba=abbab.
Flip LHS and RHS.
Defines rule #8.