| Back: | ⟨a, b | aabbbabbaab=1⟩ |
|---|
Completion settings:
Axiom: aabbbabbaab=1.
Referenced by [4].
Axiom: baa=c.
Referenced by [4], [5], [6], [7], [8], [9], [20].
Axiom: abccb=d.
Referenced by [5], [12], [14], [15], [25].
Overlap of [1] aabbbabbaab=1 with [2] baa=c:
Critical pair: aabbbabcb=1.
Referenced by [6], [7], [8], [10], [12].
Overlap of [2] baa=c with [3] abccb=d:
Critical pair: bad=cbccb.
Referenced by [18].
Overlap of [2] baa=c with [4] aabbbabcb=1:
Critical pair: b=cbbbabcb.
Flip LHS and RHS.
Overlap of [2] baa=c with [4] aabbbabcb=1:
Critical pair: ba=cabbbabcb.
Flip LHS and RHS.
Referenced by [26].
Overlap of [4] aabbbabcb=1 with [2] baa=c:
Critical pair: aabbbabcc=aa.
Referenced by [13].
Overlap of [6] cbbbabcb=b with [2] baa=c:
Critical pair: cbbbabcc=baa.
Reduce RHS:
| [2] | (baa) |
| ⇒ c |
Overlap of [4] aabbbabcb=1 with [9] cbbbabcc=c:
Critical pair: aabbbabc=bbabcc.
Overlap of [6] cbbbabcb=b with [9] cbbbabcc=c:
Critical pair: cbbbabc=bbbabcc.
Overlap of [4] aabbbabcb=1 with [10] aabbbabc=bbabcc:
Critical pair: bbabccb=1.
Reduce LHS:
| [3] | bb(abccb) |
| ⇒ bbd |
Defines rule #2.
Referenced by [14], [16], [19], [22], [24], [27], [32], [33], [35], [36], [38], [40], [41], [42], [44], [47], [48], [49], [50], [51], [52].
Overlap of [8] aabbbabcc=aa with [10] aabbbabc=bbabcc:
Critical pair: bbabccc=aa.
Flip LHS and RHS.
Referenced by [19].
Overlap of [3] abccb=d with [12] bbd=1:
Critical pair: abcc=dbd.
Referenced by [15], [19], [21], [23], [30].
Overlap of [3] abccb=d with [14] abcc=dbd:
Critical pair: dbdb=d.
Overlap of [12] bbd=1 with [15] dbdb=d:
Critical pair: bbd=bdb.
Reduce LHS:
| [12] | (bbd) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [17], [21], [23].
Overlap of [16] bdb=1 with [15] dbdb=d:
Critical pair: bd=db.
Flip LHS and RHS.
Defines rule #1.
Referenced by [18], [21], [23], [30], [33], [36], [39], [42], [44], [47], [48].
Overlap of [5] bad=cbccb with [17] db=bd:
Critical pair: babd=cbccbb.
Referenced by [20].
Simplify [13] aa=bbabccc.
Reduce RHS:
| [14] | bb(abcc)c |
| [12] | ⇒ (bbd)bdc |
| ⇒ bdc |
Referenced by [20].
Overlap of [2] baa=c with [19] aa=bdc:
Critical pair: babdc=ca.
Reduce LHS:
| [18] | (babd)c |
| ⇒ cbccbbc |
Flip LHS and RHS.
Overlap of [14] abcc=dbd with [20] ca=cbccbbc:
Critical pair: abccbccbbc=dbda.
Reduce LHS:
| [14] | (abcc)bccbbc |
| [17] | ⇒ (db)dbccbbc |
| [17] | ⇒ bd(db)ccbbc |
| [16] | ⇒ (bdb)dccbbc |
| ⇒ dccbbc |
Reduce RHS:
| [17] | (db)da |
| ⇒ bdda |
Flip LHS and RHS.
Overlap of [12] bbd=1 with [21] bdda=dccbbc:
Critical pair: bdccbbc=da.
Flip LHS and RHS.
Referenced by [24].
Overlap of [21] bdda=dccbbc with [14] abcc=dbd:
Critical pair: bdddbd=dccbbcbcc.
Reduce LHS:
| [17] | bdd(db)d |
| [17] | ⇒ bd(db)dd |
| [16] | ⇒ (bdb)ddd |
| ⇒ ddd |
Flip LHS and RHS.
Referenced by [32].
Overlap of [12] bbd=1 with [22] da=bdccbbc:
Critical pair: bbbdccbbc=a.
Reduce LHS:
| [12] | b(bbd)ccbbc |
| ⇒ bccbbc |
Flip LHS and RHS.
Defines rule #15.
Referenced by [25], [26], [27], [28], [29], [31].
Overlap of [3] abccb=d with [24] a=bccbbc:
Critical pair: bccbbcbccb=d.
Referenced by [27].
Simplify [7] cabbbabcb=ba.
Reduce RHS:
| [24] | b(a) |
| ⇒ bbccbbc |
Referenced by [27].
Overlap of [26] cabbbabcb=bbccbbc with [20] ca=cbccbbc:
Critical pair: cbccbbcbbbabcb=bbccbbc.
Reduce LHS:
| [11] | cbccbb(cbbbabc)b |
| [24] | ⇒ cbccbbbbb(a)bccb |
| [25] | ⇒ cbccbbbbb(bccbbcbccb) |
| [12] | ⇒ cbccbbb(bbd) |
| ⇒ cbccbbb |
Flip LHS and RHS.
Defines rule #4.
Referenced by [28], [29], [34], [35], [38].
Simplify [11] cbbbabc=bbbabcc.
Reduce RHS:
| [24] | bbb(a)bcc |
| [27] | ⇒ bb(bbccbbc)bcc |
| ⇒ bbcbccbbbbcc |
Referenced by [29].
Overlap of [28] cbbbabc=bbcbccbbbbcc with [24] a=bccbbc:
Critical pair: cbbbbccbbcbc=bbcbccbbbbcc.
Reduce LHS:
| [27] | cbb(bbccbbc)bc |
| ⇒ cbbcbccbbbbc |
Flip LHS and RHS.
Referenced by [40].
Simplify [14] abcc=dbd.
Reduce RHS:
| [17] | (db)d |
| ⇒ bdd |
Referenced by [31].
Overlap of [30] abcc=bdd with [24] a=bccbbc:
Critical pair: bccbbcbcc=bdd.
Referenced by [33], [35], [36].
Overlap of [12] bbd=1 with [23] dccbbcbcc=ddd:
Critical pair: bbddd=ccbbcbcc.
Reduce LHS:
| [12] | (bbd)dd |
| ⇒ dd |
Flip LHS and RHS.
Defines rule #9.
Referenced by [33], [37], [47].
Overlap of [32] ccbbcbcc=dd with [31] bccbbcbcc=bdd:
Critical pair: ccbbcbdd=ddbbcbcc.
Reduce RHS:
| [17] | d(db)bcbcc |
| [17] | ⇒ (db)dbcbcc |
| [17] | ⇒ bd(db)cbcc |
| [17] | ⇒ b(db)dcbcc |
| [12] | ⇒ (bbd)dcbcc |
| ⇒ dcbcc |
Flip LHS and RHS.
Defines rule #3.
Overlap of [27] bbccbbc=cbccbbb with [27] bbccbbc=cbccbbb:
Critical pair: bbcccbccbbb=cbccbbbcbbc.
Referenced by [46].
Overlap of [27] bbccbbc=cbccbbb with [31] bccbbcbcc=bdd:
Critical pair: bbdd=cbccbbbbcc.
Reduce LHS:
| [12] | (bbd)d |
| ⇒ d |
Flip LHS and RHS.
Referenced by [36], [37], [40], [41], [46].
Overlap of [31] bccbbcbcc=bdd with [35] cbccbbbbcc=d:
Critical pair: bccbbcbcd=bddbccbbbbcc.
Reduce RHS:
| [17] | bd(db)ccbbbbcc |
| [17] | ⇒ b(db)dccbbbbcc |
| [12] | ⇒ (bbd)dccbbbbcc |
| ⇒ dccbbbbcc |
Flip LHS and RHS.
Defines rule #7.
Overlap of [35] cbccbbbbcc=d with [32] ccbbcbcc=dd:
Critical pair: cbccbbbbcdd=dcbbcbcc.
Flip LHS and RHS.
Defines rule #8.
Overlap of [12] bbd=1 with [36] dccbbbbcc=bccbbcbcd:
Critical pair: bbbccbbcbcd=ccbbbbcc.
Reduce LHS:
| [27] | b(bbccbbc)bcd |
| ⇒ bcbccbbbbcd |
Referenced by [39].
Overlap of [38] bcbccbbbbcd=ccbbbbcc with [17] db=bd:
Critical pair: bcbccbbbbcbd=ccbbbbccb.
Referenced by [44].
Overlap of [29] bbcbccbbbbcc=cbbcbccbbbbc with [35] cbccbbbbcc=d:
Critical pair: bbd=cbbcbccbbbbc.
Reduce LHS:
| [12] | (bbd) |
| ⇒ 1 |
Flip LHS and RHS.
Referenced by [41].
Overlap of [40] cbbcbccbbbbc=1 with [35] cbccbbbbcc=d:
Critical pair: cbbcbccbbbbd=bccbbbbcc.
Reduce LHS:
| [12] | cbbcbccbb(bbd) |
| ⇒ cbbcbccbb |
Flip LHS and RHS.
Defines rule #5.
Referenced by [42], [43], [45].
Overlap of [36] dccbbbbcc=bccbbcbcd with [41] bccbbbbcc=cbbcbccbb:
Critical pair: dccbbbcbbcbccbb=bccbbcbcdbbbbcc.
Reduce RHS:
| [17] | bccbbcbc(db)bbbcc |
| [17] | ⇒ bccbbcbcb(db)bbcc |
| [12] | ⇒ bccbbcbc(bbd)bbcc |
| ⇒ bccbbcbcbbcc |
Referenced by [49].
Overlap of [41] bccbbbbcc=cbbcbccbb with [41] bccbbbbcc=cbbcbccbb:
Critical pair: bccbbbcbbcbccbb=cbbcbccbbbbbbcc.
Referenced by [50].
Overlap of [39] bcbccbbbbcbd=ccbbbbccb with [17] db=bd:
Critical pair: bcbccbbbbcbbd=ccbbbbccbb.
Reduce LHS:
| [12] | bcbccbbbbc(bbd) |
| ⇒ bcbccbbbbc |
Defines rule #6.
Referenced by [45].
Overlap of [44] bcbccbbbbc=ccbbbbccbb with [44] bcbccbbbbc=ccbbbbccbb:
Critical pair: bcbccbbbccbbbbccbb=ccbbbbccbbbccbbbbc.
Reduce LHS:
| [41] | bcbccbb(bccbbbbcc)bb |
| ⇒ bcbccbbcbbcbccbbbb |
Referenced by [51].
Overlap of [34] bbcccbccbbb=cbccbbbcbbc with [35] cbccbbbbcc=d:
Critical pair: bbccd=cbccbbbcbbcbcc.
Flip LHS and RHS.
Overlap of [46] cbccbbbcbbcbcc=bbccd with [32] ccbbcbcc=dd:
Critical pair: cbccbbbcbbcbdd=bbccdbbcbcc.
Reduce RHS:
| [17] | bbcc(db)bcbcc |
| [17] | ⇒ bbccb(db)cbcc |
| [12] | ⇒ bbcc(bbd)cbcc |
| ⇒ bbcccbcc |
Flip LHS and RHS.
Defines rule #10.
Overlap of [46] cbccbbbcbbcbcc=bbccd with [46] cbccbbbcbbcbcc=bbccd:
Critical pair: cbccbbbcbbbbccd=bbccdbbbcbbcbcc.
Reduce RHS:
| [17] | bbcc(db)bbcbbcbcc |
| [17] | ⇒ bbccb(db)bcbbcbcc |
| [12] | ⇒ bbcc(bbd)bcbbcbcc |
| ⇒ bbccbcbbcbcc |
Flip LHS and RHS.
Defines rule #13.
Overlap of [42] dccbbbcbbcbccbb=bccbbcbcbbcc with [12] bbd=1:
Critical pair: dccbbbcbbcbcc=bccbbcbcbbccd.
Defines rule #12.
Overlap of [43] bccbbbcbbcbccbb=cbbcbccbbbbbbcc with [12] bbd=1:
Critical pair: bccbbbcbbcbcc=cbbcbccbbbbbbccd.
Defines rule #11.
Overlap of [45] bcbccbbcbbcbccbbbb=ccbbbbccbbbccbbbbc with [12] bbd=1:
Critical pair: bcbccbbcbbcbccbb=ccbbbbccbbbccbbbbcd.
Referenced by [52].
Overlap of [51] bcbccbbcbbcbccbb=ccbbbbccbbbccbbbbcd with [12] bbd=1:
Critical pair: bcbccbbcbbcbcc=ccbbbbccbbbccbbbbcdd.
Defines rule #14.