| Back: | ⟨a, b | aaa=b, abbbb=b⟩ |
|---|
Completion settings:
Axiom: aaa=b.
Flip LHS and RHS.
Defines rule #2.
Referenced by [2].
Axiom: abbbb=b.
Reduce LHS:
| [1] | a(b)bbb |
| [1] | ⇒ aaaa(b)bb |
| [1] | ⇒ aaaaaaa(b)b |
| [1] | ⇒ aaaaaaaaaa(b) |
| ⇒ aaaaaaaaaaaaa |
Reduce RHS:
| [1] | (b) |
| ⇒ aaa |
Defines rule #1.