| Back: | ⟨a, b | abb=aab, abaa=b⟩ |
|---|
Completion settings:
Axiom: abb=aab.
Flip LHS and RHS.
Referenced by [4], [5], [6], [13].
Axiom: abaa=b.
Referenced by [3], [4], [5], [6], [7], [12].
Overlap of [2] abaa=b with [2] abaa=b:
Critical pair: abab=bbaa.
Overlap of [1] aab=abb with [2] abaa=b:
Critical pair: ab=abbaa.
Flip LHS and RHS.
Referenced by [10].
Overlap of [2] abaa=b with [1] aab=abb:
Critical pair: ababb=bb.
Reduce LHS:
| [3] | (abab)b |
| [1] | ⇒ bb(aab) |
| ⇒ bbabb |
Referenced by [8].
Overlap of [2] abaa=b with [1] aab=abb:
Critical pair: abaabb=bab.
Reduce LHS:
| [2] | (abaa)bb |
| ⇒ bbb |
Flip LHS and RHS.
Overlap of [6] bab=bbb with [2] abaa=b:
Critical pair: bb=bbbaa.
Flip LHS and RHS.
Referenced by [9], [12], [14].
Simplify [5] bbabb=bb.
Reduce LHS:
| [6] | b(bab)b |
| ⇒ bbbbb |
Referenced by [9].
Overlap of [8] bbbbb=bb with [7] bbbaa=bb:
Critical pair: bbbb=bbaa.
Flip LHS and RHS.
Simplify [4] abbaa=ab.
Reduce LHS:
| [9] | a(bbaa) |
| ⇒ abbbb |
Referenced by [11], [12], [15].
Overlap of [10] abbbb=ab with [6] bab=bbb:
Critical pair: abbbbbb=abab.
Reduce LHS:
| [10] | (abbbb)bb |
| ⇒ abbb |
Reduce RHS:
| [3] | (abab) |
| [9] | ⇒ (bbaa) |
| ⇒ bbbb |
Overlap of [10] abbbb=ab with [7] bbbaa=bb:
Critical pair: abbb=abaa.
Reduce LHS:
| [11] | (abbb) |
| ⇒ bbbb |
Reduce RHS:
| [2] | (abaa) |
| ⇒ b |
Defines rule #3.
Referenced by [13], [14], [15].
Overlap of [1] aab=abb with [12] bbbb=b:
Critical pair: aab=abbbbb.
Reduce LHS:
| [1] | (aab) |
| ⇒ abb |
Reduce RHS:
| [11] | (abbb)bb |
| [12] | ⇒ (bbbb)bb |
| ⇒ bbb |
Referenced by [15].
Overlap of [12] bbbb=b with [7] bbbaa=bb:
Critical pair: bbb=baa.
Flip LHS and RHS.
Defines rule #2.
Overlap of [10] abbbb=ab with [13] abb=bbb:
Critical pair: bbbbb=ab.
Reduce LHS:
| [12] | (bbbb)b |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #1.