| Back: | ⟨a, b | aaaa=1, ababb=ba⟩ |
|---|
Completion settings:
Axiom: aaaa=1.
Defines rule #50.
Referenced by [8], [9], [12], [24], [29], [54], [105].
Axiom: ababb=ba.
Referenced by [6].
Axiom: abb=c.
Referenced by [6], [7], [8], [10], [11], [13], [14], [19], [35], [47], [49], [50], [52], [54], [62], [73].
Axiom: bbbb=d.
Referenced by [14], [15], [16], [30], [48].
Axiom: daa=e.
Referenced by [7], [9], [25], [27], [40], [66], [67], [72], [75], [76].
Overlap of [2] ababb=ba with [3] abb=c:
Critical pair: abc=ba.
Flip LHS and RHS.
Defines rule #47.
Referenced by [11], [12], [13], [16], [17], [23], [41], [47], [48], [54], [75], [85], [86].
Overlap of [5] daa=e with [3] abb=c:
Critical pair: dac=ebb.
Flip LHS and RHS.
Referenced by [53].
Overlap of [1] aaaa=1 with [3] abb=c:
Critical pair: aaac=bb.
Referenced by [54].
Overlap of [5] daa=e with [1] aaaa=1:
Critical pair: d=eaa.
Flip LHS and RHS.
Referenced by [10], [26], [42], [67], [72], [87], [93], [98], [104], [112].
Overlap of [9] eaa=d with [3] abb=c:
Critical pair: eac=dbb.
Flip LHS and RHS.
Referenced by [18].
Overlap of [3] abb=c with [6] ba=abc:
Critical pair: ababc=ca.
Reduce LHS:
| [6] | a(ba)bc |
| ⇒ aabcbc |
Referenced by [32].
Overlap of [6] ba=abc with [1] aaaa=1:
Critical pair: b=abcaaa.
Flip LHS and RHS.
Referenced by [33].
Overlap of [6] ba=abc with [3] abb=c:
Critical pair: bc=abcbb.
Flip LHS and RHS.
Referenced by [23].
Overlap of [3] abb=c with [4] bbbb=d:
Critical pair: ad=cbb.
Flip LHS and RHS.
Referenced by [21], [23], [51].
Overlap of [4] bbbb=d with [4] bbbb=d:
Critical pair: bd=db.
Flip LHS and RHS.
Defines rule #42.
Referenced by [17], [18], [20], [22], [26], [28], [31], [32], [36], [37], [42], [43], [47], [52], [53], [60], [61], [94], [106], [110], [125].
Overlap of [4] bbbb=d with [6] ba=abc:
Critical pair: bbbabc=da.
Reduce LHS:
| [6] | bb(ba)bc |
| [6] | ⇒ b(ba)bcbc |
| [6] | ⇒ (ba)bcbcbc |
| ⇒ abcbcbcbc |
Referenced by [55].
Overlap of [15] db=bd with [6] ba=abc:
Critical pair: dabc=bda.
Flip LHS and RHS.
Referenced by [34].
Simplify [10] dbb=eac.
Reduce LHS:
| [15] | (db)b |
| [15] | ⇒ b(db) |
| ⇒ bbd |
Referenced by [19], [20], [21], [22], [43], [53], [60], [61], [65], [74].
Overlap of [3] abb=c with [18] bbd=eac:
Critical pair: aeac=cd.
Referenced by [45], [85], [86], [91].
Overlap of [18] bbd=eac with [15] db=bd:
Critical pair: bbbd=eacb.
Reduce LHS:
| [18] | b(bbd) |
| ⇒ beac |
Overlap of [14] cbb=ad with [18] bbd=eac:
Critical pair: ceac=add.
Referenced by [51], [55], [64], [87], [91], [92], [93], [95], [97].
Overlap of [15] db=bd with [18] bbd=eac:
Critical pair: deac=bdbd.
Reduce RHS:
| [15] | b(db)d |
| [18] | ⇒ (bbd)d |
| ⇒ eacd |
Referenced by [51], [64], [88].
Overlap of [13] abcbb=bc with [14] cbb=ad:
Critical pair: abad=bc.
Reduce LHS:
| [6] | a(ba)d |
| ⇒ aabcd |
Referenced by [24], [25], [26], [27], [28].
Overlap of [1] aaaa=1 with [23] aabcd=bc:
Critical pair: aabc=bcd.
Referenced by [27], [28], [29], [32], [44], [47], [52].
Overlap of [5] daa=e with [23] aabcd=bc:
Critical pair: dabc=eabcd.
Referenced by [34].
Overlap of [9] eaa=d with [23] aabcd=bc:
Critical pair: ebc=dbcd.
Reduce RHS:
| [15] | (db)cd |
| ⇒ bdcd |
Referenced by [37], [53], [89], [94].
Overlap of [23] aabcd=bc with [5] daa=e:
Critical pair: aabce=bcaa.
Reduce LHS:
| [24] | (aabc)e |
| ⇒ bcde |
Flip LHS and RHS.
Referenced by [33].
Overlap of [23] aabcd=bc with [15] db=bd:
Critical pair: aabcbd=bcb.
Reduce LHS:
| [24] | (aabc)bd |
| [15] | ⇒ bc(db)d |
| ⇒ bcbdd |
Referenced by [57].
Overlap of [1] aaaa=1 with [24] aabc=bcd:
Critical pair: aabcd=bc.
Reduce LHS:
| [24] | (aabc)d |
| ⇒ bcdd |
Overlap of [4] bbbb=d with [29] bcdd=bc:
Critical pair: bbbbc=dcdd.
Reduce LHS:
| [4] | (bbbb)c |
| ⇒ dc |
Flip LHS and RHS.
Overlap of [30] dcdd=dc with [15] db=bd:
Critical pair: dcdbd=dcb.
Reduce LHS:
| [15] | dc(db)d |
| ⇒ dcbdd |
Referenced by [37].
Overlap of [11] aabcbc=ca with [24] aabc=bcd:
Critical pair: bcdbc=ca.
Reduce LHS:
| [15] | bc(db)c |
| ⇒ bcbdc |
Referenced by [35], [36], [37], [38], [39], [43].
Overlap of [12] abcaaa=b with [27] bcaa=bcde:
Critical pair: abcdea=b.
Referenced by [41], [42], [43], [44], [45], [46], [50], [71], [87].
Simplify [17] bda=dabc.
Reduce RHS:
| [25] | (dabc) |
| ⇒ eabcd |
Overlap of [3] abb=c with [32] bcbdc=ca:
Critical pair: abca=ccbdc.
Referenced by [59].
Overlap of [15] db=bd with [32] bcbdc=ca:
Critical pair: dca=bdcbdc.
Flip LHS and RHS.
Referenced by [60].
Overlap of [26] ebc=bdcd with [32] bcbdc=ca:
Critical pair: eca=bdcdbdc.
Reduce RHS:
| [15] | bdc(db)dc |
| [31] | ⇒ b(dcbdd)c |
| ⇒ bdcbc |
Flip LHS and RHS.
Referenced by [61].
Overlap of [32] bcbdc=ca with [30] dcdd=dc:
Critical pair: bcbdc=cadd.
Reduce LHS:
| [32] | (bcbdc) |
| ⇒ ca |
Flip LHS and RHS.
Referenced by [39], [40], [51], [64], [65], [92].
Overlap of [32] bcbdc=ca with [38] cadd=ca:
Critical pair: bcbdca=caadd.
Reduce LHS:
| [32] | (bcbdc)a |
| ⇒ caa |
Flip LHS and RHS.
Referenced by [64].
Overlap of [38] cadd=ca with [5] daa=e:
Critical pair: cade=caaa.
Flip LHS and RHS.
Referenced by [79].
Overlap of [6] ba=abc with [33] abcdea=b:
Critical pair: bb=abcbcdea.
Flip LHS and RHS.
Referenced by [62].
Overlap of [9] eaa=d with [33] abcdea=b:
Critical pair: eab=dbcdea.
Reduce RHS:
| [15] | (db)cdea |
| ⇒ bdcdea |
Flip LHS and RHS.
Referenced by [80].
Overlap of [34] bda=eabcd with [33] abcdea=b:
Critical pair: bdb=eabcdbcdea.
Reduce LHS:
| [15] | b(db) |
| [18] | ⇒ (bbd) |
| ⇒ eac |
Reduce RHS:
| [15] | eabc(db)cdea |
| [32] | ⇒ ea(bcbdc)dea |
| ⇒ eacadea |
Flip LHS and RHS.
Referenced by [98].
Overlap of [24] aabc=bcd with [33] abcdea=b:
Critical pair: ab=bcddea.
Reduce RHS:
| [29] | (bcdd)ea |
| ⇒ bcea |
Flip LHS and RHS.
Referenced by [47], [48], [49], [50].
Overlap of [33] abcdea=b with [19] aeac=cd:
Critical pair: abcdecd=beac.
Reduce RHS:
| [20] | (beac) |
| ⇒ eacb |
Flip LHS and RHS.
Referenced by [63].
Overlap of [33] abcdea=b with [33] abcdea=b:
Critical pair: abcdeb=bbcdea.
Flip LHS and RHS.
Referenced by [64].
Overlap of [3] abb=c with [44] bcea=ab:
Critical pair: abab=ccea.
Reduce LHS:
| [6] | a(ba)b |
| [24] | ⇒ (aabc)b |
| [15] | ⇒ bc(db) |
| ⇒ bcbd |
Overlap of [4] bbbb=d with [44] bcea=ab:
Critical pair: bbbab=dcea.
Reduce LHS:
| [6] | bb(ba)b |
| [6] | ⇒ b(ba)bcb |
| [6] | ⇒ (ba)bcbcb |
| ⇒ abcbcbcb |
Referenced by [55].
Overlap of [44] bcea=ab with [3] abb=c:
Critical pair: bcec=abbb.
Reduce RHS:
| [3] | (abb)b |
| ⇒ cb |
Flip LHS and RHS.
Defines rule #43.
Referenced by [51], [52], [53], [54], [56], [57], [59], [60], [61], [62], [63], [85], [86], [94].
Overlap of [44] bcea=ab with [33] abcdea=b:
Critical pair: bceb=abbcdea.
Reduce RHS:
| [3] | (abb)cdea |
| ⇒ ccdea |
Referenced by [51].
Overlap of [14] cbb=ad with [49] cb=bcec:
Critical pair: bcecb=ad.
Reduce LHS:
| [49] | bce(cb) |
| [50] | ⇒ (bceb)cec |
| [22] | ⇒ cc(deac)ec |
| [21] | ⇒ c(ceac)dec |
| [38] | ⇒ (cadd)dec |
| ⇒ cadec |
Referenced by [54].
Overlap of [24] aabc=bcd with [49] cb=bcec:
Critical pair: aabbcec=bcdb.
Reduce LHS:
| [3] | a(abb)cec |
| ⇒ accec |
Reduce RHS:
| [15] | bc(db) |
| [47] | ⇒ (bcbd) |
| ⇒ ccea |
Flip LHS and RHS.
Referenced by [58], [64], [91], [92], [95].
Overlap of [26] ebc=bdcd with [49] cb=bcec:
Critical pair: ebbcec=bdcdb.
Reduce LHS:
| [7] | (ebb)cec |
| ⇒ daccec |
Reduce RHS:
| [15] | bdc(db) |
| [49] | ⇒ bd(cb)d |
| [15] | ⇒ b(db)cecd |
| [18] | ⇒ (bbd)cecd |
| ⇒ eaccecd |
Referenced by [81].
Overlap of [8] aaac=bb with [51] cadec=ad:
Critical pair: aaaad=bbadec.
Reduce LHS:
| [1] | (aaaa)d |
| ⇒ d |
Reduce RHS:
| [6] | b(ba)dec |
| [6] | ⇒ (ba)bcdec |
| [49] | ⇒ ab(cb)cdec |
| [3] | ⇒ (abb)ceccdec |
| ⇒ cceccdec |
Flip LHS and RHS.
Defines rule #22.
Referenced by [85], [88], [89], [90], [93], [96], [111], [115], [132], [133], [139], [143], [149].
Overlap of [16] abcbcbcbc=da with [48] abcbcbcb=dcea:
Critical pair: dceac=da.
Reduce LHS:
| [21] | d(ceac) |
| ⇒ dadd |
Referenced by [65], [66], [68].
Simplify [20] beac=eacb.
Reduce RHS:
| [49] | ea(cb) |
| ⇒ eabcec |
Referenced by [77].
Simplify [28] bcbdd=bcb.
Reduce RHS:
| [49] | b(cb) |
| ⇒ bbcec |
Referenced by [58].
Overlap of [57] bcbdd=bbcec with [47] bcbd=ccea:
Critical pair: ccead=bbcec.
Reduce LHS:
| [52] | (ccea)d |
| ⇒ accecd |
Flip LHS and RHS.
Referenced by [82].
Simplify [35] abca=ccbdc.
Reduce RHS:
| [49] | c(cb)dc |
| [49] | ⇒ (cb)cecdc |
| ⇒ bceccecdc |
Overlap of [36] bdcbdc=dca with [49] cb=bcec:
Critical pair: bdbcecdc=dca.
Reduce LHS:
| [15] | b(db)cecdc |
| [18] | ⇒ (bbd)cecdc |
| ⇒ eaccecdc |
Flip LHS and RHS.
Overlap of [37] bdcbc=eca with [49] cb=bcec:
Critical pair: bdbcecc=eca.
Reduce LHS:
| [15] | b(db)cecc |
| [18] | ⇒ (bbd)cecc |
| ⇒ eaccecc |
Flip LHS and RHS.
Referenced by [64], [95], [97].
Overlap of [41] abcbcdea=bb with [49] cb=bcec:
Critical pair: abbceccdea=bb.
Reduce LHS:
| [3] | (abb)ceccdea |
| ⇒ cceccdea |
Flip LHS and RHS.
Referenced by [64], [74], [82], [83].
Overlap of [45] eacb=abcdecd with [49] cb=bcec:
Critical pair: eabcec=abcdecd.
Referenced by [77].
Overlap of [46] bbcdea=abcdeb with [62] bb=cceccdea:
Critical pair: cceccdeacdea=abcdeb.
Reduce LHS:
| [22] | ccecc(deac)dea |
| [21] | ⇒ ccec(ceac)ddea |
| [38] | ⇒ cce(cadd)ddea |
| [38] | ⇒ cce(cadd)ea |
| [61] | ⇒ cc(eca)ea |
| [21] | ⇒ c(ceac)ceccea |
| [38] | ⇒ (cadd)ceccea |
| [52] | ⇒ cace(ccea) |
| [21] | ⇒ ca(ceac)cec |
| [39] | ⇒ (caadd)cec |
| ⇒ caacec |
Flip LHS and RHS.
Referenced by [84].
Overlap of [18] bbd=eac with [55] dadd=da:
Critical pair: bbda=eacadd.
Reduce LHS:
| [34] | b(bda) |
| ⇒ beabcd |
Reduce RHS:
| [38] | ea(cadd) |
| ⇒ eaca |
Referenced by [85].
Overlap of [55] dadd=da with [55] dadd=da:
Critical pair: dadda=daadd.
Reduce LHS:
| [55] | (dadd)a |
| [5] | ⇒ (daa) |
| ⇒ e |
Reduce RHS:
| [5] | (daa)dd |
| ⇒ edd |
Flip LHS and RHS.
Defines rule #2.
Referenced by [67], [68], [69], [70], [117], [124], [126], [129], [136], [137], [144], [150], [155], [158], [162], [165], [167], [168], [177].
Overlap of [66] edd=e with [5] daa=e:
Critical pair: ede=eaa.
Reduce RHS:
| [9] | (eaa) |
| ⇒ d |
Defines rule #1.
Referenced by [69], [70], [95], [96], [97], [98], [114], [116], [118], [120], [122], [123], [129], [130], [131], [134], [138], [140], [142], [144], [149], [151], [155], [157], [165], [168], [169], [170], [171], [174], [175], [176], [177].
Overlap of [66] edd=e with [55] dadd=da:
Critical pair: edda=eadd.
Reduce LHS:
| [66] | (edd)a |
| ⇒ ea |
Flip LHS and RHS.
Referenced by [71], [72], [91], [117].
Overlap of [67] ede=d with [66] edd=e:
Critical pair: ede=ddd.
Reduce LHS:
| [67] | (ede) |
| ⇒ d |
Flip LHS and RHS.
Defines rule #4.
Overlap of [67] ede=d with [67] ede=d:
Critical pair: edd=dde.
Reduce LHS:
| [66] | (edd) |
| ⇒ e |
Flip LHS and RHS.
Defines rule #3.
Referenced by [108], [125], [129], [132], [139], [141], [143].
Overlap of [33] abcdea=b with [68] eadd=ea:
Critical pair: abcdea=bdd.
Reduce LHS:
| [33] | (abcdea) |
| ⇒ b |
Flip LHS and RHS.
Defines rule #40.
Referenced by [73], [74], [75], [106], [110].
Overlap of [68] eadd=ea with [5] daa=e:
Critical pair: eade=eaaa.
Reduce RHS:
| [9] | (eaa)a |
| ⇒ da |
Flip LHS and RHS.
Referenced by [81], [93], [95], [97], [101], [112], [118].
Overlap of [3] abb=c with [71] bdd=b:
Critical pair: abb=cdd.
Reduce LHS:
| [3] | (abb) |
| ⇒ c |
Flip LHS and RHS.
Defines rule #5.
Referenced by [76], [85], [86], [93], [95], [96], [99], [116], [118], [120], [122], [123], [129], [130], [131], [134], [142], [149], [154], [161], [163], [166], [169], [170], [171], [173], [174], [175], [176].
Overlap of [18] bbd=eac with [71] bdd=b:
Critical pair: bb=eacd.
Reduce LHS:
| [62] | (bb) |
| ⇒ cceccdea |
Overlap of [71] bdd=b with [5] daa=e:
Critical pair: bde=baa.
Reduce RHS:
| [6] | (ba)a |
| [59] | ⇒ (abca) |
| ⇒ bceccecdc |
Flip LHS and RHS.
Referenced by [78].
Overlap of [73] cdd=c with [5] daa=e:
Critical pair: cde=caa.
Flip LHS and RHS.
Simplify [56] beac=eabcec.
Reduce RHS:
| [63] | (eabcec) |
| ⇒ abcdecd |
Referenced by [80].
Simplify [59] abca=bceccecdc.
Reduce RHS:
| [75] | (bceccecdc) |
| ⇒ bde |
Overlap of [40] caaa=cade with [76] caa=cde:
Critical pair: cdea=cade.
Referenced by [80].
Overlap of [42] bdcdea=eab with [79] cdea=cade:
Critical pair: bdcade=eab.
Reduce LHS:
| [60] | b(dca)de |
| [77] | ⇒ (beac)cecdcde |
| ⇒ abcdecdcecdcde |
Flip LHS and RHS.
Referenced by [85].
Overlap of [53] daccec=eaccecd with [72] da=eade:
Critical pair: eadeccec=eaccecd.
Overlap of [58] bbcec=accecd with [62] bb=cceccdea:
Critical pair: cceccdeacec=accecd.
Reduce LHS:
| [74] | (cceccdea)cec |
| ⇒ eacdcec |
Referenced by [88].
Simplify [62] bb=cceccdea.
Reduce RHS:
| [74] | (cceccdea) |
| ⇒ eacd |
Referenced by [85], [86], [87], [99].
Simplify [64] abcdeb=caacec.
Reduce RHS:
| [76] | (caa)cec |
| ⇒ cdecec |
Referenced by [87].
Overlap of [65] beabcd=eaca with [80] eab=abcdecdcecdcde:
Critical pair: babcdecdcecdcdecd=eaca.
Reduce LHS:
| [6] | (ba)bcdecdcecdcdecd |
| [49] | ⇒ ab(cb)cdecdcecdcdecd |
| [83] | ⇒ a(bb)ceccdecdcecdcdecd |
| [19] | ⇒ (aeac)dceccdecdcecdcdecd |
| [73] | ⇒ (cdd)ceccdecdcecdcdecd |
| [54] | ⇒ (cceccdec)dcecdcdecd |
| ⇒ ddcecdcdecd |
Flip LHS and RHS.
Referenced by [100].
Overlap of [6] ba=abc with [78] abca=bde:
Critical pair: bbde=abcbca.
Reduce LHS:
| [83] | (bb)de |
| [73] | ⇒ ea(cdd)e |
| ⇒ eace |
Reduce RHS:
| [49] | ab(cb)ca |
| [83] | ⇒ a(bb)cecca |
| [19] | ⇒ (aeac)dcecca |
| [73] | ⇒ (cdd)cecca |
| ⇒ ccecca |
Flip LHS and RHS.
Referenced by [98].
Overlap of [33] abcdea=b with [78] abca=bde:
Critical pair: abcdebde=bbca.
Reduce LHS:
| [84] | (abcdeb)de |
| ⇒ cdececde |
Reduce RHS:
| [83] | (bb)ca |
| [60] | ⇒ eac(dca) |
| [21] | ⇒ ea(ceac)cecdc |
| [9] | ⇒ (eaa)ddcecdc |
| [69] | ⇒ (ddd)cecdc |
| ⇒ dcecdc |
Flip LHS and RHS.
Defines rule #12.
Referenced by [127], [128], [129], [134], [145].
Overlap of [22] deac=eacd with [54] cceccdec=d:
Critical pair: dead=eacdceccdec.
Reduce RHS:
| [82] | (eacdcec)cdec |
| ⇒ accecdcdec |
Referenced by [93].
Overlap of [26] ebc=bdcd with [54] cceccdec=d:
Critical pair: ebd=bdcdceccdec.
Referenced by [102].
Overlap of [54] cceccdec=d with [54] cceccdec=d:
Critical pair: cceccded=dceccdec.
Flip LHS and RHS.
Referenced by [102], [111], [134].
Overlap of [52] ccea=accec with [19] aeac=cd:
Critical pair: ccecd=acceceac.
Reduce RHS:
| [21] | acce(ceac) |
| [68] | ⇒ acc(eadd) |
| [52] | ⇒ a(ccea) |
| ⇒ aaccec |
Flip LHS and RHS.
Overlap of [52] ccea=accec with [21] ceac=add:
Critical pair: cadd=accecc.
Reduce LHS:
| [38] | (cadd) |
| ⇒ ca |
Defines rule #39.
Referenced by [93], [95], [97], [98], [112].
Overlap of [21] ceac=add with [92] ca=accecc:
Critical pair: ceaaccecc=adda.
Reduce LHS:
| [9] | c(eaa)ccecc |
| ⇒ cdccecc |
Reduce RHS:
| [72] | ad(da) |
| [88] | ⇒ a(dead)e |
| [91] | ⇒ (aaccec)dcdece |
| [73] | ⇒ cce(cdd)cdece |
| [54] | ⇒ (cceccdec)e |
| ⇒ de |
Referenced by [94], [95], [96], [97], [116], [119].
Overlap of [93] cdccecc=de with [49] cb=bcec:
Critical pair: cdccecbcec=deb.
Reduce LHS:
| [49] | cdcce(cb)cec |
| [26] | ⇒ cdcc(ebc)eccec |
| [49] | ⇒ cdc(cb)dcdeccec |
| [49] | ⇒ cd(cb)cecdcdeccec |
| [15] | ⇒ c(db)ceccecdcdeccec |
| [49] | ⇒ (cb)dceccecdcdeccec |
| ⇒ bcecdceccecdcdeccec |
Flip LHS and RHS.
Overlap of [93] cdccecc=de with [52] ccea=accec:
Critical pair: cdccecaccec=decea.
Reduce LHS:
| [61] | cdcc(eca)ccec |
| [21] | ⇒ cdc(ceac)ceccccec |
| [92] | ⇒ cd(ca)ddceccccec |
| [73] | ⇒ cdaccec(cdd)ceccccec |
| [72] | ⇒ c(da)cceccceccccec |
| [81] | ⇒ c(eadeccec)cceccccec |
| [21] | ⇒ (ceac)cecdcceccccec |
| [93] | ⇒ addce(cdccecc)ccec |
| [67] | ⇒ addc(ede)ccec |
| ⇒ addcdccec |
Flip LHS and RHS.
Overlap of [93] cdccecc=de with [54] cceccdec=d:
Critical pair: cdd=dedec.
Reduce LHS:
| [73] | (cdd) |
| ⇒ c |
Reduce RHS:
| [67] | d(ede)c |
| ⇒ ddc |
Flip LHS and RHS.
Defines rule #6.
Referenced by [97], [100], [101], [103], [109], [128], [146].
Overlap of [93] cdccecc=de with [92] ca=accecc:
Critical pair: cdccecaccecc=dea.
Reduce LHS:
| [61] | cdcc(eca)ccecc |
| [21] | ⇒ cdc(ceac)ceccccecc |
| [96] | ⇒ cdca(ddc)eccccecc |
| [92] | ⇒ cd(ca)ceccccecc |
| [72] | ⇒ c(da)cceccceccccecc |
| [81] | ⇒ c(eadeccec)cceccccecc |
| [21] | ⇒ (ceac)cecdcceccccecc |
| [96] | ⇒ a(ddc)ecdcceccccecc |
| [93] | ⇒ ace(cdccecc)ccecc |
| [67] | ⇒ ac(ede)ccecc |
| [93] | ⇒ a(cdccecc) |
| ⇒ ade |
Flip LHS and RHS.
Overlap of [43] eacadea=eac with [97] dea=ade:
Critical pair: eacaade=eac.
Reduce LHS:
| [92] | ea(ca)ade |
| [9] | ⇒ (eaa)cceccade |
| [86] | ⇒ d(ccecca)de |
| [97] | ⇒ (dea)cede |
| [67] | ⇒ adec(ede) |
| ⇒ adecd |
Flip LHS and RHS.
Referenced by [99], [101], [111], [112].
Simplify [83] bb=eacd.
Reduce RHS:
| [98] | (eac)d |
| [73] | ⇒ ade(cdd) |
| ⇒ adec |
Defines rule #48.
Simplify [85] eaca=ddcecdcdecd.
Reduce RHS:
| [96] | (ddc)ecdcdecd |
| ⇒ cecdcdecd |
Referenced by [101].
Overlap of [100] eaca=cecdcdecd with [98] eac=adecd:
Critical pair: adecda=cecdcdecd.
Reduce LHS:
| [72] | adec(da) |
| [95] | ⇒ a(decea)de |
| [96] | ⇒ aa(ddc)dccecde |
| ⇒ aacdccecde |
Referenced by [121].
Simplify [89] ebd=bdcdceccdec.
Reduce RHS:
| [90] | bdc(dceccdec) |
| ⇒ bdccceccded |
Referenced by [110].
Simplify [95] decea=addcdccec.
Reduce RHS:
| [96] | a(ddc)dccec |
| ⇒ acdccec |
Referenced by [112].
Overlap of [97] dea=ade with [9] eaa=d:
Critical pair: dd=adea.
Reduce RHS:
| [97] | a(dea) |
| ⇒ aade |
Flip LHS and RHS.
Referenced by [105].
Overlap of [1] aaaa=1 with [104] aade=dd:
Critical pair: aadd=de.
Referenced by [106], [107], [108], [109].
Overlap of [105] aadd=de with [15] db=bd:
Critical pair: aadbd=deb.
Reduce LHS:
| [15] | aa(db)d |
| [71] | ⇒ aa(bdd) |
| ⇒ aab |
Reduce RHS:
| [94] | (deb) |
| ⇒ bcecdceccecdcdeccec |
Overlap of [105] aadd=de with [69] ddd=d:
Critical pair: aad=ded.
Defines rule #45.
Referenced by [110].
Overlap of [105] aadd=de with [70] dde=e:
Critical pair: aae=dee.
Defines rule #44.
Overlap of [105] aadd=de with [96] ddc=c:
Critical pair: aac=dec.
Defines rule #46.
Referenced by [112], [113], [121].
Overlap of [107] aad=ded with [15] db=bd:
Critical pair: aabd=dedb.
Reduce LHS:
| [106] | (aab)d |
| ⇒ bcecdceccecdcdeccecd |
Reduce RHS:
| [15] | de(db) |
| [102] | ⇒ d(ebd) |
| [15] | ⇒ (db)dccceccded |
| [71] | ⇒ (bdd)ccceccded |
| ⇒ bccceccded |
Referenced by [123].
Overlap of [98] eac=adecd with [54] cceccdec=d:
Critical pair: ead=adecdceccdec.
Reduce RHS:
| [90] | adec(dceccdec) |
| ⇒ adeccceccded |
Referenced by [117].
Overlap of [98] eac=adecd with [92] ca=accecc:
Critical pair: eaaccecc=adecda.
Reduce LHS:
| [9] | (eaa)ccecc |
| ⇒ dccecc |
Reduce RHS:
| [72] | adec(da) |
| [103] | ⇒ a(decea)de |
| [109] | ⇒ (aac)dccecde |
| ⇒ decdccecde |
Flip LHS and RHS.
Referenced by [121].
Simplify [91] aaccec=ccecd.
Reduce LHS:
| [109] | (aac)cec |
| ⇒ deccec |
Defines rule #14.
Referenced by [114], [115], [116], [135], [156], [160].
Overlap of [67] ede=d with [113] deccec=ccecd:
Critical pair: eccecd=dccec.
Flip LHS and RHS.
Defines rule #10.
Referenced by [119], [120], [121], [122], [123], [127], [158], [162], [167].
Overlap of [113] deccec=ccecd with [54] cceccdec=d:
Critical pair: ded=ccecdcdec.
Flip LHS and RHS.
Referenced by [129].
Overlap of [113] deccec=ccecd with [93] cdccecc=de:
Critical pair: deccede=ccecddccecc.
Reduce LHS:
| [67] | decc(ede) |
| ⇒ deccd |
Reduce RHS:
| [73] | cce(cdd)ccecc |
| ⇒ ccecccecc |
Flip LHS and RHS.
Defines rule #32.
Overlap of [68] eadd=ea with [111] ead=adeccceccded:
Critical pair: adeccceccdedd=ea.
Reduce LHS:
| [66] | adeccceccd(edd) |
| ⇒ adeccceccde |
Flip LHS and RHS.
Simplify [72] da=eade.
Reduce RHS:
| [117] | (ea)de |
| [67] | ⇒ adeccceccd(ede) |
| [73] | ⇒ adecccec(cdd) |
| ⇒ adecccecc |
Referenced by [172].
Overlap of [93] cdccecc=de with [114] dccec=eccecd:
Critical pair: ceccecdc=de.
Referenced by [120], [122], [123].
Simplify [94] deb=bcecdceccecdcdeccec.
Reduce RHS:
| [119] | bcecd(ceccecdc)deccec |
| [73] | ⇒ bce(cdd)edeccec |
| [67] | ⇒ bcec(ede)ccec |
| [114] | ⇒ bcec(dccec) |
| ⇒ bcececcecd |
Referenced by [124].
Overlap of [101] aacdccecde=cecdcdecd with [109] aac=dec:
Critical pair: decdccecde=cecdcdecd.
Reduce LHS:
| [112] | (decdccecde) |
| [114] | ⇒ (dccec)c |
| ⇒ eccecdc |
Simplify [106] aab=bcecdceccecdcdeccec.
Reduce RHS:
| [119] | bcecd(ceccecdc)deccec |
| [73] | ⇒ bce(cdd)edeccec |
| [67] | ⇒ bcec(ede)ccec |
| [114] | ⇒ bcec(dccec) |
| ⇒ bcececcecd |
Referenced by [126].
Overlap of [110] bcecdceccecdcdeccecd=bccceccded with [119] ceccecdc=de:
Critical pair: bcecddedeccecd=bccceccded.
Reduce LHS:
| [73] | bce(cdd)edeccecd |
| [67] | ⇒ bcec(ede)ccecd |
| [114] | ⇒ bcec(dccec)d |
| [73] | ⇒ bcececce(cdd) |
| ⇒ bcececcec |
Simplify [120] deb=bcececcecd.
Reduce RHS:
| [123] | (bcececcec)d |
| [66] | ⇒ bccceccd(edd) |
| ⇒ bccceccde |
Referenced by [125].
Overlap of [70] dde=e with [124] deb=bccceccde:
Critical pair: dbccceccde=eb.
Reduce LHS:
| [15] | (db)ccceccde |
| ⇒ bdccceccde |
Flip LHS and RHS.
Referenced by [153].
Simplify [122] aab=bcececcecd.
Reduce RHS:
| [123] | (bcececcec)d |
| [66] | ⇒ bccceccd(edd) |
| ⇒ bccceccde |
Defines rule #49.
Overlap of [87] dcecdc=cdececde with [114] dccec=eccecd:
Critical pair: dcececcecd=cdececdecec.
Referenced by [137].
Overlap of [96] ddc=c with [87] dcecdc=cdececde:
Critical pair: dcdececde=cecdc.
Overlap of [87] dcecdc=cdececde with [128] dcdececde=cecdc:
Critical pair: dceccecdc=cdececdedececde.
Reduce LHS:
| [121] | dc(eccecdc) |
| [115] | ⇒ d(ccecdcdec)d |
| [70] | ⇒ (dde)dd |
| [66] | ⇒ (edd) |
| ⇒ e |
Reduce RHS:
| [67] | cdececd(ede)cecde |
| [73] | ⇒ cdece(cdd)cecde |
| ⇒ cdececcecde |
Flip LHS and RHS.
Referenced by [131].
Overlap of [128] dcdececde=cecdc with [67] ede=d:
Critical pair: dcdececdd=cecdcde.
Reduce LHS:
| [73] | dcdece(cdd) |
| ⇒ dcdecec |
Referenced by [138].
Overlap of [129] cdececcecde=e with [67] ede=d:
Critical pair: cdececcecdd=ede.
Reduce LHS:
| [73] | cdececce(cdd) |
| ⇒ cdececcec |
Reduce RHS:
| [67] | (ede) |
| ⇒ d |
Overlap of [54] cceccdec=d with [131] cdececcec=d:
Critical pair: cceccded=ddececcec.
Reduce RHS:
| [70] | (dde)ceccec |
| ⇒ ececcec |
Flip LHS and RHS.
Defines rule #18.
Referenced by [137], [149], [158], [160], [162], [167], [169].
Overlap of [131] cdececcec=d with [54] cceccdec=d:
Critical pair: cdeced=dcdec.
Flip LHS and RHS.
Defines rule #7.
Referenced by [134], [135], [136], [138], [142].
Overlap of [87] dcecdc=cdececde with [133] dcdec=cdeced:
Critical pair: dceccdeced=cdececdedec.
Reduce LHS:
| [90] | (dceccdec)ed |
| [67] | ⇒ cceccd(ede)d |
| [73] | ⇒ ccec(cdd)d |
| ⇒ cceccd |
Reduce RHS:
| [67] | cdececd(ede)c |
| [73] | ⇒ cdece(cdd)c |
| ⇒ cdececc |
Flip LHS and RHS.
Overlap of [133] dcdec=cdeced with [113] deccec=ccecd:
Critical pair: dcccecd=cdecedcec.
Simplify [121] eccecdc=cecdcdecd.
Reduce RHS:
| [133] | cec(dcdec)d |
| [66] | ⇒ ceccdec(edd) |
| ⇒ ceccdece |
Defines rule #17.
Overlap of [127] dcececcecd=cdececdecec with [132] ececcec=cceccded:
Critical pair: dccceccdedd=cdececdecec.
Reduce LHS:
| [66] | dccceccd(edd) |
| ⇒ dccceccde |
Referenced by [153].
Overlap of [130] dcdecec=cecdcde with [133] dcdec=cdeced:
Critical pair: cdecedec=cecdcde.
Reduce LHS:
| [67] | cdec(ede)c |
| ⇒ cdecdc |
Referenced by [139].
Overlap of [54] cceccdec=d with [138] cdecdc=cecdcde:
Critical pair: cceccdececdcde=ddecdc.
Reduce LHS:
| [54] | (cceccdec)ecdcde |
| ⇒ decdcde |
Reduce RHS:
| [70] | (dde)cdc |
| ⇒ ecdc |
Overlap of [67] ede=d with [139] decdcde=ecdc:
Critical pair: eecdc=dcdcde.
Defines rule #8.
Overlap of [70] dde=e with [139] decdcde=ecdc:
Critical pair: decdc=ecdcde.
Defines rule #9.
Referenced by [148].
Overlap of [140] eecdc=dcdcde with [133] dcdec=cdeced:
Critical pair: eeccdeced=dcdcdedec.
Reduce RHS:
| [67] | dcdcd(ede)c |
| [73] | ⇒ dcd(cdd)c |
| ⇒ dcdcc |
Overlap of [54] cceccdec=d with [134] cdececc=cceccd:
Critical pair: cceccdecceccd=ddececc.
Reduce LHS:
| [54] | (cceccdec)ceccd |
| ⇒ dceccd |
Reduce RHS:
| [70] | (dde)cecc |
| ⇒ ececc |
Referenced by [144], [145], [146], [147], [148].
Overlap of [66] edd=e with [143] dceccd=ececc:
Critical pair: edececc=ececcd.
Reduce LHS:
| [67] | (ede)cecc |
| ⇒ dcecc |
Defines rule #11.
Referenced by [149], [159], [160], [162], [167], [169].
Overlap of [87] dcecdc=cdececde with [143] dceccd=ececc:
Critical pair: dcecececc=cdececdeeccd.
Defines rule #23.
Overlap of [96] ddc=c with [143] dceccd=ececc:
Critical pair: dececc=ceccd.
Defines rule #16.
Referenced by [157].
Overlap of [140] eecdc=dcdcde with [143] dceccd=ececc:
Critical pair: eecececc=dcdcdeeccd.
Defines rule #20.
Overlap of [141] decdc=ecdcde with [143] dceccd=ececc:
Critical pair: decececc=ecdcdeeccd.
Defines rule #21.
Overlap of [144] dcecc=ececcd with [54] cceccdec=d:
Critical pair: dcecd=ececcdceccdec.
Reduce RHS:
| [144] | ececc(dcecc)dec |
| [73] | ⇒ ececcecec(cdd)ec |
| [132] | ⇒ (ececcec)eccec |
| [67] | ⇒ cceccd(ede)ccec |
| [73] | ⇒ ccec(cdd)ccec |
| ⇒ cceccccec |
Flip LHS and RHS.
Defines rule #31.
Referenced by [160].
Overlap of [142] eeccdeced=dcdcc with [66] edd=e:
Critical pair: eeccdece=dcdccd.
Referenced by [152].
Overlap of [142] eeccdeced=dcdcc with [67] ede=d:
Critical pair: eeccdecd=dcdcce.
Referenced by [154].
Overlap of [150] eeccdece=dcdccd with [134] cdececc=cceccd:
Critical pair: eeccceccd=dcdccdcc.
Referenced by [163].
Simplify [125] eb=bdccceccde.
Reduce RHS:
| [137] | b(dccceccde) |
| ⇒ bcdececdecec |
Defines rule #41.
Overlap of [151] eeccdecd=dcdcce with [73] cdd=c:
Critical pair: eeccdec=dcdcced.
Defines rule #13.
Overlap of [67] ede=d with [154] eeccdec=dcdcced:
Critical pair: eddcdcced=deccdec.
Reduce LHS:
| [66] | (edd)cdcced |
| ⇒ ecdcced |
Flip LHS and RHS.
Defines rule #15.
Referenced by [157].
Overlap of [154] eeccdec=dcdcced with [113] deccec=ccecd:
Critical pair: eeccccecd=dcdccedcec.
Overlap of [155] deccdec=ecdcced with [146] dececc=ceccd:
Critical pair: deccceccd=ecdccedecc.
Reduce RHS:
| [67] | ecdcc(ede)cc |
| ⇒ ecdccdcc |
Referenced by [164].
Overlap of [136] eccecdc=ceccdece with [114] dccec=eccecd:
Critical pair: eccececcecd=ceccdececec.
Reduce LHS:
| [132] | ecc(ececcec)d |
| [66] | ⇒ ecccceccd(edd) |
| ⇒ ecccceccde |
Overlap of [136] eccecdc=ceccdece with [144] dcecc=ececcd:
Critical pair: eccecececcd=ceccdeceecc.
Referenced by [173].
Overlap of [149] cceccccec=dcecd with [132] ececcec=cceccded:
Critical pair: ccecccccceccded=dcecdeccec.
Reduce RHS:
| [113] | dcec(deccec) |
| [144] | ⇒ (dcecc)cecd |
| ⇒ ececcdcecd |
Referenced by [175].
Overlap of [135] dcccecd=cdecedcec with [73] cdd=c:
Critical pair: dcccec=cdecedcecd.
Defines rule #19.
Overlap of [135] dcccecd=cdecedcec with [114] dccec=eccecd:
Critical pair: dcccececcecd=cdecedcecccec.
Reduce LHS:
| [132] | dccc(ececcec)d |
| [66] | ⇒ dccccceccd(edd) |
| ⇒ dccccceccde |
Reduce RHS:
| [144] | cdece(dcecc)cec |
| ⇒ cdeceececcdcec |
Referenced by [174].
Overlap of [152] eeccceccd=dcdccdcc with [73] cdd=c:
Critical pair: eecccecc=dcdccdccd.
Defines rule #25.
Referenced by [165].
Simplify [117] ea=adeccceccde.
Reduce RHS:
| [157] | a(deccceccd)e |
| ⇒ aecdccdcce |
Defines rule #37.
Overlap of [67] ede=d with [163] eecccecc=dcdccdccd:
Critical pair: eddcdccdccd=decccecc.
Reduce LHS:
| [66] | (edd)cdccdccd |
| ⇒ ecdccdccd |
Flip LHS and RHS.
Defines rule #27.
Referenced by [172].
Overlap of [156] eeccccecd=dcdccedcec with [73] cdd=c:
Critical pair: eeccccec=dcdccedcecd.
Defines rule #24.
Referenced by [168].
Overlap of [156] eeccccecd=dcdccedcec with [114] dccec=eccecd:
Critical pair: eeccccececcecd=dcdccedcecccec.
Reduce LHS:
| [132] | eecccc(ececcec)d |
| [66] | ⇒ eecccccceccd(edd) |
| ⇒ eecccccceccde |
Reduce RHS:
| [144] | dcdcce(dcecc)cec |
| ⇒ dcdcceececcdcec |
Referenced by [176].
Overlap of [67] ede=d with [166] eeccccec=dcdccedcecd:
Critical pair: eddcdccedcecd=deccccec.
Reduce LHS:
| [66] | (edd)cdccedcecd |
| ⇒ ecdccedcecd |
Flip LHS and RHS.
Defines rule #26.
Overlap of [67] ede=d with [158] ecccceccde=ceccdececec:
Critical pair: edceccdececec=dcccceccde.
Reduce LHS:
| [144] | e(dcecc)dececec |
| [73] | ⇒ eecec(cdd)ececec |
| [132] | ⇒ e(ececcec)ecec |
| [67] | ⇒ ecceccd(ede)cec |
| [73] | ⇒ eccec(cdd)cec |
| ⇒ eccecccec |
Flip LHS and RHS.
Referenced by [171].
Overlap of [158] ecccceccde=ceccdececec with [67] ede=d:
Critical pair: ecccceccdd=ceccdecececde.
Reduce LHS:
| [73] | eccccec(cdd) |
| ⇒ eccccecc |
Defines rule #28.
Overlap of [169] dcccceccde=eccecccec with [67] ede=d:
Critical pair: dcccceccdd=eccecccecde.
Reduce LHS:
| [73] | dccccec(cdd) |
| ⇒ dccccecc |
Defines rule #30.
Simplify [118] da=adecccecc.
Reduce RHS:
| [165] | a(decccecc) |
| ⇒ aecdccdccd |
Defines rule #38.
Overlap of [159] eccecececcd=ceccdeceecc with [73] cdd=c:
Critical pair: eccecececc=ceccdeceeccd.
Defines rule #29.
Overlap of [162] dccccceccde=cdeceececcdcec with [67] ede=d:
Critical pair: dccccceccdd=cdeceececcdcecde.
Reduce LHS:
| [73] | dcccccec(cdd) |
| ⇒ dcccccecc |
Defines rule #33.
Overlap of [160] ccecccccceccded=ececcdcecd with [67] ede=d:
Critical pair: ccecccccceccdd=ececcdcecde.
Reduce LHS:
| [73] | cceccccccec(cdd) |
| ⇒ cceccccccecc |
Defines rule #36.
Overlap of [167] eecccccceccde=dcdcceececcdcec with [67] ede=d:
Critical pair: eecccccceccdd=dcdcceececcdcecde.
Reduce LHS:
| [73] | eeccccccec(cdd) |
| ⇒ eeccccccecc |
Defines rule #34.
Referenced by [177].
Overlap of [67] ede=d with [176] eeccccccecc=dcdcceececcdcecde:
Critical pair: eddcdcceececcdcecde=deccccccecc.
Reduce LHS:
| [66] | (edd)cdcceececcdcecde |
| ⇒ ecdcceececcdcecde |
Flip LHS and RHS.
Defines rule #35.