| Back: | ⟨a, b | aa=1, bbabb=babb⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #1.
Axiom: bbabb=babb.
Referenced by [4].
Axiom: bb=c.
Defines rule #3.
Referenced by [4], [5], [6], [7].
Simplify [2] bbabb=babb.
Reduce RHS:
| [3] | ba(bb) |
| ⇒ bac |
Referenced by [5].
Overlap of [4] bbabb=bac with [3] bb=c:
Critical pair: cabb=bac.
Reduce LHS:
| [3] | ca(bb) |
| ⇒ cac |
Flip LHS and RHS.
Defines rule #4.
Referenced by [7].
Overlap of [3] bb=c with [3] bb=c:
Critical pair: bc=cb.
Defines rule #2.
Referenced by [7].
Overlap of [3] bb=c with [5] bac=cac:
Critical pair: bcac=cac.
Reduce LHS:
| [6] | (bc)ac |
| [5] | ⇒ c(bac) |
| ⇒ ccac |
Defines rule #5.