| Back: | ⟨a, b | aaa=ab, bbaa=a⟩ |
|---|
Completion settings:
Axiom: aaa=ab.
Flip LHS and RHS.
Defines rule #2.
Referenced by [3].
Axiom: bbaa=a.
Overlap of [1] ab=aaa with [2] bbaa=a:
Critical pair: aa=aaabaa.
Reduce RHS:
| [1] | aa(ab)aa |
| ⇒ aaaaaaa |
Flip LHS and RHS.
Referenced by [4].
Overlap of [2] bbaa=a with [3] aaaaaaa=aa:
Critical pair: bbaa=aaaaaa.
Reduce LHS:
| [2] | (bbaa) |
| ⇒ a |
Flip LHS and RHS.
Defines rule #1.
Referenced by [5].
Overlap of [2] bbaa=a with [4] aaaaaa=a:
Critical pair: bba=aaaaa.
Defines rule #3.