| Back: | ⟨a, b | aa=1, ababab=bab⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #1.
Axiom: ababab=bab.
Overlap of [1] aa=1 with [2] ababab=bab:
Critical pair: abab=babab.
Flip LHS and RHS.
Defines rule #3.
Referenced by [4].
Overlap of [2] ababab=bab with [2] ababab=bab:
Critical pair: abbab=babab.
Reduce RHS:
| [3] | (babab) |
| ⇒ abab |
Referenced by [5].
Overlap of [1] aa=1 with [4] abbab=abab:
Critical pair: aabab=bbab.
Reduce LHS:
| [1] | (aa)bab |
| ⇒ bab |
Flip LHS and RHS.
Defines rule #2.