| Back: | ⟨a, b | aaab=b, babb=a⟩ |
|---|
Completion settings:
Axiom: aaab=b.
Referenced by [4], [5], [6], [9], [16].
Axiom: babb=a.
Referenced by [3], [4], [6], [7], [9], [13], [14].
Overlap of [2] babb=a with [2] babb=a:
Critical pair: baba=aabb.
Flip LHS and RHS.
Referenced by [5], [10], [11], [12].
Overlap of [1] aaab=b with [2] babb=a:
Critical pair: aaaa=babb.
Reduce RHS:
| [2] | (babb) |
| ⇒ a |
Overlap of [1] aaab=b with [3] aabb=baba:
Critical pair: ababa=bb.
Overlap of [5] ababa=bb with [1] aaab=b:
Critical pair: ababb=bbaab.
Reduce LHS:
| [2] | a(babb) |
| ⇒ aa |
Flip LHS and RHS.
Referenced by [9], [10], [11], [15].
Overlap of [5] ababa=bb with [2] babb=a:
Critical pair: abaa=bbbb.
Overlap of [5] ababa=bb with [5] ababa=bb:
Critical pair: abbb=bbba.
Referenced by [13].
Overlap of [2] babb=a with [6] bbaab=aa:
Critical pair: baaa=aaab.
Reduce RHS:
| [1] | (aaab) |
| ⇒ b |
Overlap of [3] aabb=baba with [6] bbaab=aa:
Critical pair: aaaa=babaaab.
Reduce LHS:
| [4] | (aaaa) |
| ⇒ a |
Reduce RHS:
| [7] | b(abaa)ab |
| ⇒ bbbbbab |
Flip LHS and RHS.
Overlap of [6] bbaab=aa with [3] aabb=baba:
Critical pair: bbbaba=aab.
Flip LHS and RHS.
Referenced by [12].
Overlap of [3] aabb=baba with [9] baaa=b:
Critical pair: aabb=babaaaa.
Reduce LHS:
| [11] | (aab)b |
| ⇒ bbbabab |
Reduce RHS:
| [7] | b(abaa)aa |
| ⇒ bbbbbaa |
Referenced by [13].
Overlap of [2] babb=a with [10] bbbbbab=a:
Critical pair: baba=abbbbab.
Reduce RHS:
| [8] | (abbb)bab |
| [12] | ⇒ (bbbabab) |
| ⇒ bbbbbaa |
Referenced by [15].
Overlap of [10] bbbbbab=a with [2] babb=a:
Critical pair: bbbba=ab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [15].
Overlap of [14] ab=bbbba with [6] bbaab=aa:
Critical pair: aaa=bbbbabaab.
Reduce RHS:
| [13] | bbb(baba)ab |
| [9] | ⇒ bbbbbbb(baaa)b |
| ⇒ bbbbbbbbb |
Defines rule #4.
Overlap of [1] aaab=b with [15] aaa=bbbbbbbbb:
Critical pair: bbbbbbbbbb=b.
Defines rule #1.
Overlap of [4] aaaa=a with [15] aaa=bbbbbbbbb:
Critical pair: bbbbbbbbba=a.
Defines rule #2.