Certificate for #11071 ⟨a, b | baab=aaa, bbbb=1⟩

Completion settings:

• Auxiliary generators:
  1. c = bbb
  2. d = cacaca
  3. e = dadadad
• Reduction order:
  • Left-to-right recursive path with deg(a) = 0; deg(e) = 1; deg(d) = 2; deg(c) = deg(b) = 3, c < b

Axiom: baab=aaa.

Referenced by [10], [11].

Axiom: bbbb=1.

Referenced by [6].

Axiom: bbb=c.

Referenced by [6], [7], [8], [12].

Axiom: cacaca=d.

Referenced by [16], [17], [18], [19], [20].

Axiom: dadadad=e.

Referenced by [28], [29], [30], [31], [50], [53], [59], [81], [84], [96], [102], [119].

Overlap of [2] bbbb=1 with [3] bbb=c:

Critical pair: cb=1.

Defines rule #57.

Referenced by [7], [8], [9], [11], [13], [23], [33], [36], [92].

Overlap of [3] bbb=c with [3] bbb=c:

Critical pair: bc=cb.

Reduce RHS:

Defines rule #58.

Referenced by [10], [19], [25], [44], [85], [88], [176], [177].

Overlap of [6] cb=1 with [3] bbb=c:

Critical pair: cc=bb.

Flip LHS and RHS.

Defines rule #59.

Referenced by [9], [12], [14], [15], [26], [149], [163], [167].

Overlap of [6] cb=1 with [8] bb=cc:

Critical pair: ccc=b.

Defines rule #60.

Referenced by [34], [78], [83], [86], [90], [145].

Overlap of [1] baab=aaa with [7] bc=1:

Critical pair: baa=aaac.

Referenced by [12], [13], [14], [38].

Overlap of [6] cb=1 with [1] baab=aaa:

Critical pair: caaa=aab.

Flip LHS and RHS.

Referenced by [15], [17], [33], [34], [36], [39].

Overlap of [3] bbb=c with [10] baa=aaac:

Critical pair: bbaaac=caa.

Reduce LHS:

Referenced by [21].

Overlap of [6] cb=1 with [10] baa=aaac:

Critical pair: caaac=aa.

Referenced by [18], [20], [24], [32].

Overlap of [8] bb=cc with [10] baa=aaac:

Critical pair: baaac=ccaa.

Reduce LHS:

Referenced by [20], [40].

Overlap of [11] aab=caaa with [8] bb=cc:

Critical pair: aacc=caaab.

Reduce RHS:

Referenced by [22].

Overlap of [4] cacaca=d with [4] cacaca=d:

Critical pair: cad=dca.

Flip LHS and RHS.

Defines rule #32.

Referenced by [24], [27], [29], [33], [35], [36], [45], [55], [62], [75], [79], [87], [110].

Overlap of [4] cacaca=d with [11] aab=caaa:

Critical pair: cacaccaaa=dab.

Referenced by [23].

Overlap of [4] cacaca=d with [13] caaac=aa:

Critical pair: cacaaa=daac.

Referenced by [22].

Overlap of [7] bc=1 with [4] cacaca=d:

Critical pair: bd=acaca.

Flip LHS and RHS.

Defines rule #56.

Referenced by [23], [37], [46], [76], [80], [89], [94], [111].

Overlap of [13] caaac=aa with [4] cacaca=d:

Critical pair: caaad=aaacaca.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21], [23].

Overlap of [12] ccaaac=caa with [20] ccaaa=caaad:

Critical pair: caaadc=caa.

Referenced by [41].

Simplify [15] aacc=cacaaa.

Reduce RHS:

Referenced by [32], [33], [34], [35].

Overlap of [17] cacaccaaa=dab with [20] ccaaa=caaad:

Critical pair: cacacaaad=dab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #52.

Referenced by [25], [26], [30], [51], [57], [82].

Overlap of [16] dca=cad with [13] caaac=aa:

Critical pair: daa=cadaac.

Flip LHS and RHS.

Referenced by [32].

Overlap of [23] dab=daad with [7] bc=1:

Critical pair: da=daadc.

Flip LHS and RHS.

Referenced by [27], [31], [41], [49], [52], [67].

Overlap of [23] dab=daad with [8] bb=cc:

Critical pair: dacc=daadb.

Referenced by [35].

Overlap of [25] daadc=da with [16] dca=cad:

Critical pair: daacad=daa.

Referenced by [42].

Overlap of [5] dadadad=e with [5] dadadad=e:

Critical pair: dae=ead.

Flip LHS and RHS.

Referenced by [56], [77], [95], [108], [112], [113], [116], [125].

Overlap of [5] dadadad=e with [16] dca=cad:

Critical pair: dadadacad=eca.

Referenced by [126].

Overlap of [5] dadadad=e with [23] dab=daad:

Critical pair: dadadadaad=eab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [112], [128].

Overlap of [5] dadadad=e with [25] daadc=da:

Critical pair: dadadada=eaadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [68].

Overlap of [13] caaac=aa with [22] aacc=daac:

Critical pair: cadaac=aac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [33], [34], [35], [36], [37], [38], [40], [42], [47], [76], [104], [117], [122], [127], [134].

Overlap of [22] aacc=daac with [6] cb=1:

Critical pair: aac=daacb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [55].

Overlap of [22] aacc=daac with [9] ccc=b:

Critical pair: aab=daacc.

Reduce LHS:

Reduce RHS:

Referenced by [39], [41].

Overlap of [16] dca=cad with [22] aacc=daac:

Critical pair: dcdaac=cadacc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [43].

Overlap of [32] aac=daa with [6] cb=1:

Critical pair: aa=daab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [43], [48].

Overlap of [32] aac=daa with [19] acaca=bd:

Critical pair: abd=daaaca.

Reduce RHS:

Defines rule #47.

Simplify [10] baa=aaac.

Reduce RHS:

Defines rule #37.

Referenced by [54], [103], [163].

Simplify [11] aab=caaa.

Reduce RHS:

Referenced by [51], [57], [66].

Overlap of [14] aaacac=ccaa with [32] aac=daa:

Critical pair: adaaac=ccaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [69].

Overlap of [21] caaadc=caa with [34] caaa=dddaa:

Critical pair: dddaadc=caa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44], [45], [46], [47], [64], [69], [70].

Overlap of [27] daacad=daa with [32] aac=daa:

Critical pair: ddaaad=daa.

Referenced by [59].

Overlap of [35] cadaadb=dcddaa with [36] cadaa=aa:

Critical pair: aadb=dcddaa.

Referenced by [90], [146].

Overlap of [7] bc=1 with [41] caa=ddda:

Critical pair: bddda=aa.

Referenced by [50], [51], [52], [54].

Overlap of [16] dca=cad with [41] caa=ddda:

Critical pair: dddda=cada.

Flip LHS and RHS.

Referenced by [48], [55], [62], [71].

Overlap of [19] acaca=bd with [41] caa=ddda:

Critical pair: acaddda=bda.

Flip LHS and RHS.

Referenced by [72].

Overlap of [32] aac=daa with [41] caa=ddda:

Critical pair: aaddda=daaaa.

Referenced by [57].

Simplify [36] cadaa=aa.

Reduce LHS:

Referenced by [49], [55], [60], [62], [63].

Overlap of [48] ddddaa=aa with [25] daadc=da:

Critical pair: dddda=aadc.

Flip LHS and RHS.

Referenced by [52], [67], [68], [73].

Overlap of [44] bddda=aa with [5] dadadad=e:

Critical pair: bdde=aadadad.

Referenced by [74].

Overlap of [44] bddda=aa with [23] dab=daad:

Critical pair: bdddaad=aab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [54], [58], [61], [64], [65].

Overlap of [44] bddda=aa with [25] daadc=da:

Critical pair: bddda=aaadc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [53].

Overlap of [52] adddda=aa with [5] dadadad=e:

Critical pair: addde=aadadad.

Flip LHS and RHS.

Referenced by [74].

Overlap of [44] bddda=aa with [51] dddaa=aaad:

Critical pair: baaad=aaa.

Reduce LHS:

Referenced by [55], [56], [57].

Overlap of [16] dca=cad with [54] adaaad=aaa:

Critical pair: dcaaa=caddaaad.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [58], [59], [97], [103], [127].

Overlap of [28] ead=dae with [54] adaaad=aaa:

Critical pair: eaaa=daeaaad.

Flip LHS and RHS.

Referenced by [97].

Overlap of [54] adaaad=aaa with [23] dab=daad:

Critical pair: adaaadaad=aaaab.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Overlap of [51] dddaa=aaad with [55] daaad=aa:

Critical pair: ddaa=aaadad.

Flip LHS and RHS.

Defines rule #13.

Referenced by [59], [72].

Overlap of [55] daaad=aa with [5] dadadad=e:

Critical pair: daaae=aaadadad.

Reduce RHS:

Referenced by [60], [61].

Overlap of [48] ddddaa=aa with [59] daaae=daa:

Critical pair: ddddaa=aaae.

Reduce LHS:

Flip LHS and RHS.

Referenced by [62], [63], [64], [65], [80], [99], [103].

Overlap of [51] dddaa=aaad with [59] daaae=daa:

Critical pair: dddaa=aaadae.

Reduce LHS:

Flip LHS and RHS.

Referenced by [65].

Overlap of [16] dca=cad with [60] aaae=aa:

Critical pair: dcaa=cadaae.

Reduce LHS:

Reduce RHS:

Referenced by [63], [67], [68], [71], [73].

Overlap of [48] ddddaa=aa with [60] aaae=aa:

Critical pair: ddddaa=aaae.

Reduce LHS:

Reduce RHS:

Referenced by [75], [76], [77], [82].

Overlap of [41] caa=ddda with [60] aaae=aa:

Critical pair: caa=dddaae.

Reduce LHS:

Reduce RHS:

Defines rule #14.

Referenced by [65], [66], [69], [70], [72], [103].

Overlap of [51] dddaa=aaad with [60] aaae=aa:

Critical pair: dddaa=aaadae.

Reduce LHS:

Reduce RHS:

Referenced by [66], [69], [72], [78].

Simplify [39] aab=dddaa.

Reduce RHS:

Defines rule #48.

Overlap of [25] daadc=da with [49] aadc=dddda:

Critical pair: ddddda=da.

Reduce LHS:

Referenced by [72], [78], [79], [93], [101], [124].

Overlap of [31] eaadc=ea with [49] aadc=dddda:

Critical pair: edddda=ea.

Reduce LHS:

Referenced by [106], [107], [109].

Overlap of [40] ccaa=adadaa with [41] caa=ddda:

Critical pair: cddda=adadaa.

Reduce LHS:

Referenced by [78].

Simplify [41] caa=ddda.

Reduce RHS:

Defines rule #19.

Referenced by [72], [78], [80], [100].

Simplify [45] cada=dddda.

Reduce RHS:

Referenced by [75], [78], [79], [80], [81], [82], [129].

Simplify [46] bda=acaddda.

Reduce RHS:

Defines rule #39.

Simplify [49] aadc=dddda.

Reduce RHS:

Referenced by [90], [105], [113], [123], [130].

Simplify [50] bdde=aadadad.

Reduce RHS:

Referenced by [121], [131].

Overlap of [16] dca=cad with [63] aaea=aa:

Critical pair: dcaa=cadaea.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [93].

Overlap of [63] aaea=aa with [19] acaca=bd:

Critical pair: aaebd=aacaca.

Reduce RHS:

Referenced by [91].

Overlap of [63] aaea=aa with [28] ead=dae:

Critical pair: aadae=aad.

Referenced by [132].

Overlap of [9] ccc=b with [71] cada=aae:

Critical pair: ccaae=bada.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Referenced by [167], [176], [177].

Overlap of [16] dca=cad with [71] cada=aae:

Critical pair: daae=cadda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #27.

Referenced by [83], [84], [101].

Overlap of [19] acaca=bd with [71] cada=aae:

Critical pair: acaaae=bdda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #43.

Referenced by [163], [164].

Overlap of [71] cada=aae with [5] dadadad=e:

Critical pair: cae=aaedadad.

Referenced by [92], [98].

Overlap of [71] cada=aae with [23] dab=daad:

Critical pair: cadaad=aaeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [91].

Overlap of [9] ccc=b with [79] cadda=da:

Critical pair: ccda=badda.

Referenced by [152].

Overlap of [79] cadda=da with [5] dadadad=e:

Critical pair: cade=dadadad.

Reduce RHS:

Defines rule #24.

Referenced by [85], [86], [87], [89], [110], [120], [142].

Overlap of [7] bc=1 with [84] cade=e:

Critical pair: be=ade.

Defines rule #38.

Referenced by [149].

Overlap of [9] ccc=b with [84] cade=e:

Critical pair: cce=bade.

Referenced by [147].

Overlap of [16] dca=cad with [84] cade=e:

Critical pair: de=cadde.

Flip LHS and RHS.

Defines rule #28.

Referenced by [88], [89], [101], [167].

Overlap of [7] bc=1 with [87] cadde=de:

Critical pair: bde=adde.

Defines rule #40.

Overlap of [19] acaca=bd with [87] cadde=de:

Critical pair: acade=bddde.

Reduce LHS:

Flip LHS and RHS.

Referenced by [92], [103], [121].

Overlap of [73] aadc=aae with [9] ccc=b:

Critical pair: aadb=aaecc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [134].

Overlap of [76] aaebd=dadaaa with [82] aaeb=aad:

Critical pair: aadd=dadaaa.

Defines rule #12.

Referenced by [153].

Overlap of [6] cb=1 with [89] bddde=ae:

Critical pair: cae=ddde.

Reduce LHS:

Referenced by [98].

Overlap of [67] daae=da with [75] aaeea=aae:

Critical pair: daae=daea.

Reduce LHS:

Flip LHS and RHS.

Referenced by [94], [95], [97].

Overlap of [93] daea=da with [19] acaca=bd:

Critical pair: daebd=dacaca.

Reduce RHS:

Referenced by [135].

Overlap of [93] daea=da with [28] ead=dae:

Critical pair: dadae=dad.

Referenced by [96], [119], [136].

Overlap of [5] dadadad=e with [95] dadae=dad:

Critical pair: dadadad=eae.

Reduce LHS:

Flip LHS and RHS.

Referenced by [109], [113], [114], [115], [121].

Overlap of [56] daeaaad=eaaa with [93] daea=da:

Critical pair: daaad=eaaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [99], [139], [179], [180], [181].

Simplify [81] cae=aaedadad.

Reduce RHS:

Referenced by [133].

Overlap of [97] eaaa=aa with [60] aaae=aa:

Critical pair: eaa=aae.

Flip LHS and RHS.

Referenced by [100], [101], [107], [115], [129], [130], [134].

Overlap of [70] caa=aaade with [99] aae=eaa:

Critical pair: ceaa=aaadee.

Referenced by [137].

Overlap of [79] cadda=da with [99] aae=eaa:

Critical pair: caddeaa=daae.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [102], [103], [104], [105], [106], [141], [147], [152], [154], [161].

Overlap of [5] dadadad=e with [101] deaa=da:

Critical pair: dadadada=eeaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [115].

Overlap of [89] bddde=ae with [101] deaa=da:

Critical pair: bddda=aeaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [107].

Overlap of [101] deaa=da with [32] aac=daa:

Critical pair: dedaa=dac.

Flip LHS and RHS.

Referenced by [169].

Overlap of [101] deaa=da with [73] aadc=aae:

Critical pair: deaae=dadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [138].

Overlap of [101] deaa=da with [68] eaae=ea:

Critical pair: dea=dae.

Flip LHS and RHS.

Referenced by [108], [112], [113], [116], [125], [132], [135], [136], [138].

Overlap of [103] aeaa=aa with [68] eaae=ea:

Critical pair: aea=aae.

Reduce RHS:

Referenced by [108], [109].

Overlap of [107] aea=eaa with [28] ead=dae:

Critical pair: adae=eaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [128], [147].

Overlap of [107] aea=eaa with [96] eae=e:

Critical pair: ae=eaae.

Reduce RHS:

Defines rule #2.

Referenced by [110], [120], [121], [133], [142], [143], [147], [153], [155], [162], [166], [168], [173].

Overlap of [16] dca=cad with [109] ae=ea:

Critical pair: dcea=cade.

Reduce RHS:

Referenced by [111], [112], [113], [114], [115].

Overlap of [110] dcea=e with [19] acaca=bd:

Critical pair: dcebd=ecaca.

Referenced by [139].

Overlap of [110] dcea=e with [30] eab=eaad:

Critical pair: dceaad=eb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #49.

Referenced by [140].

Overlap of [110] dcea=e with [73] aadc=aae:

Critical pair: dceaae=eadc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [118].

Overlap of [110] dcea=e with [96] eae=e:

Critical pair: dce=ee.

Referenced by [115], [140].

Overlap of [110] dcea=e with [99] aae=eaa:

Critical pair: dceeaa=eae.

Reduce LHS:

Reduce RHS:

Defines rule #3.

Referenced by [116], [117], [139], [141], [142], [145], [146], [147], [155], [157], [158], [159], [160], [162], [166], [168], [171], [178], [179], [180], [181].

Overlap of [115] eea=e with [28] ead=dae:

Critical pair: edae=ed.

Reduce LHS:

Referenced by [140], [143], [147], [173], [174], [175].

Overlap of [115] eea=e with [32] aac=daa:

Critical pair: eedaa=eac.

Flip LHS and RHS.

Referenced by [118], [145], [157], [179].

Simplify [113] deac=e.

Reduce LHS:

Referenced by [119], [120], [121], [122], [123], [124].

Overlap of [5] dadadad=e with [118] deedaa=e:

Critical pair: dadadae=eeedaa.

Reduce LHS:

Referenced by [127], [141], [153], [154], [158].

Overlap of [84] cade=e with [118] deedaa=e:

Critical pair: cae=eedaa.

Reduce LHS:

Referenced by [133], [137].

Overlap of [89] bddde=ae with [118] deedaa=e:

Critical pair: bdde=aeedaa.

Reduce LHS:

Reduce RHS:

Referenced by [131].

Overlap of [118] deedaa=e with [32] aac=daa:

Critical pair: deeddaa=ec.

Flip LHS and RHS.

Referenced by [126], [139], [141].

Overlap of [118] deedaa=e with [73] aadc=aae:

Critical pair: deedaae=edc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [164], [174], [175].

Overlap of [118] deedaa=e with [67] daae=da:

Critical pair: deeda=ee.

Referenced by [142], [143].

Simplify [28] ead=dae.

Reduce RHS:

Defines rule #8.

Referenced by [135], [144], [148], [150], [155].

Simplify [29] dadadacad=eca.

Reduce RHS:

Referenced by [127].

Overlap of [126] dadadacad=deeddaaa with [119] dadad=eeedaa:

Critical pair: eeedaaacad=deeddaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [139].

Simplify [30] eab=eaad.

Reduce RHS:

Defines rule #50.

Referenced by [135], [156].

Simplify [71] cada=aae.

Reduce RHS:

Defines rule #23.

Simplify [73] aadc=aae.

Reduce RHS:

Defines rule #34.

Referenced by [152], [174].

Simplify [74] bdde=addde.

Reduce RHS:

Referenced by [149], [164], [178].

Overlap of [77] aadae=aad with [106] dae=dea:

Critical pair: aadea=aad.

Defines rule #5.

Referenced by [139], [167].

Overlap of [98] cae=ddde with [109] ae=ea:

Critical pair: cea=ddde.

Reduce LHS:

Flip LHS and RHS.

Referenced by [155], [166], [180].

Overlap of [90] aaecc=dcddaa with [99] aae=eaa:

Critical pair: eaacc=dcddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [146].

Overlap of [94] daebd=dbd with [106] dae=dea:

Critical pair: deabd=dbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [151].

Overlap of [95] dadae=dad with [106] dae=dea:

Critical pair: dadea=dad.

Defines rule #10.

Referenced by [141], [146], [148], [150], [153], [156].

Overlap of [100] ceaa=aaadee with [120] cea=eedaa:

Critical pair: eedaaa=aaadee.

Referenced by [139].

Simplify [105] dadc=dae.

Reduce RHS:

Defines rule #35.

Referenced by [145], [164], [175].

Simplify [111] dcebd=ecaca.

Reduce RHS:

Referenced by [140].

Overlap of [139] dcebd=aadadee with [114] dce=ee:

Critical pair: eebd=aadadee.

Reduce LHS:

Referenced by [141], [146], [147], [154].

Simplify [122] ec=deeddaa.

Reduce RHS:

Referenced by [145], [159].

Overlap of [84] cade=e with [124] deeda=ee:

Critical pair: caee=eeda.

Reduce LHS:

Referenced by [144], [147], [181].

Overlap of [124] deeda=ee with [109] ae=ea:

Critical pair: deedea=eee.

Reduce LHS:

Referenced by [145], [153], [154], [157].

Overlap of [142] ce=eeda with [125] ead=dea:

Critical pair: cdea=eedaad.

Referenced by [161], [162].

Overlap of [138] dadc=dea with [9] ccc=b:

Critical pair: dadb=deacc.

Reduce RHS:

Referenced by [160].

Simplify [43] aadb=dcddaa.

Reduce RHS:

Defines rule #53.

Overlap of [86] cce=bade with [142] ce=eeda:

Critical pair: ceeda=bade.

Reduce LHS:

Flip LHS and RHS.

Defines rule #42.

Referenced by [150].

Overlap of [136] dadea=dad with [125] ead=dea:

Critical pair: daddea=dadd.

Defines rule #16.

Referenced by [151], [155], [156], [157].

Overlap of [8] bb=cc with [131] bdde=edaa:

Critical pair: bedaa=ccdde.

Reduce LHS:

Flip LHS and RHS.

Referenced by [170].

Overlap of [147] bade=adade with [125] ead=dea:

Critical pair: baddea=adadead.

Reduce RHS:

Referenced by [152], [167], [168].

Simplify [135] dbd=daddea.

Reduce RHS:

Defines rule #51.

Overlap of [83] ccda=badda with [130] aadc=eaa:

Critical pair: ccdeaa=baddaadc.

Reduce LHS:

Reduce RHS:

Defines rule #45.

Overlap of [91] aadd=dadaaa with [143] deed=eee:

Critical pair: aadeee=dadaaaeed.

Reduce RHS:

Flip LHS and RHS.

Referenced by [154].

Overlap of [143] deed=eee with [140] edd=aadadee:

Critical pair: deaadadee=eeed.

Reduce LHS:

Flip LHS and RHS.

Referenced by [158], [159], [160], [167].

Overlap of [148] daddea=dadd with [125] ead=dea:

Critical pair: dadddea=daddd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [165].

Overlap of [148] daddea=dadd with [128] eab=adea:

Critical pair: daddadea=daddb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #55.

Overlap of [148] daddea=dadd with [117] eac=eedaa:

Critical pair: daddeedaa=daddc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #36.

Simplify [119] dadad=eeedaa.

Reduce RHS:

Defines rule #17.

Referenced by [167].

Simplify [141] ec=eeedaa.

Reduce RHS:

Defines rule #30.

Simplify [145] dadb=eeedaa.

Reduce RHS:

Defines rule #54.

Overlap of [144] cdea=eedaad with [101] deaa=da:

Critical pair: cda=eedaada.

Referenced by [171].

Overlap of [144] cdea=eedaad with [109] ae=ea:

Critical pair: cdeea=eedaade.

Reduce LHS:

Referenced by [167], [172].

Overlap of [8] bb=cc with [80] bdda=aaaade:

Critical pair: baaaade=ccdda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [176].

Overlap of [80] bdda=aaaade with [138] dadc=dea:

Critical pair: bddea=aaaadedc.

Reduce LHS:

Reduce RHS:

Referenced by [165], [173].

Simplify [155] daddd=dedaaa.

Reduce RHS:

Defines rule #18.

Referenced by [166].

Overlap of [165] daddd=daaaadee with [133] ddde=eedaa:

Critical pair: daeedaa=daaaadeee.

Reduce LHS:

Referenced by [169], [170].

Overlap of [8] bb=cc with [150] baddea=adadd:

Critical pair: badadd=ccaddea.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [171], [172].

Overlap of [150] baddea=adadd with [109] ae=ea:

Critical pair: baddeea=adadde.

Reduce LHS:

Defines rule #46.

Simplify [104] dac=dedaa.

Reduce RHS:

Defines rule #33.

Simplify [149] ccdde=adedaa.

Reduce RHS:

Referenced by [177].

Simplify [161] cda=eedaada.

Reduce RHS:

Defines rule #21.

Simplify [162] cde=eedaade.

Reduce RHS:

Defines rule #22.

Overlap of [164] edaaa=aaaadee with [109] ae=ea:

Critical pair: edaaea=aaaadeee.

Reduce LHS:

Referenced by [174].

Overlap of [173] edaa=aaaadeee with [130] aadc=eaa:

Critical pair: edeaa=aaaadeeedc.

Reduce LHS:

Reduce RHS:

Referenced by [175].

Overlap of [174] eda=aaaadeeee with [138] dadc=dea:

Critical pair: edea=aaaadeeeedc.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Referenced by [178], [179], [180], [181].

Overlap of [7] bc=1 with [163] ccdda=adaaaade:

Critical pair: badaaaade=cdda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [7] bc=1 with [170] ccdde=adaaaadeee:

Critical pair: badaaaadeee=cdde.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Simplify [131] bdde=edaa.

Reduce RHS:

Defines rule #44.

Simplify [117] eac=eedaa.

Reduce RHS:

Defines rule #31.

Simplify [133] ddde=eedaa.

Reduce RHS:

Defines rule #15.

Simplify [142] ce=eeda.

Reduce RHS:

Defines rule #20.