| Back: | ⟨a, b, c | ab=c, bca=bc⟩ |
|---|
Completion settings:
Axiom: ab=c.
Defines rule #1.
Axiom: bca=bc.
Defines rule #4.
Overlap of [1] ab=c with [2] bca=bc:
Critical pair: abc=cca.
Reduce LHS:
| [1] | (ab)c |
| ⇒ cc |
Flip LHS and RHS.
Defines rule #2.
Referenced by [5].
Overlap of [2] bca=bc with [1] ab=c:
Critical pair: bcc=bcb.
Flip LHS and RHS.
Defines rule #5.
Overlap of [3] cca=cc with [1] ab=c:
Critical pair: ccc=ccb.
Flip LHS and RHS.
Defines rule #3.