| Back: | ⟨a, b, c | ab=1, cbbcc=b⟩ |
|---|
Completion settings:
Axiom: ab=1.
Axiom: cbbcc=b.
Referenced by [5].
Axiom: cb=d.
Referenced by [5], [6], [8], [11], [12], [13], [15], [21].
Axiom: bdbc=e.
Referenced by [7], [8], [9], [10], [22].
Overlap of [2] cbbcc=b with [3] cb=d:
Critical pair: dbcc=b.
Referenced by [6], [9], [11], [14], [16], [18].
Overlap of [5] dbcc=b with [3] cb=d:
Critical pair: dbcd=bb.
Flip LHS and RHS.
Referenced by [9].
Overlap of [1] ab=1 with [4] bdbc=e:
Critical pair: ae=dbc.
Referenced by [23].
Overlap of [3] cb=d with [4] bdbc=e:
Critical pair: ce=ddbc.
Flip LHS and RHS.
Referenced by [16], [17], [24].
Overlap of [4] bdbc=e with [5] dbcc=b:
Critical pair: bb=ec.
Reduce LHS:
| [6] | (bb) |
| ⇒ dbcd |
Referenced by [10], [11], [14], [17], [19].
Overlap of [4] bdbc=e with [9] dbcd=ec:
Critical pair: bec=ed.
Overlap of [9] dbcd=ec with [5] dbcc=b:
Critical pair: dbcb=ecbcc.
Reduce LHS:
| [3] | db(cb) |
| ⇒ dbd |
Reduce RHS:
| [3] | e(cb)cc |
| ⇒ edcc |
Referenced by [25].
Overlap of [3] cb=d with [10] bec=ed:
Critical pair: ced=dec.
Flip LHS and RHS.
Referenced by [14], [15], [29].
Overlap of [10] bec=ed with [3] cb=d:
Critical pair: bed=edb.
Referenced by [14].
Overlap of [9] dbcd=ec with [12] dec=ced:
Critical pair: dbcced=ecec.
Reduce LHS:
| [5] | (dbcc)ed |
| [13] | ⇒ (bed) |
| ⇒ edb |
Referenced by [15].
Overlap of [12] dec=ced with [3] cb=d:
Critical pair: ded=cedb.
Reduce RHS:
| [14] | c(edb) |
| ⇒ cecec |
Flip LHS and RHS.
Referenced by [27].
Overlap of [8] ddbc=ce with [5] dbcc=b:
Critical pair: db=cec.
Referenced by [17], [18], [19], [22], [23], [24], [25].
Overlap of [9] dbcd=ec with [8] ddbc=ce:
Critical pair: dbcce=ecdbc.
Reduce LHS:
| [16] | (db)cce |
| ⇒ ceccce |
Reduce RHS:
| [16] | ec(db)c |
| ⇒ eccecc |
Defines rule #13.
Overlap of [5] dbcc=b with [16] db=cec:
Critical pair: ceccc=b.
Flip LHS and RHS.
Defines rule #7.
Referenced by [20], [21], [22].
Overlap of [9] dbcd=ec with [16] db=cec:
Critical pair: ceccd=ec.
Defines rule #3.
Overlap of [1] ab=1 with [18] b=ceccc:
Critical pair: aceccc=1.
Defines rule #9.
Overlap of [3] cb=d with [18] b=ceccc:
Critical pair: cceccc=d.
Defines rule #5.
Referenced by [28].
Overlap of [4] bdbc=e with [16] db=cec:
Critical pair: bcecc=e.
Reduce LHS:
| [18] | (b)cecc |
| ⇒ ceccccecc |
Defines rule #14.
Simplify [7] ae=dbc.
Reduce RHS:
| [16] | (db)c |
| ⇒ cecc |
Defines rule #8.
Overlap of [8] ddbc=ce with [16] db=cec:
Critical pair: dcecc=ce.
Defines rule #6.
Referenced by [26], [28], [30].
Overlap of [11] dbd=edcc with [16] db=cec:
Critical pair: cecd=edcc.
Defines rule #2.
Referenced by [26].
Overlap of [25] cecd=edcc with [24] dcecc=ce:
Critical pair: cecce=edcccecc.
Defines rule #12.
Referenced by [28].
Overlap of [15] cecec=ded with [22] ceccccecc=e:
Critical pair: cee=dedcccecc.
Flip LHS and RHS.
Referenced by [31].
Overlap of [24] dcecc=ce with [22] ceccccecc=e:
Critical pair: de=ceccecc.
Reduce RHS:
| [26] | (cecce)cc |
| [21] | ⇒ edc(cceccc)c |
| ⇒ edcdc |
Defines rule #4.
Overlap of [12] dec=ced with [28] de=edcdc:
Critical pair: edcdcc=ced.
Flip LHS and RHS.
Defines rule #1.
Referenced by [30].
Overlap of [29] ced=edcdcc with [24] dcecc=ce:
Critical pair: cece=edcdcccecc.
Defines rule #11.
Simplify [27] dedcccecc=cee.
Reduce LHS:
| [28] | (de)dcccecc |
| ⇒ edcdcdcccecc |
Flip LHS and RHS.
Defines rule #10.