| Back: | ⟨a, b | aab=aa, baa=ab⟩ |
|---|
Completion settings:
Axiom: aab=aa.
Referenced by [3], [4], [5], [6].
Axiom: baa=ab.
Referenced by [3], [4], [5], [6], [7], [8].
Overlap of [2] baa=ab with [1] aab=aa:
Critical pair: baa=abb.
Reduce LHS:
| [2] | (baa) |
| ⇒ ab |
Flip LHS and RHS.
Referenced by [5].
Overlap of [2] baa=ab with [1] aab=aa:
Critical pair: baaa=abab.
Reduce LHS:
| [2] | (baa)a |
| ⇒ aba |
Flip LHS and RHS.
Referenced by [5].
Overlap of [3] abb=ab with [2] baa=ab:
Critical pair: abab=abaa.
Reduce LHS:
| [4] | (abab) |
| ⇒ aba |
Reduce RHS:
| [2] | a(baa) |
| [1] | ⇒ (aab) |
| ⇒ aa |
Overlap of [5] aba=aa with [2] baa=ab:
Critical pair: aab=aaa.
Reduce LHS:
| [1] | (aab) |
| ⇒ aa |
Flip LHS and RHS.
Defines rule #2.
Referenced by [7].
Overlap of [2] baa=ab with [6] aaa=aa:
Critical pair: baa=aba.
Reduce LHS:
| [2] | (baa) |
| ⇒ ab |
Reduce RHS:
| [5] | (aba) |
| ⇒ aa |
Defines rule #1.
Referenced by [8].
Simplify [2] baa=ab.
Reduce RHS:
| [7] | (ab) |
| ⇒ aa |
Defines rule #3.