| Back: | ⟨a, b | aab=b, ababaa=b⟩ |
|---|
Completion settings:
Axiom: aab=b.
Defines rule #2.
Referenced by [3], [4], [5], [7], [12].
Axiom: ababaa=b.
Overlap of [1] aab=b with [2] ababaa=b:
Critical pair: ab=babaa.
Flip LHS and RHS.
Referenced by [7], [8], [10], [11].
Overlap of [2] ababaa=b with [1] aab=b:
Critical pair: ababb=bb.
Overlap of [1] aab=b with [4] ababb=bb:
Critical pair: abb=babb.
Flip LHS and RHS.
Referenced by [6].
Overlap of [5] babb=abb with [5] babb=abb:
Critical pair: bababb=abbabb.
Reduce LHS:
| [4] | b(ababb) |
| ⇒ bbb |
Reduce RHS:
| [5] | ab(babb) |
| [4] | ⇒ (ababb) |
| ⇒ bb |
Overlap of [3] babaa=ab with [1] aab=b:
Critical pair: babab=abab.
Referenced by [9].
Overlap of [6] bbb=bb with [3] babaa=ab:
Critical pair: bbab=bbabaa.
Reduce RHS:
| [3] | b(babaa) |
| ⇒ bab |
Overlap of [8] bbab=bab with [2] ababaa=b:
Critical pair: bbb=bababaa.
Reduce LHS:
| [6] | (bbb) |
| ⇒ bb |
Reduce RHS:
| [7] | (babab)aa |
| [2] | ⇒ (ababaa) |
| ⇒ b |
Defines rule #1.
Referenced by [11].
Overlap of [8] bbab=bab with [3] babaa=ab:
Critical pair: bab=babaa.
Reduce RHS:
| [3] | (babaa) |
| ⇒ ab |
Defines rule #4.
Referenced by [11].
Overlap of [9] bb=b with [3] babaa=ab:
Critical pair: bab=babaa.
Reduce LHS:
| [10] | (bab) |
| ⇒ ab |
Reduce RHS:
| [10] | (bab)aa |
| ⇒ abaa |
Flip LHS and RHS.
Referenced by [12].
Overlap of [1] aab=b with [11] abaa=ab:
Critical pair: aab=baa.
Reduce LHS:
| [1] | (aab) |
| ⇒ b |
Flip LHS and RHS.
Defines rule #3.