| Back: | ⟨a, b | aaa=a, aabb=bbb⟩ |
|---|
Completion settings:
Axiom: aaa=a.
Defines rule #1.
Referenced by [3].
Axiom: aabb=bbb.
Flip LHS and RHS.
Defines rule #2.
Referenced by [3].
Overlap of [2] bbb=aabb with [2] bbb=aabb:
Critical pair: baabb=aabbb.
Reduce RHS:
| [2] | aa(bbb) |
| [1] | ⇒ (aaa)abb |
| ⇒ aabb |
Defines rule #3.