| Back: | ⟨a, b, c | ab=a, cca=bc⟩ |
|---|
Completion settings:
Axiom: ab=a.
Defines rule #1.
Axiom: cca=bc.
Referenced by [4], [7], [9], [11], [13].
Axiom: cb=d.
Defines rule #5.
Referenced by [4], [6], [8], [10], [12].
Overlap of [2] cca=bc with [1] ab=a:
Critical pair: cca=bcb.
Reduce LHS:
| [2] | (cca) |
| ⇒ bc |
Reduce RHS:
| [3] | b(cb) |
| ⇒ bd |
Defines rule #3.
Referenced by [5], [6], [7], [8], [11], [13].
Overlap of [1] ab=a with [4] bc=bd:
Critical pair: abd=ac.
Reduce LHS:
| [1] | (ab)d |
| ⇒ ad |
Flip LHS and RHS.
Defines rule #2.
Overlap of [3] cb=d with [4] bc=bd:
Critical pair: cbd=dc.
Reduce LHS:
| [3] | (cb)d |
| ⇒ dd |
Flip LHS and RHS.
Defines rule #4.
Referenced by [7], [9], [11], [12].
Overlap of [4] bc=bd with [2] cca=bc:
Critical pair: bbc=bdca.
Reduce LHS:
| [4] | b(bc) |
| ⇒ bbd |
Reduce RHS:
| [6] | b(dc)a |
| ⇒ bdda |
Flip LHS and RHS.
Defines rule #11.
Overlap of [4] bc=bd with [3] cb=d:
Critical pair: bd=bdb.
Flip LHS and RHS.
Defines rule #7.
Overlap of [5] ac=ad with [2] cca=bc:
Critical pair: abc=adca.
Reduce LHS:
| [1] | (ab)c |
| [5] | ⇒ (ac) |
| ⇒ ad |
Reduce RHS:
| [6] | a(dc)a |
| ⇒ adda |
Flip LHS and RHS.
Defines rule #10.
Overlap of [5] ac=ad with [3] cb=d:
Critical pair: ad=adb.
Flip LHS and RHS.
Defines rule #6.
Overlap of [6] dc=dd with [2] cca=bc:
Critical pair: dbc=ddca.
Reduce LHS:
| [4] | d(bc) |
| ⇒ dbd |
Reduce RHS:
| [6] | d(dc)a |
| ⇒ ddda |
Flip LHS and RHS.
Defines rule #12.
Overlap of [6] dc=dd with [3] cb=d:
Critical pair: dd=ddb.
Flip LHS and RHS.
Defines rule #8.
Simplify [2] cca=bc.
Reduce RHS:
| [4] | (bc) |
| ⇒ bd |
Defines rule #9.