| Back: | ⟨a, b, c | aa=1, bbbccb=1⟩ |
|---|
Completion settings:
Axiom: aa=1.
Defines rule #1.
Axiom: bbbccb=1.
Referenced by [4].
Axiom: cb=d.
Defines rule #3.
Referenced by [4], [5], [7], [8], [9], [12], [15], [22], [24], [26], [27].
Overlap of [2] bbbccb=1 with [3] cb=d:
Critical pair: bbbcd=1.
Referenced by [5], [6], [8], [11], [14], [18].
Overlap of [3] cb=d with [4] bbbcd=1:
Critical pair: c=dbbcd.
Flip LHS and RHS.
Referenced by [6], [7], [10], [12], [14], [19].
Overlap of [4] bbbcd=1 with [5] dbbcd=c:
Critical pair: bbbcc=bbcd.
Overlap of [5] dbbcd=c with [5] dbbcd=c:
Critical pair: dbbcc=cbbcd.
Reduce RHS:
| [3] | (cb)bcd |
| ⇒ dbcd |
Referenced by [12].
Overlap of [6] bbbcc=bbcd with [3] cb=d:
Critical pair: bbbcd=bbcdb.
Reduce LHS:
| [4] | (bbbcd) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [9], [10], [13].
Overlap of [3] cb=d with [8] bbcdb=1:
Critical pair: c=dbcdb.
Flip LHS and RHS.
Referenced by [11], [12], [13], [16].
Overlap of [8] bbcdb=1 with [5] dbbcd=c:
Critical pair: bbcc=bcd.
Referenced by [13].
Overlap of [4] bbbcd=1 with [9] dbcdb=c:
Critical pair: bbbcc=bcdb.
Reduce LHS:
| [6] | (bbbcc) |
| ⇒ bbcd |
Overlap of [5] dbbcd=c with [9] dbcdb=c:
Critical pair: dbbcc=cbcdb.
Reduce LHS:
| [7] | (dbbcc) |
| ⇒ dbcd |
Reduce RHS:
| [3] | (cb)cdb |
| ⇒ dcdb |
Overlap of [8] bbcdb=1 with [9] dbcdb=c:
Critical pair: bbcc=cdb.
Reduce LHS:
| [10] | (bbcc) |
| ⇒ bcd |
Defines rule #8.
Referenced by [14], [18], [20], [21], [23], [28].
Overlap of [13] bcd=cdb with [5] dbbcd=c:
Critical pair: bcc=cdbbbcd.
Reduce RHS:
| [4] | cd(bbbcd) |
| ⇒ cd |
Defines rule #9.
Referenced by [15], [16], [17].
Overlap of [3] cb=d with [14] bcc=cd:
Critical pair: ccd=dcc.
Defines rule #14.
Overlap of [9] dbcdb=c with [14] bcc=cd:
Critical pair: dbcdcd=ccc.
Reduce LHS:
| [12] | (dbcd)cd |
| [12] | ⇒ dc(dbcd) |
| ⇒ dcdcdb |
Defines rule #15.
Referenced by [22].
Overlap of [14] bcc=cd with [15] ccd=dcc:
Critical pair: bdcc=cdd.
Flip LHS and RHS.
Defines rule #11.
Referenced by [20].
Overlap of [4] bbbcd=1 with [11] bbcd=bcdb:
Critical pair: bbcdb=1.
Reduce LHS:
| [11] | (bbcd)b |
| [13] | ⇒ (bcd)bb |
| ⇒ cdbbb |
Defines rule #7.
Referenced by [23], [26], [28].
Overlap of [5] dbbcd=c with [11] bbcd=bcdb:
Critical pair: dbcdb=c.
Reduce LHS:
| [12] | (dbcd)b |
| ⇒ dcdbb |
Defines rule #10.
Referenced by [25].
Overlap of [13] bcd=cdb with [17] cdd=bdcc:
Critical pair: bbdcc=cdbd.
Flip LHS and RHS.
Defines rule #12.
Referenced by [21].
Overlap of [13] bcd=cdb with [20] cdbd=bbdcc:
Critical pair: bbbdcc=cdbbd.
Flip LHS and RHS.
Defines rule #13.
Referenced by [23].
Overlap of [15] ccd=dcc with [16] dcdcdb=ccc:
Critical pair: ccccc=dcccdcdb.
Reduce RHS:
| [15] | dc(ccd)cdb |
| [15] | ⇒ dcdc(ccd)b |
| [3] | ⇒ dcdcdc(cb) |
| ⇒ dcdcdcd |
Flip LHS and RHS.
Defines rule #16.
Overlap of [13] bcd=cdb with [21] cdbbd=bbbdcc:
Critical pair: bbbbdcc=cdbbbd.
Reduce RHS:
| [18] | (cdbbb)d |
| ⇒ d |
Referenced by [24].
Overlap of [23] bbbbdcc=d with [3] cb=d:
Critical pair: bbbbdcd=db.
Referenced by [25].
Overlap of [24] bbbbdcd=db with [19] dcdbb=c:
Critical pair: bbbbc=dbbb.
Defines rule #4.
Referenced by [26], [27], [28].
Overlap of [3] cb=d with [25] bbbbc=dbbb:
Critical pair: cdbbb=dbbbc.
Reduce LHS:
| [18] | (cdbbb) |
| ⇒ 1 |
Flip LHS and RHS.
Defines rule #6.
Overlap of [25] bbbbc=dbbb with [3] cb=d:
Critical pair: bbbbd=dbbbb.
Defines rule #2.
Overlap of [25] bbbbc=dbbb with [13] bcd=cdb:
Critical pair: bbbcdb=dbbbd.
Reduce LHS:
| [13] | bb(bcd)b |
| [13] | ⇒ b(bcd)bb |
| [13] | ⇒ (bcd)bbb |
| [18] | ⇒ (cdbbb)b |
| ⇒ b |
Flip LHS and RHS.
Defines rule #5.