| Back: | ⟨a, b | aaaa=1, abbba=bb⟩ |
|---|
Completion settings:
Axiom: aaaa=1.
Defines rule #35.
Referenced by [5], [6], [8], [14], [15].
Axiom: abbba=bb.
Referenced by [5], [6], [7], [9], [13], [20].
Axiom: bababa=c.
Defines rule #33.
Referenced by [7], [8], [9], [10], [17], [28], [34], [110], [146].
Axiom: cbcbcbc=d.
Referenced by [11], [12], [18], [27], [31], [32], [37], [42], [47], [53], [58], [59], [64].
Overlap of [1] aaaa=1 with [2] abbba=bb:
Critical pair: aaabb=bbba.
Overlap of [2] abbba=bb with [1] aaaa=1:
Critical pair: abbb=bbaaa.
Flip LHS and RHS.
Referenced by [21].
Overlap of [2] abbba=bb with [3] bababa=c:
Critical pair: abbc=bbbaba.
Flip LHS and RHS.
Overlap of [3] bababa=c with [1] aaaa=1:
Critical pair: babab=caaa.
Flip LHS and RHS.
Defines rule #34.
Referenced by [27], [136], [139].
Overlap of [3] bababa=c with [2] abbba=bb:
Critical pair: bababbb=cbbba.
Referenced by [22].
Overlap of [3] bababa=c with [3] bababa=c:
Critical pair: bac=cba.
Flip LHS and RHS.
Defines rule #30.
Referenced by [12], [16], [19], [20], [26], [29], [31], [54].
Overlap of [4] cbcbcbc=d with [4] cbcbcbc=d:
Critical pair: cbd=dbc.
Flip LHS and RHS.
Referenced by [35], [48], [60], [84], [89], [90], [91], [110], [111], [112], [135], [137], [141].
Overlap of [4] cbcbcbc=d with [10] cba=bac:
Critical pair: cbcbcbbac=dba.
Referenced by [37].
Overlap of [5] aaabb=bbba with [2] abbba=bb:
Critical pair: aabb=bbbaba.
Reduce RHS:
| [7] | (bbbaba) |
| ⇒ abbc |
Overlap of [1] aaaa=1 with [13] aabb=abbc:
Critical pair: aaabbc=bb.
Reduce LHS:
| [5] | (aaabb)c |
| ⇒ bbbac |
Overlap of [1] aaaa=1 with [13] aabb=abbc:
Critical pair: aaaabbc=abb.
Reduce LHS:
| [1] | (aaaa)bbc |
| ⇒ bbc |
Flip LHS and RHS.
Defines rule #18.
Referenced by [16], [17], [19], [20], [21], [23], [25], [26], [29], [30], [31], [33], [41], [43], [44], [45], [52], [75], [82].
Overlap of [10] cba=bac with [15] abb=bbc:
Critical pair: cbbbc=bacbb.
Flip LHS and RHS.
Referenced by [28], [32], [83].
Overlap of [15] abb=bbc with [3] bababa=c:
Critical pair: abc=bbcababa.
Flip LHS and RHS.
Referenced by [38].
Overlap of [14] bbbac=bb with [4] cbcbcbc=d:
Critical pair: bbbad=bbbcbcbc.
Referenced by [24].
Overlap of [14] bbbac=bb with [10] cba=bac:
Critical pair: bbbabac=bbba.
Reduce LHS:
| [7] | (bbbaba)c |
| [15] | ⇒ (abb)cc |
| ⇒ bbccc |
Flip LHS and RHS.
Referenced by [20], [22], [24], [25], [26], [29], [31], [36].
Overlap of [2] abbba=bb with [15] abb=bbc:
Critical pair: bbcba=bb.
Reduce LHS:
| [10] | bb(cba) |
| [19] | ⇒ (bbba)c |
| ⇒ bbcccc |
Referenced by [26], [29], [31], [55], [72].
Simplify [6] bbaaa=abbb.
Reduce RHS:
| [15] | (abb)b |
| ⇒ bbcb |
Referenced by [26].
Simplify [9] bababbb=cbbba.
Reduce RHS:
| [19] | c(bbba) |
| ⇒ cbbccc |
Referenced by [23].
Overlap of [22] bababbb=cbbccc with [15] abb=bbc:
Critical pair: babbbcb=cbbccc.
Reduce LHS:
| [15] | b(abb)bcb |
| ⇒ bbbcbcb |
Flip LHS and RHS.
Overlap of [18] bbbad=bbbcbcbc with [19] bbba=bbccc:
Critical pair: bbcccd=bbbcbcbc.
Flip LHS and RHS.
Overlap of [15] abb=bbc with [19] bbba=bbccc:
Critical pair: abbbccc=bbcbba.
Reduce LHS:
| [15] | (abb)bccc |
| ⇒ bbcbccc |
Flip LHS and RHS.
Referenced by [39].
Overlap of [15] abb=bbc with [21] bbaaa=bbcb:
Critical pair: abbbcb=bbcbaaa.
Reduce LHS:
| [15] | (abb)bcb |
| ⇒ bbcbcb |
Reduce RHS:
| [10] | bb(cba)aa |
| [19] | ⇒ (bbba)caa |
| [20] | ⇒ (bbcccc)aa |
| ⇒ bbaa |
Flip LHS and RHS.
Referenced by [29].
Overlap of [4] cbcbcbc=d with [8] caaa=babab:
Critical pair: cbcbcbbabab=daaa.
Flip LHS and RHS.
Referenced by [40].
Overlap of [3] bababa=c with [16] bacbb=cbbbc:
Critical pair: babacbbbc=ccbb.
Reduce LHS:
| [16] | ba(bacbb)bc |
| [16] | ⇒ (bacbb)bcbc |
| [24] | ⇒ c(bbbcbcbc) |
| [23] | ⇒ (cbbccc)d |
| ⇒ bbbcbcbd |
Referenced by [49].
Overlap of [15] abb=bbc with [26] bbaa=bbcbcb:
Critical pair: abbbcbcb=bbcbaa.
Reduce LHS:
| [15] | (abb)bcbcb |
| ⇒ bbcbcbcb |
Reduce RHS:
| [10] | bb(cba)a |
| [19] | ⇒ (bbba)ca |
| [20] | ⇒ (bbcccc)a |
| ⇒ bba |
Flip LHS and RHS.
Referenced by [30], [31], [32], [36], [37], [38], [39], [40], [46], [51], [54], [66].
Overlap of [15] abb=bbc with [29] bba=bbcbcbcb:
Critical pair: abbcbcbcb=bbca.
Reduce LHS:
| [15] | (abb)cbcbcb |
| ⇒ bbccbcbcb |
Flip LHS and RHS.
Referenced by [38].
Overlap of [15] abb=bbc with [29] bba=bbcbcbcb:
Critical pair: abbbcbcbcb=bbcba.
Reduce LHS:
| [15] | (abb)bcbcbcb |
| [4] | ⇒ bb(cbcbcbc)b |
| ⇒ bbdb |
Reduce RHS:
| [10] | bb(cba) |
| [19] | ⇒ (bbba)c |
| [20] | ⇒ (bbcccc) |
| ⇒ bb |
Referenced by [32], [33], [34], [35], [36], [54], [79].
Overlap of [29] bba=bbcbcbcb with [16] bacbb=cbbbc:
Critical pair: bcbbbc=bbcbcbcbcbb.
Reduce RHS:
| [4] | bb(cbcbcbc)bb |
| [31] | ⇒ (bbdb)b |
| ⇒ bbb |
Referenced by [47], [48], [87].
Overlap of [15] abb=bbc with [31] bbdb=bb:
Critical pair: abb=bbcdb.
Reduce LHS:
| [15] | (abb) |
| ⇒ bbc |
Flip LHS and RHS.
Overlap of [31] bbdb=bb with [3] bababa=c:
Critical pair: bbdc=bbababa.
Reduce RHS:
| [3] | b(bababa) |
| ⇒ bc |
Referenced by [41], [42], [55], [56], [65], [73], [80], [84].
Overlap of [31] bbdb=bb with [11] dbc=cbd:
Critical pair: bbcbd=bbc.
Overlap of [31] bbdb=bb with [29] bba=bbcbcbcb:
Critical pair: bbdbbcbcbcb=bbba.
Reduce LHS:
| [31] | (bbdb)bcbcbcb |
| [24] | ⇒ (bbbcbcbc)b |
| ⇒ bbcccdb |
Reduce RHS:
| [19] | (bbba) |
| ⇒ bbccc |
Referenced by [67].
Overlap of [12] cbcbcbbac=dba with [29] bba=bbcbcbcb:
Critical pair: cbcbcbbcbcbcbc=dba.
Reduce LHS:
| [4] | cbcbcbb(cbcbcbc) |
| ⇒ cbcbcbbd |
Flip LHS and RHS.
Referenced by [94].
Overlap of [17] bbcababa=abc with [30] bbca=bbccbcbcb:
Critical pair: bbccbcbcbbaba=abc.
Reduce LHS:
| [29] | bbccbcbc(bba)ba |
| [29] | ⇒ bbccbcbcbbcbcbc(bba) |
| ⇒ bbccbcbcbbcbcbcbbcbcbcb |
Flip LHS and RHS.
Overlap of [25] bbcbba=bbcbccc with [29] bba=bbcbcbcb:
Critical pair: bbcbbcbcbcb=bbcbccc.
Referenced by [54].
Simplify [27] daaa=cbcbcbbabab.
Reduce RHS:
| [29] | cbcbc(bba)bab |
| [29] | ⇒ cbcbcbbcbcbc(bba)b |
| ⇒ cbcbcbbcbcbcbbcbcbcbb |
Referenced by [65].
Overlap of [15] abb=bbc with [34] bbdc=bc:
Critical pair: abc=bbcdc.
Reduce LHS:
| [38] | (abc) |
| ⇒ bbccbcbcbbcbcbcbbcbcbcb |
Referenced by [50].
Overlap of [34] bbdc=bc with [4] cbcbcbc=d:
Critical pair: bbdd=bcbcbcbc.
Reduce RHS:
| [4] | b(cbcbcbc) |
| ⇒ bd |
Referenced by [43], [57], [74], [79], [81], [85].
Overlap of [15] abb=bbc with [42] bbdd=bd:
Critical pair: abd=bbcdd.
Referenced by [46], [82], [88], [114], [116].
Overlap of [15] abb=bbc with [33] bbcdb=bbc:
Critical pair: abbc=bbccdb.
Reduce LHS:
| [15] | (abb)c |
| ⇒ bbcc |
Flip LHS and RHS.
Referenced by [90].
Overlap of [15] abb=bbc with [35] bbcbd=bbc:
Critical pair: abbbc=bbcbcbd.
Reduce LHS:
| [15] | (abb)bc |
| ⇒ bbcbc |
Flip LHS and RHS.
Referenced by [49].
Overlap of [29] bba=bbcbcbcb with [43] abd=bbcdd:
Critical pair: bbbbcdd=bbcbcbcbbd.
Flip LHS and RHS.
Referenced by [68].
Overlap of [4] cbcbcbc=d with [32] bcbbbc=bbb:
Critical pair: cbcbcbbb=dbbbc.
Referenced by [65].
Overlap of [11] dbc=cbd with [32] bcbbbc=bbb:
Critical pair: dbbb=cbdbbbc.
Flip LHS and RHS.
Referenced by [95].
Overlap of [28] bbbcbcbd=ccbb with [45] bbcbcbd=bbcbc:
Critical pair: bbbcbc=ccbb.
Defines rule #12.
Referenced by [52], [53], [54], [61], [62], [65], [144].
Simplify [38] abc=bbccbcbcbbcbcbcbbcbcbcb.
Reduce RHS:
| [41] | (bbccbcbcbbcbcbcbbcbcbcb) |
| ⇒ bbcdc |
Overlap of [29] bba=bbcbcbcb with [50] abc=bbcdc:
Critical pair: bbbbcdc=bbcbcbcbbc.
Flip LHS and RHS.
Referenced by [65].
Overlap of [15] abb=bbc with [49] bbbcbc=ccbb:
Critical pair: accbb=bbcbcbc.
Referenced by [69].
Overlap of [49] bbbcbc=ccbb with [4] cbcbcbc=d:
Critical pair: bbbd=ccbbbcbc.
Reduce RHS:
| [49] | cc(bbbcbc) |
| ⇒ ccccbb |
Flip LHS and RHS.
Referenced by [54], [55], [56], [57], [62], [70].
Overlap of [49] bbbcbc=ccbb with [10] cba=bac:
Critical pair: bbbcbbac=ccbbba.
Reduce LHS:
| [29] | bbbc(bba)c |
| [39] | ⇒ b(bbcbbcbcbcb)c |
| [49] | ⇒ (bbbcbc)ccc |
| [23] | ⇒ c(cbbccc) |
| [49] | ⇒ c(bbbcbc)b |
| ⇒ cccbbb |
Reduce RHS:
| [29] | ccb(bba) |
| [49] | ⇒ cc(bbbcbc)bcb |
| [53] | ⇒ (ccccbb)bcb |
| [31] | ⇒ b(bbdb)cb |
| ⇒ bbbcb |
Overlap of [53] ccccbb=bbbd with [20] bbcccc=bb:
Critical pair: ccccbb=bbbdcccc.
Reduce LHS:
| [53] | (ccccbb) |
| ⇒ bbbd |
Reduce RHS:
| [34] | b(bbdc)ccc |
| [20] | ⇒ (bbcccc) |
| ⇒ bb |
Referenced by [56], [57], [62], [63], [70], [77], [83], [93], [96].
Overlap of [53] ccccbb=bbbd with [34] bbdc=bc:
Critical pair: ccccbc=bbbddc.
Reduce RHS:
| [55] | (bbbd)dc |
| [34] | ⇒ (bbdc) |
| ⇒ bc |
Referenced by [59].
Overlap of [53] ccccbb=bbbd with [42] bbdd=bd:
Critical pair: ccccbd=bbbddd.
Reduce RHS:
| [55] | (bbbd)dd |
| [42] | ⇒ (bbdd) |
| ⇒ bd |
Referenced by [58].
Overlap of [4] cbcbcbc=d with [57] ccccbd=bd:
Critical pair: cbcbcbbd=dcccbd.
Flip LHS and RHS.
Referenced by [97].
Overlap of [56] ccccbc=bc with [4] cbcbcbc=d:
Critical pair: cccd=bcbcbc.
Flip LHS and RHS.
Referenced by [60], [61], [64], [65], [66], [68], [69], [103], [112], [115].
Overlap of [11] dbc=cbd with [59] bcbcbc=cccd:
Critical pair: dcccd=cbdbcbc.
Reduce RHS:
| [11] | cb(dbc)bc |
| [11] | ⇒ cbcb(dbc) |
| ⇒ cbcbcbd |
Referenced by [99].
Overlap of [49] bbbcbc=ccbb with [59] bcbcbc=cccd:
Critical pair: bbcccd=ccbbbc.
Referenced by [67].
Overlap of [54] cccbbb=bbbcb with [49] bbbcbc=ccbb:
Critical pair: cccccbb=bbbcbcbc.
Reduce LHS:
| [53] | c(ccccbb) |
| [55] | ⇒ c(bbbd) |
| ⇒ cbb |
Reduce RHS:
| [49] | (bbbcbc)bc |
| ⇒ ccbbbc |
Flip LHS and RHS.
Referenced by [67].
Overlap of [54] cccbbb=bbbcb with [55] bbbd=bb:
Critical pair: cccbb=bbbcbd.
Reduce RHS:
| [35] | b(bbcbd) |
| ⇒ bbbc |
Defines rule #13.
Referenced by [71], [73], [74].
Overlap of [4] cbcbcbc=d with [59] bcbcbc=cccd:
Critical pair: ccccd=d.
Simplify [40] daaa=cbcbcbbcbcbcbbcbcbcbb.
Reduce RHS:
| [51] | cbcbc(bbcbcbcbbc)bcbcbb |
| [47] | ⇒ (cbcbcbbb)bcdcbcbcbb |
| [49] | ⇒ d(bbbcbc)dcbcbcbb |
| [34] | ⇒ dcc(bbdc)bcbcbb |
| [59] | ⇒ dcc(bcbcbc)bb |
| [64] | ⇒ dc(ccccd)bb |
| ⇒ dcdbb |
Simplify [29] bba=bbcbcbcb.
Reduce RHS:
| [59] | b(bcbcbc)b |
| ⇒ bcccdb |
Overlap of [36] bbcccdb=bbccc with [61] bbcccd=ccbbbc:
Critical pair: ccbbbcb=bbccc.
Reduce LHS:
| [62] | (ccbbbc)b |
| ⇒ cbbb |
Flip LHS and RHS.
Referenced by [72], [75], [76], [87], [91].
Overlap of [46] bbcbcbcbbd=bbbbcdd with [59] bcbcbc=cccd:
Critical pair: bcccdbbd=bbbbcdd.
Referenced by [100].
Simplify [52] accbb=bbcbcbc.
Reduce RHS:
| [59] | b(bcbcbc) |
| ⇒ bcccd |
Referenced by [96].
Simplify [53] ccccbb=bbbd.
Reduce RHS:
| [55] | (bbbd) |
| ⇒ bb |
Referenced by [71].
Overlap of [70] ccccbb=bb with [63] cccbb=bbbc:
Critical pair: cbbbc=bb.
Defines rule #9.
Referenced by [72], [75], [76], [83], [95], [123].
Overlap of [20] bbcccc=bb with [71] cbbbc=bb:
Critical pair: bbcccbb=bbbbbc.
Reduce LHS:
| [67] | (bbccc)bb |
| ⇒ cbbbbb |
Flip LHS and RHS.
Defines rule #5.
Overlap of [63] cccbb=bbbc with [34] bbdc=bc:
Critical pair: cccbc=bbbcdc.
Referenced by [153].
Overlap of [63] cccbb=bbbc with [42] bbdd=bd:
Critical pair: cccbd=bbbcdd.
Overlap of [15] abb=bbc with [67] bbccc=cbbb:
Critical pair: acbbb=bbcccc.
Reduce RHS:
| [67] | (bbccc)c |
| [71] | ⇒ (cbbbc) |
| ⇒ bb |
Referenced by [77].
Overlap of [71] cbbbc=bb with [67] bbccc=cbbb:
Critical pair: cbcbbb=bbcc.
Flip LHS and RHS.
Defines rule #11.
Referenced by [87].
Overlap of [75] acbbb=bb with [55] bbbd=bb:
Critical pair: acbb=bbd.
Referenced by [78], [79], [80], [81], [86], [101].
Overlap of [77] acbb=bbd with [66] bba=bcccdb:
Critical pair: acbcccdb=bbda.
Flip LHS and RHS.
Referenced by [102].
Overlap of [77] acbb=bbd with [31] bbdb=bb:
Critical pair: acbb=bbddb.
Reduce LHS:
| [77] | (acbb) |
| ⇒ bbd |
Reduce RHS:
| [42] | (bbdd)b |
| ⇒ bdb |
Referenced by [80], [81], [82], [83], [84], [85], [86], [94], [97], [100], [101], [103], [107], [108], [109], [113], [123].
Overlap of [77] acbb=bbd with [34] bbdc=bc:
Critical pair: acbc=bbddc.
Reduce RHS:
| [79] | (bbd)dc |
| ⇒ bdbdc |
Overlap of [77] acbb=bbd with [42] bbdd=bd:
Critical pair: acbd=bbddd.
Reduce RHS:
| [79] | (bbd)dd |
| ⇒ bdbdd |
Overlap of [15] abb=bbc with [79] bbd=bdb:
Critical pair: abdb=bbcd.
Reduce LHS:
| [43] | (abd)b |
| ⇒ bbcddb |
Referenced by [136].
Overlap of [16] bacbb=cbbbc with [79] bbd=bdb:
Critical pair: bacbbdb=cbbbcbd.
Reduce LHS:
| [16] | (bacbb)db |
| [71] | ⇒ (cbbbc)db |
| [79] | ⇒ (bbd)b |
| ⇒ bdbb |
Reduce RHS:
| [71] | (cbbbc)bd |
| [55] | ⇒ (bbbd) |
| ⇒ bb |
Referenced by [87], [95], [100], [108].
Overlap of [34] bbdc=bc with [79] bbd=bdb:
Critical pair: bdbc=bc.
Reduce LHS:
| [11] | b(dbc) |
| ⇒ bcbd |
Referenced by [89], [90], [91], [94], [97], [111], [115].
Overlap of [42] bbdd=bd with [79] bbd=bdb:
Critical pair: bdbd=bd.
Referenced by [86], [102], [104], [105], [107], [109].
Overlap of [77] acbb=bbd with [79] bbd=bdb:
Critical pair: acbdb=bbdd.
Reduce LHS:
| [81] | (acbd)b |
| [85] | ⇒ (bdbd)db |
| ⇒ bddb |
Reduce RHS:
| [79] | (bbd)d |
| [85] | ⇒ (bdbd) |
| ⇒ bd |
Referenced by [88], [89], [90], [91], [92], [126].
Overlap of [83] bdbb=bb with [67] bbccc=cbbb:
Critical pair: bdcbbb=bbccc.
Reduce RHS:
| [76] | (bbcc)c |
| [32] | ⇒ c(bcbbbc) |
| ⇒ cbbb |
Referenced by [107].
Overlap of [43] abd=bbcdd with [86] bddb=bd:
Critical pair: abd=bbcdddb.
Reduce LHS:
| [43] | (abd) |
| ⇒ bbcdd |
Flip LHS and RHS.
Overlap of [86] bddb=bd with [33] bbcdb=bbc:
Critical pair: bddbbc=bdbcdb.
Reduce LHS:
| [86] | (bddb)bc |
| [11] | ⇒ b(dbc) |
| [84] | ⇒ (bcbd) |
| ⇒ bc |
Reduce RHS:
| [11] | b(dbc)db |
| [84] | ⇒ (bcbd)db |
| ⇒ bcdb |
Flip LHS and RHS.
Defines rule #4.
Overlap of [86] bddb=bd with [44] bbccdb=bbcc:
Critical pair: bddbbcc=bdbccdb.
Reduce LHS:
| [86] | (bddb)bcc |
| [11] | ⇒ b(dbc)c |
| [84] | ⇒ (bcbd)c |
| ⇒ bcc |
Reduce RHS:
| [11] | b(dbc)cdb |
| [84] | ⇒ (bcbd)cdb |
| ⇒ bccdb |
Flip LHS and RHS.
Defines rule #10.
Overlap of [86] bddb=bd with [67] bbccc=cbbb:
Critical pair: bddcbbb=bdbccc.
Reduce RHS:
| [11] | b(dbc)cc |
| [84] | ⇒ (bcbd)cc |
| ⇒ bccc |
Flip LHS and RHS.
Referenced by [93], [96], [100], [106].
Overlap of [86] bddb=bd with [86] bddb=bd:
Critical pair: bddbd=bdddb.
Reduce LHS:
| [86] | (bddb)d |
| ⇒ bdd |
Flip LHS and RHS.
Referenced by [127].
Simplify [66] bba=bcccdb.
Reduce RHS:
| [91] | (bccc)db |
| [55] | ⇒ bddc(bbbd)b |
| ⇒ bddcbbb |
Simplify [37] dba=cbcbcbbd.
Reduce RHS:
| [79] | cbcbc(bbd) |
| [84] | ⇒ cbc(bcbd)b |
| ⇒ cbcbcb |
Overlap of [48] cbdbbbc=dbbb with [83] bdbb=bb:
Critical pair: cbbbc=dbbb.
Reduce LHS:
| [71] | (cbbbc) |
| ⇒ bb |
Flip LHS and RHS.
Defines rule #1.
Referenced by [98], [107], [108], [112], [120], [122].
Simplify [69] accbb=bcccd.
Reduce RHS:
| [91] | (bccc)d |
| [55] | ⇒ bddc(bbbd) |
| ⇒ bddcbb |
Referenced by [122].
Simplify [58] dcccbd=cbcbcbbd.
Reduce RHS:
| [79] | cbcbc(bbd) |
| [84] | ⇒ cbc(bcbd)b |
| ⇒ cbcbcb |
Referenced by [98].
Overlap of [97] dcccbd=cbcbcb with [74] cccbd=bbbcdd:
Critical pair: dbbbcdd=cbcbcb.
Reduce LHS:
| [95] | (dbbb)cdd |
| ⇒ bbcdd |
Flip LHS and RHS.
Referenced by [99].
Simplify [60] dcccd=cbcbcbd.
Reduce RHS:
| [98] | (cbcbcb)d |
| ⇒ bbcddd |
Referenced by [102].
Overlap of [68] bcccdbbd=bbbbcdd with [79] bbd=bdb:
Critical pair: bcccdbdb=bbbbcdd.
Reduce LHS:
| [91] | (bccc)dbdb |
| [79] | ⇒ bddcb(bbd)bdb |
| [79] | ⇒ bddc(bbd)bbdb |
| [83] | ⇒ bddc(bdbb)bdb |
| [79] | ⇒ bddcb(bbd)b |
| [79] | ⇒ bddc(bbd)bb |
| [83] | ⇒ bddc(bdbb)b |
| ⇒ bddcbbb |
Simplify [77] acbb=bbd.
Reduce RHS:
| [79] | (bbd) |
| ⇒ bdb |
Referenced by [124].
Simplify [78] bbda=acbcccdb.
Reduce RHS:
| [80] | (acbc)ccdb |
| [85] | ⇒ (bdbd)cccdb |
| [99] | ⇒ b(dcccd)b |
| [88] | ⇒ b(bbcdddb) |
| ⇒ bbbcdd |
Referenced by [103].
Overlap of [102] bbda=bbbcdd with [79] bbd=bdb:
Critical pair: bdba=bbbcdd.
Reduce LHS:
| [94] | b(dba) |
| [59] | ⇒ (bcbcbc)b |
| ⇒ cccdb |
Referenced by [115].
Simplify [80] acbc=bdbdc.
Reduce RHS:
| [85] | (bdbd)c |
| ⇒ bdc |
Referenced by [125].
Simplify [81] acbd=bdbdd.
Reduce RHS:
| [85] | (bdbd)d |
| ⇒ bdd |
Simplify [91] bccc=bddcbbb.
Reduce RHS:
| [100] | (bddcbbb) |
| ⇒ bbbbcdd |
Defines rule #16.
Overlap of [95] dbbb=bb with [93] bba=bddcbbb:
Critical pair: dbbddcbbb=bba.
Reduce LHS:
| [79] | d(bbd)dcbbb |
| [85] | ⇒ d(bdbd)cbbb |
| [87] | ⇒ d(bdcbbb) |
| ⇒ dcbbb |
Reduce RHS:
| [93] | (bba) |
| [100] | ⇒ (bddcbbb) |
| ⇒ bbbbcdd |
Referenced by [120].
Overlap of [95] dbbb=bb with [79] bbd=bdb:
Critical pair: dbbdb=bbd.
Reduce LHS:
| [79] | d(bbd)b |
| [83] | ⇒ d(bdbb) |
| ⇒ dbb |
Reduce RHS:
| [79] | (bbd) |
| ⇒ bdb |
Flip LHS and RHS.
Referenced by [109], [110], [111], [112], [113], [120], [122], [123], [124].
Overlap of [85] bdbd=bd with [108] bdb=dbb:
Critical pair: dbbd=bd.
Reduce LHS:
| [79] | d(bbd) |
| [108] | ⇒ d(bdb) |
| ⇒ ddbb |
Referenced by [112], [113], [123].
Overlap of [108] bdb=dbb with [3] bababa=c:
Critical pair: bdc=dbbababa.
Reduce RHS:
| [3] | db(bababa) |
| [11] | ⇒ (dbc) |
| ⇒ cbd |
Referenced by [112], [116], [118], [120], [122], [125].
Overlap of [108] bdb=dbb with [11] dbc=cbd:
Critical pair: bcbd=dbbc.
Reduce LHS:
| [84] | (bcbd) |
| ⇒ bc |
Flip LHS and RHS.
Defines rule #8.
Referenced by [112], [144], [149].
Overlap of [109] ddbb=bd with [59] bcbcbc=cccd:
Critical pair: ddbcccd=bdcbcbc.
Reduce LHS:
| [11] | d(dbc)ccd |
| [110] | ⇒ dc(bdc)cd |
| [110] | ⇒ dcc(bdc)d |
| [74] | ⇒ d(cccbd)d |
| [95] | ⇒ (dbbb)cddd |
| ⇒ bbcddd |
Reduce RHS:
| [110] | (bdc)bcbc |
| [108] | ⇒ c(bdb)cbc |
| [111] | ⇒ c(dbbc)bc |
| ⇒ cbcbc |
Flip LHS and RHS.
Defines rule #15.
Overlap of [109] ddbb=bd with [79] bbd=bdb:
Critical pair: ddbdb=bdd.
Reduce LHS:
| [108] | dd(bdb) |
| [109] | ⇒ d(ddbb) |
| ⇒ dbd |
Flip LHS and RHS.
Referenced by [114], [116], [117], [119], [120], [122], [123], [126].
Overlap of [43] abd=bbcdd with [113] bdd=dbd:
Critical pair: adbd=bbcddd.
Referenced by [129].
Overlap of [59] bcbcbc=cccd with [84] bcbd=bc:
Critical pair: bcbcbc=cccdbd.
Reduce LHS:
| [59] | (bcbcbc) |
| ⇒ cccd |
Reduce RHS:
| [103] | (cccdb)d |
| ⇒ bbbcddd |
Defines rule #14.
Referenced by [123].
Overlap of [43] abd=bbcdd with [110] bdc=cbd:
Critical pair: acbd=bbcddc.
Reduce LHS:
| [105] | (acbd) |
| [113] | ⇒ (bdd) |
| ⇒ dbd |
Flip LHS and RHS.
Referenced by [130].
Simplify [105] acbd=bdd.
Reduce RHS:
| [113] | (bdd) |
| ⇒ dbd |
Overlap of [117] acbd=dbd with [110] bdc=cbd:
Critical pair: accbd=dbdc.
Reduce RHS:
| [110] | d(bdc) |
| ⇒ dcbd |
Referenced by [131].
Overlap of [117] acbd=dbd with [113] bdd=dbd:
Critical pair: acdbd=dbdd.
Reduce RHS:
| [113] | d(bdd) |
| ⇒ ddbd |
Referenced by [133].
Simplify [93] bba=bddcbbb.
Reduce RHS:
| [113] | (bdd)cbbb |
| [110] | ⇒ d(bdc)bbb |
| [108] | ⇒ dc(bdb)bb |
| [95] | ⇒ dc(dbbb)b |
| [107] | ⇒ (dcbbb) |
| ⇒ bbbbcdd |
Defines rule #27.
Simplify [94] dba=cbcbcb.
Reduce RHS:
| [112] | (cbcbc)b |
| [88] | ⇒ (bbcdddb) |
| ⇒ bbcdd |
Defines rule #29.
Referenced by [146], [147], [148], [149].
Simplify [96] accbb=bddcbb.
Reduce RHS:
| [113] | (bdd)cbb |
| [110] | ⇒ d(bdc)bb |
| [108] | ⇒ dc(bdb)b |
| [95] | ⇒ dc(dbbb) |
| ⇒ dcbb |
Referenced by [150].
Overlap of [64] ccccd=d with [115] cccd=bbbcddd:
Critical pair: cbbbcddd=d.
Reduce LHS:
| [71] | (cbbbc)ddd |
| [79] | ⇒ (bbd)dd |
| [108] | ⇒ (bdb)dd |
| [79] | ⇒ d(bbd)d |
| [108] | ⇒ d(bdb)d |
| [109] | ⇒ (ddbb)d |
| [113] | ⇒ (bdd) |
| ⇒ dbd |
Referenced by [126], [127], [128], [129], [130], [134].
Simplify [101] acbb=bdb.
Reduce RHS:
| [108] | (bdb) |
| ⇒ dbb |
Defines rule #20.
Simplify [104] acbc=bdc.
Reduce RHS:
| [110] | (bdc) |
| ⇒ cbd |
Referenced by [140].
Overlap of [86] bddb=bd with [113] bdd=dbd:
Critical pair: dbdb=bd.
Reduce LHS:
| [123] | (dbd)b |
| ⇒ db |
Flip LHS and RHS.
Defines rule #2.
Referenced by [127], [128], [131], [132], [135], [137], [140], [141], [144], [145].
Simplify [92] bdddb=bdd.
Reduce RHS:
| [126] | (bd)d |
| [123] | ⇒ (dbd) |
| ⇒ d |
Referenced by [128].
Overlap of [127] bdddb=d with [126] bd=db:
Critical pair: dbddb=d.
Reduce LHS:
| [123] | (dbd)db |
| ⇒ ddb |
Defines rule #3.
Referenced by [133], [135], [137], [139], [145], [146], [149], [150], [151].
Overlap of [114] adbd=bbcddd with [123] dbd=d:
Critical pair: ad=bbcddd.
Defines rule #19.
Referenced by [138].
Simplify [116] bbcddc=dbd.
Reduce RHS:
| [123] | (dbd) |
| ⇒ d |
Simplify [118] accbd=dcbd.
Reduce RHS:
| [126] | dc(bd) |
| ⇒ dcdb |
Referenced by [132].
Overlap of [131] accbd=dcdb with [126] bd=db:
Critical pair: accdb=dcdb.
Referenced by [142].
Simplify [119] acdbd=ddbd.
Reduce RHS:
| [128] | (ddb)d |
| ⇒ dd |
Referenced by [134].
Overlap of [133] acdbd=dd with [123] dbd=d:
Critical pair: acd=dd.
Defines rule #21.
Referenced by [138].
Overlap of [128] ddb=d with [11] dbc=cbd:
Critical pair: dcbd=dc.
Reduce LHS:
| [126] | dc(bd) |
| ⇒ dcdb |
Referenced by [136], [139], [142].
Overlap of [130] bbcddc=d with [8] caaa=babab:
Critical pair: bbcddbabab=daaa.
Reduce LHS:
| [82] | (bbcddb)abab |
| ⇒ bbcdabab |
Reduce RHS:
| [65] | (daaa) |
| [135] | ⇒ (dcdb)b |
| ⇒ dcb |
Referenced by [143].
Overlap of [128] ddb=d with [130] bbcddc=d:
Critical pair: ddd=dbcddc.
Reduce RHS:
| [11] | (dbc)ddc |
| [126] | ⇒ c(bd)ddc |
| [126] | ⇒ cd(bd)dc |
| [128] | ⇒ c(ddb)dc |
| ⇒ cddc |
Flip LHS and RHS.
Overlap of [134] acd=dd with [137] cddc=ddd:
Critical pair: addd=dddc.
Reduce LHS:
| [129] | (ad)dd |
| ⇒ bbcddddd |
Flip LHS and RHS.
Overlap of [137] cddc=ddd with [8] caaa=babab:
Critical pair: cddbabab=dddaaa.
Reduce LHS:
| [128] | c(ddb)abab |
| ⇒ cdabab |
Reduce RHS:
| [65] | dd(daaa) |
| [135] | ⇒ dd(dcdb)b |
| [138] | ⇒ (dddc)b |
| [128] | ⇒ bbcddd(ddb) |
| ⇒ bbcdddd |
Referenced by [143].
Simplify [125] acbc=cbd.
Reduce RHS:
| [126] | c(bd) |
| ⇒ cdb |
Defines rule #25.
Simplify [11] dbc=cbd.
Reduce RHS:
| [126] | c(bd) |
| ⇒ cdb |
Defines rule #7.
Simplify [132] accdb=dcdb.
Reduce RHS:
| [135] | (dcdb) |
| ⇒ dc |
Overlap of [136] bbcdabab=dcb with [139] cdabab=bbcdddd:
Critical pair: bbbbcdddd=dcb.
Flip LHS and RHS.
Overlap of [142] accdb=dc with [111] dbbc=bc:
Critical pair: accbc=dcbc.
Reduce RHS:
| [143] | (dcb)c |
| [138] | ⇒ bbbbcd(dddc) |
| [89] | ⇒ bbb(bcdb)bcddddd |
| [49] | ⇒ b(bbbcbc)ddddd |
| [126] | ⇒ bccb(bd)dddd |
| [126] | ⇒ bcc(bd)bdddd |
| [90] | ⇒ (bccdb)bdddd |
| [126] | ⇒ bcc(bd)ddd |
| [90] | ⇒ (bccdb)ddd |
| ⇒ bccddd |
Defines rule #26.
Overlap of [142] accdb=dc with [126] bd=db:
Critical pair: accddb=dcd.
Reduce LHS:
| [128] | acc(ddb) |
| ⇒ accd |
Referenced by [154].
Overlap of [121] dba=bbcdd with [3] bababa=c:
Critical pair: dc=bbcddbaba.
Reduce RHS:
| [128] | bbc(ddb)aba |
| ⇒ bbcdaba |
Flip LHS and RHS.
Referenced by [151].
Overlap of [89] bcdb=bc with [121] dba=bbcdd:
Critical pair: bcbbcdd=bca.
Flip LHS and RHS.
Defines rule #31.
Overlap of [90] bccdb=bcc with [121] dba=bbcdd:
Critical pair: bccbbcdd=bcca.
Flip LHS and RHS.
Defines rule #32.
Overlap of [128] ddb=d with [121] dba=bbcdd:
Critical pair: dbbcdd=da.
Reduce LHS:
| [111] | (dbbc)dd |
| ⇒ bcdd |
Flip LHS and RHS.
Defines rule #28.
Referenced by [151].
Simplify [122] accbb=dcbb.
Reduce RHS:
| [143] | (dcb)b |
| [128] | ⇒ bbbbcdd(ddb) |
| ⇒ bbbbcddd |
Defines rule #23.
Simplify [146] bbcdaba=dc.
Reduce LHS:
| [149] | bbc(da)ba |
| [128] | ⇒ bbcbc(ddb)a |
| [149] | ⇒ bbcbc(da) |
| [112] | ⇒ bb(cbcbc)dd |
| ⇒ bbbbcddddd |
Flip LHS and RHS.
Defines rule #6.
Referenced by [152], [153], [154].
Simplify [50] abc=bbcdc.
Reduce RHS:
| [151] | bbc(dc) |
| ⇒ bbcbbbbcddddd |
Defines rule #22.
Simplify [73] cccbc=bbbcdc.
Reduce RHS:
| [151] | bbbc(dc) |
| ⇒ bbbcbbbbcddddd |
Defines rule #17.
Simplify [145] accd=dcd.
Reduce RHS:
| [151] | (dc)d |
| ⇒ bbbbcdddddd |
Defines rule #24.