| Back: | ⟨a, b | abaabbabbba=1⟩ |
|---|
Completion settings:
Axiom: abaabbabbba=1.
Referenced by [4].
Axiom: baa=c.
Referenced by [4], [5], [6], [8], [10], [11], [15], [20], [22].
Axiom: ccbba=d.
Referenced by [5], [6], [7], [12], [23], [29].
Overlap of [1] abaabbabbba=1 with [2] baa=c:
Critical pair: acbbabbba=1.
Referenced by [6], [7], [8], [9], [11], [15].
Overlap of [3] ccbba=d with [2] baa=c:
Critical pair: ccbc=da.
Flip LHS and RHS.
Overlap of [2] baa=c with [4] acbbabbba=1:
Critical pair: ba=ccbbabbba.
Reduce RHS:
| [3] | (ccbba)bbba |
| ⇒ dbbba |
Flip LHS and RHS.
Referenced by [10], [11], [22].
Overlap of [3] ccbba=d with [4] acbbabbba=1:
Critical pair: ccbb=dcbbabbba.
Flip LHS and RHS.
Referenced by [30].
Overlap of [4] acbbabbba=1 with [2] baa=c:
Critical pair: acbbabbc=a.
Referenced by [12].
Overlap of [4] acbbabbba=1 with [4] acbbabbba=1:
Critical pair: acbbabbb=cbbabbba.
Overlap of [6] dbbba=ba with [2] baa=c:
Critical pair: dbbc=baa.
Reduce RHS:
| [2] | (baa) |
| ⇒ c |
Referenced by [13].
Overlap of [6] dbbba=ba with [4] acbbabbba=1:
Critical pair: dbbb=bacbbabbba.
Reduce RHS:
| [9] | b(acbbabbb)a |
| [2] | ⇒ bcbbabb(baa) |
| ⇒ bcbbabbc |
Flip LHS and RHS.
Referenced by [13], [14], [16].
Overlap of [3] ccbba=d with [8] acbbabbc=a:
Critical pair: ccbba=dcbbabbc.
Reduce LHS:
| [3] | (ccbba) |
| ⇒ d |
Flip LHS and RHS.
Referenced by [14].
Overlap of [10] dbbc=c with [11] bcbbabbc=dbbb:
Critical pair: dbdbbb=cbbabbc.
Flip LHS and RHS.
Referenced by [15], [16], [17].
Overlap of [12] dcbbabbc=d with [11] bcbbabbc=dbbb:
Critical pair: dcbbabdbbb=dbbabbc.
Flip LHS and RHS.
Referenced by [18].
Overlap of [4] acbbabbba=1 with [9] acbbabbb=cbbabbba:
Critical pair: cbbabbbaa=1.
Reduce LHS:
| [2] | cbbabb(baa) |
| [13] | ⇒ (cbbabbc) |
| ⇒ dbdbbb |
Referenced by [16], [17], [19].
Overlap of [11] bcbbabbc=dbbb with [13] cbbabbc=dbdbbb:
Critical pair: bdbdbbb=dbbb.
Reduce LHS:
| [15] | b(dbdbbb) |
| ⇒ b |
Flip LHS and RHS.
Simplify [13] cbbabbc=dbdbbb.
Reduce RHS:
| [15] | (dbdbbb) |
| ⇒ 1 |
Referenced by [27].
Simplify [14] dbbabbc=dcbbabdbbb.
Reduce RHS:
| [16] | dcbbab(dbbb) |
| ⇒ dcbbabb |
Referenced by [31].
Simplify [15] dbdbbb=1.
Reduce LHS:
| [16] | db(dbbb) |
| ⇒ dbb |
Defines rule #2.
Referenced by [20], [22], [24], [32], [38], [39], [40], [42], [44], [46], [48], [49], [52], [55], [57], [59], [60], [61].
Overlap of [19] dbb=1 with [2] baa=c:
Critical pair: dbc=aa.
Flip LHS and RHS.
Overlap of [5] da=ccbc with [20] aa=dbc:
Critical pair: ddbc=ccbca.
Flip LHS and RHS.
Referenced by [33].
Overlap of [6] dbbba=ba with [20] aa=dbc:
Critical pair: dbbbdbc=baa.
Reduce LHS:
| [19] | (dbb)bdbc |
| ⇒ bdbc |
Reduce RHS:
| [2] | (baa) |
| ⇒ c |
Referenced by [23].
Overlap of [22] bdbc=c with [3] ccbba=d:
Critical pair: bdbd=ccbba.
Reduce RHS:
| [3] | (ccbba) |
| ⇒ d |
Overlap of [23] bdbd=d with [19] dbb=1:
Critical pair: bdb=dbb.
Reduce RHS:
| [19] | (dbb) |
| ⇒ 1 |
Overlap of [23] bdbd=d with [24] bdb=1:
Critical pair: bd=db.
Defines rule #1.
Referenced by [26], [36], [37], [39], [40], [42], [43], [44], [47], [48], [52], [57].
Overlap of [25] bd=db with [5] da=ccbc:
Critical pair: bccbc=dba.
Flip LHS and RHS.
Referenced by [28].
Overlap of [17] cbbabbc=1 with [17] cbbabbc=1:
Critical pair: cbbabb=bbabbc.
Flip LHS and RHS.
Referenced by [34].
Overlap of [24] bdb=1 with [26] dba=bccbc:
Critical pair: bbccbc=a.
Flip LHS and RHS.
Defines rule #15.
Referenced by [29], [30], [31], [32], [33], [34], [35].
Overlap of [3] ccbba=d with [28] a=bbccbc:
Critical pair: ccbbbbccbc=d.
Referenced by [36], [37], [40], [41].
Overlap of [7] dcbbabbba=ccbb with [28] a=bbccbc:
Critical pair: dcbbbbccbcbbba=ccbb.
Reduce LHS:
| [28] | dcbbbbccbcbbb(a) |
| ⇒ dcbbbbccbcbbbbbccbc |
Referenced by [45].
Simplify [18] dbbabbc=dcbbabb.
Reduce RHS:
| [28] | dcbb(a)bb |
| ⇒ dcbbbbccbcbb |
Referenced by [32].
Overlap of [31] dbbabbc=dcbbbbccbcbb with [19] dbb=1:
Critical pair: abbc=dcbbbbccbcbb.
Reduce LHS:
| [28] | (a)bbc |
| ⇒ bbccbcbbc |
Flip LHS and RHS.
Referenced by [45].
Overlap of [21] ccbca=ddbc with [28] a=bbccbc:
Critical pair: ccbcbbccbc=ddbc.
Simplify [27] bbabbc=cbbabb.
Reduce RHS:
| [28] | cbb(a)bb |
| ⇒ cbbbbccbcbb |
Referenced by [35].
Overlap of [34] bbabbc=cbbbbccbcbb with [28] a=bbccbc:
Critical pair: bbbbccbcbbc=cbbbbccbcbb.
Flip LHS and RHS.
Referenced by [54].
Overlap of [29] ccbbbbccbc=d with [29] ccbbbbccbc=d:
Critical pair: ccbbbbccbd=dcbbbbccbc.
Reduce LHS:
| [25] | ccbbbbcc(bd) |
| ⇒ ccbbbbccdb |
Referenced by [46].
Overlap of [33] ccbcbbccbc=ddbc with [29] ccbbbbccbc=d:
Critical pair: ccbcbbccbd=ddbccbbbbccbc.
Reduce LHS:
| [25] | ccbcbbcc(bd) |
| ⇒ ccbcbbccdb |
Reduce RHS:
| [29] | ddb(ccbbbbccbc) |
| [25] | ⇒ dd(bd) |
| ⇒ dddb |
Referenced by [38].
Overlap of [37] ccbcbbccdb=dddb with [19] dbb=1:
Critical pair: ccbcbbcc=dddbb.
Reduce RHS:
| [19] | dd(dbb) |
| ⇒ dd |
Defines rule #9.
Referenced by [39], [40], [41], [50].
Overlap of [33] ccbcbbccbc=ddbc with [38] ccbcbbcc=dd:
Critical pair: ccbcbbdd=ddbcbbcc.
Reduce LHS:
| [25] | ccbcb(bd)d |
| [25] | ⇒ ccbc(bd)bd |
| [19] | ⇒ ccbc(dbb)d |
| ⇒ ccbcd |
Defines rule #3.
Overlap of [38] ccbcbbcc=dd with [29] ccbbbbccbc=d:
Critical pair: ccbcbbd=ddbbbbccbc.
Reduce LHS:
| [25] | ccbcb(bd) |
| [25] | ⇒ ccbc(bd)b |
| [39] | ⇒ (ccbcd)bb |
| ⇒ ddbcbbccbb |
Reduce RHS:
| [19] | d(dbb)bbccbc |
| [19] | ⇒ (dbb)ccbc |
| ⇒ ccbc |
Referenced by [42].
Overlap of [38] ccbcbbcc=dd with [29] ccbbbbccbc=d:
Critical pair: ccbcbbcd=ddcbbbbccbc.
Defines rule #8.
Overlap of [25] bd=db with [40] ddbcbbccbb=ccbc:
Critical pair: bccbc=dbdbcbbccbb.
Reduce RHS:
| [25] | d(bd)bcbbccbb |
| [19] | ⇒ d(dbb)cbbccbb |
| ⇒ dcbbccbb |
Flip LHS and RHS.
Referenced by [43].
Overlap of [25] bd=db with [42] dcbbccbb=bccbc:
Critical pair: bbccbc=dbcbbccbb.
Flip LHS and RHS.
Referenced by [44].
Overlap of [25] bd=db with [43] dbcbbccbb=bbccbc:
Critical pair: bbbccbc=dbbcbbccbb.
Reduce RHS:
| [19] | (dbb)cbbccbb |
| ⇒ cbbccbb |
Flip LHS and RHS.
Defines rule #4.
Overlap of [30] dcbbbbccbcbbbbbccbc=ccbb with [32] dcbbbbccbcbb=bbccbcbbc:
Critical pair: bbccbcbbcbbbccbc=ccbb.
Referenced by [49], [50], [51].
Overlap of [36] ccbbbbccdb=dcbbbbccbc with [19] dbb=1:
Critical pair: ccbbbbcc=dcbbbbccbcb.
Flip LHS and RHS.
Referenced by [47], [48], [53].
Overlap of [25] bd=db with [46] dcbbbbccbcb=ccbbbbcc:
Critical pair: bccbbbbcc=dbcbbbbccbcb.
Flip LHS and RHS.
Referenced by [52].
Overlap of [46] dcbbbbccbcb=ccbbbbcc with [25] bd=db:
Critical pair: dcbbbbccbcdb=ccbbbbccd.
Reduce LHS:
| [39] | dcbbbb(ccbcd)b |
| [25] | ⇒ dcbbb(bd)dbcbbccb |
| [25] | ⇒ dcbb(bd)bdbcbbccb |
| [25] | ⇒ dcb(bd)bbdbcbbccb |
| [25] | ⇒ dc(bd)bbbdbcbbccb |
| [19] | ⇒ dc(dbb)bbdbcbbccb |
| [25] | ⇒ dcb(bd)bcbbccb |
| [25] | ⇒ dc(bd)bbcbbccb |
| [19] | ⇒ dc(dbb)bcbbccb |
| ⇒ dcbcbbccb |
Flip LHS and RHS.
Defines rule #7.
Referenced by [57].
Overlap of [19] dbb=1 with [45] bbccbcbbcbbbccbc=ccbb:
Critical pair: dccbb=ccbcbbcbbbccbc.
Flip LHS and RHS.
Referenced by [51].
Overlap of [38] ccbcbbcc=dd with [45] bbccbcbbcbbbccbc=ccbb:
Critical pair: ccbcccbb=ddbcbbcbbbccbc.
Defines rule #10.
Overlap of [49] ccbcbbcbbbccbc=dccbb with [45] bbccbcbbcbbbccbc=ccbb:
Critical pair: ccbcbbcbccbb=dccbbbbcbbbccbc.
Defines rule #13.
Overlap of [25] bd=db with [47] dbcbbbbccbcb=bccbbbbcc:
Critical pair: bbccbbbbcc=dbbcbbbbccbcb.
Reduce RHS:
| [19] | (dbb)cbbbbccbcb |
| ⇒ cbbbbccbcb |
Flip LHS and RHS.
Defines rule #6.
Overlap of [46] dcbbbbccbcb=ccbbbbcc with [52] cbbbbccbcb=bbccbbbbcc:
Critical pair: dcbbbbccbbbccbbbbcc=ccbbbbccbbbccbcb.
Flip LHS and RHS.
Referenced by [58].
Simplify [35] cbbbbccbcbb=bbbbccbcbbc.
Reduce LHS:
| [52] | (cbbbbccbcb)b |
| ⇒ bbccbbbbccb |
Overlap of [19] dbb=1 with [54] bbccbbbbccb=bbbbccbcbbc:
Critical pair: dbbbbccbcbbc=ccbbbbccb.
Reduce LHS:
| [19] | (dbb)bbccbcbbc |
| ⇒ bbccbcbbc |
Flip LHS and RHS.
Defines rule #5.
Referenced by [56], [57], [58].
Overlap of [55] ccbbbbccb=bbccbcbbc with [54] bbccbbbbccb=bbbbccbcbbc:
Critical pair: ccbbbbbbccbcbbc=bbccbcbbcbbbccb.
Flip LHS and RHS.
Referenced by [60].
Overlap of [55] ccbbbbccb=bbccbcbbc with [48] ccbbbbccd=dcbcbbccb:
Critical pair: ccbbbbdcbcbbccb=bbccbcbbcbbbccd.
Reduce LHS:
| [25] | ccbbb(bd)cbcbbccb |
| [25] | ⇒ ccbb(bd)bcbcbbccb |
| [25] | ⇒ ccb(bd)bbcbcbbccb |
| [25] | ⇒ cc(bd)bbbcbcbbccb |
| [19] | ⇒ cc(dbb)bbcbcbbccb |
| ⇒ ccbbcbcbbccb |
Flip LHS and RHS.
Referenced by [59].
Overlap of [53] ccbbbbccbbbccbcb=dcbbbbccbbbccbbbbcc with [55] ccbbbbccb=bbccbcbbc:
Critical pair: bbccbcbbcbbccbcb=dcbbbbccbbbccbbbbcc.
Referenced by [61].
Overlap of [19] dbb=1 with [57] bbccbcbbcbbbccd=ccbbcbcbbccb:
Critical pair: dccbbcbcbbccb=ccbcbbcbbbccd.
Flip LHS and RHS.
Defines rule #12.
Overlap of [19] dbb=1 with [56] bbccbcbbcbbbccb=ccbbbbbbccbcbbc:
Critical pair: dccbbbbbbccbcbbc=ccbcbbcbbbccb.
Flip LHS and RHS.
Defines rule #11.
Overlap of [19] dbb=1 with [58] bbccbcbbcbbccbcb=dcbbbbccbbbccbbbbcc:
Critical pair: ddcbbbbccbbbccbbbbcc=ccbcbbcbbccbcb.
Flip LHS and RHS.
Defines rule #14.