| Back: | ⟨a, b | aaa=bb, aaba=b⟩ |
|---|
Completion settings:
Axiom: aaa=bb.
Defines rule #2.
Referenced by [3], [4], [5], [8], [12], [13].
Axiom: aaba=b.
Referenced by [4], [5], [6], [8], [12], [13].
Overlap of [1] aaa=bb with [1] aaa=bb:
Critical pair: abb=bba.
Flip LHS and RHS.
Referenced by [4], [7], [8], [11], [12].
Overlap of [1] aaa=bb with [2] aaba=b:
Critical pair: ab=bbba.
Reduce RHS:
| [3] | b(bba) |
| ⇒ babb |
Flip LHS and RHS.
Overlap of [2] aaba=b with [1] aaa=bb:
Critical pair: aabbb=baa.
Overlap of [2] aaba=b with [2] aaba=b:
Critical pair: aabb=baba.
Flip LHS and RHS.
Referenced by [7].
Overlap of [4] babb=ab with [3] bba=abb:
Critical pair: bababb=abba.
Reduce LHS:
| [6] | (baba)bb |
| [5] | ⇒ (aabbb)b |
| ⇒ baab |
Reduce RHS:
| [3] | a(bba) |
| ⇒ aabb |
Referenced by [8].
Overlap of [7] baab=aabb with [2] aaba=b:
Critical pair: bb=aabba.
Reduce RHS:
| [3] | aa(bba) |
| [1] | ⇒ (aaa)bb |
| ⇒ bbbb |
Flip LHS and RHS.
Referenced by [9].
Overlap of [4] babb=ab with [8] bbbb=bb:
Critical pair: babb=abbb.
Reduce LHS:
| [4] | (babb) |
| ⇒ ab |
Flip LHS and RHS.
Referenced by [10], [11], [12].
Overlap of [4] babb=ab with [9] abbb=ab:
Critical pair: bab=abb.
Overlap of [9] abbb=ab with [3] bba=abb:
Critical pair: ababb=aba.
Reduce LHS:
| [10] | a(bab)b |
| [5] | ⇒ (aabbb) |
| ⇒ baa |
Overlap of [2] aaba=b with [11] baa=aba:
Critical pair: aaaba=ba.
Reduce LHS:
| [1] | (aaa)ba |
| [3] | ⇒ b(bba) |
| [10] | ⇒ (bab)b |
| [9] | ⇒ (abbb) |
| ⇒ ab |
Flip LHS and RHS.
Defines rule #1.
Referenced by [13].
Overlap of [11] baa=aba with [1] aaa=bb:
Critical pair: bbb=abaa.
Reduce RHS:
| [12] | a(ba)a |
| [2] | ⇒ (aaba) |
| ⇒ b |
Defines rule #3.