| Back: | ⟨a, b, c | ba=ac, bccb=1⟩ |
|---|
Completion settings:
Axiom: ba=ac.
Defines rule #12.
Axiom: bccb=1.
Referenced by [4].
Axiom: cb=d.
Defines rule #2.
Referenced by [4], [5], [8], [9], [16].
Overlap of [2] bccb=1 with [3] cb=d:
Critical pair: bcd=1.
Defines rule #7.
Referenced by [5], [6], [9], [14].
Overlap of [3] cb=d with [4] bcd=1:
Critical pair: c=dcd.
Flip LHS and RHS.
Defines rule #9.
Overlap of [4] bcd=1 with [5] dcd=c:
Critical pair: bcc=cd.
Defines rule #8.
Referenced by [9], [10], [18].
Overlap of [5] dcd=c with [5] dcd=c:
Critical pair: dcc=ccd.
Flip LHS and RHS.
Defines rule #11.
Referenced by [18].
Overlap of [3] cb=d with [1] ba=ac:
Critical pair: cac=da.
Referenced by [12].
Overlap of [6] bcc=cd with [3] cb=d:
Critical pair: bcd=cdb.
Reduce LHS:
| [4] | (bcd) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #6.
Referenced by [10], [11], [12], [13], [15].
Overlap of [6] bcc=cd with [9] cdb=1:
Critical pair: bc=cddb.
Flip LHS and RHS.
Overlap of [9] cdb=1 with [1] ba=ac:
Critical pair: cdac=a.
Referenced by [13].
Overlap of [8] cac=da with [9] cdb=1:
Critical pair: ca=dadb.
Defines rule #13.
Overlap of [11] cdac=a with [9] cdb=1:
Critical pair: cda=adb.
Defines rule #14.
Overlap of [4] bcd=1 with [10] cddb=bc:
Critical pair: bbc=db.
Defines rule #3.
Overlap of [5] dcd=c with [10] cddb=bc:
Critical pair: dbc=cdb.
Reduce RHS:
| [9] | (cdb) |
| ⇒ 1 |
Defines rule #5.
Referenced by [16].
Overlap of [15] dbc=1 with [3] cb=d:
Critical pair: dbd=b.
Defines rule #4.
Referenced by [17].
Overlap of [16] dbd=b with [16] dbd=b:
Critical pair: dbb=bbd.
Flip LHS and RHS.
Defines rule #1.
Overlap of [6] bcc=cd with [7] ccd=dcc:
Critical pair: bdcc=cdd.
Flip LHS and RHS.
Defines rule #10.