Certificate for #1777 ⟨a, b | ababaaaab=a⟩

Completion settings:

• Auxiliary generators:
  1. c = ab
  2. d = caa
  3. e = ada
• Reduction order:
  • Right-to-left recursive path with deg(b) = deg(d) = deg(c) = 0, b < d < c; deg(e) = 1; deg(a) = 2

Axiom: ababaaaab=a.

Referenced by [5].

Axiom: ab=c.

Referenced by [5], [6], [8], [71].

Axiom: caa=d.

Referenced by [5], [6], [7], [9], [11], [13], [14], [17], [19], [24].

Axiom: ada=e.

Referenced by [7], [8], [12], [15], [25], [27], [28].

Overlap of [1] ababaaaab=a with [2] ab=c:

Critical pair: cabaaaab=a.

Reduce LHS:

Referenced by [11], [12], [13], [15], [18], [20], [31], [34], [37].

Overlap of [3] caa=d with [2] ab=c:

Critical pair: cac=db.

Referenced by [9], [10], [13], [16], [21], [32], [38].

Overlap of [3] caa=d with [4] ada=e:

Critical pair: cae=dda.

Referenced by [21], [22], [39].

Overlap of [4] ada=e with [2] ab=c:

Critical pair: adc=eb.

Referenced by [14], [15], [16], [22], [29], [33], [41].

Overlap of [6] cac=db with [3] caa=d:

Critical pair: cad=dbaa.

Flip LHS and RHS.

Referenced by [25], [42].

Overlap of [6] cac=db with [6] cac=db:

Critical pair: cadb=dbac.

Referenced by [44].

Overlap of [5] cdac=a with [3] caa=d:

Critical pair: cdad=aaa.

Flip LHS and RHS.

Referenced by [24], [25], [26], [36].

Overlap of [5] cdac=a with [5] cdac=a:

Critical pair: cdaa=adac.

Reduce RHS:

Referenced by [23].

Overlap of [6] cac=db with [5] cdac=a:

Critical pair: caa=dbdac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [18], [27], [46].

Overlap of [8] adc=eb with [3] caa=d:

Critical pair: add=ebaa.

Flip LHS and RHS.

Referenced by [26].

Overlap of [8] adc=eb with [5] cdac=a:

Critical pair: ada=ebdac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [20], [47].

Overlap of [8] adc=eb with [6] cac=db:

Critical pair: addb=ebac.

Referenced by [48].

Overlap of [13] dbdac=d with [3] caa=d:

Critical pair: dbdad=daa.

Flip LHS and RHS.

Referenced by [18], [20], [23], [28], [35].

Overlap of [13] dbdac=d with [5] cdac=a:

Critical pair: dbdaa=ddac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [15] ebdac=e with [3] caa=d:

Critical pair: ebdad=eaa.

Flip LHS and RHS.

Referenced by [52].

Overlap of [15] ebdac=e with [5] cdac=a:

Critical pair: ebdaa=edac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31], [54].

Overlap of [6] cac=db with [7] cae=dda:

Critical pair: cadda=dbae.

Referenced by [56].

Overlap of [8] adc=eb with [7] cae=dda:

Critical pair: addda=ebae.

Referenced by [58].

Overlap of [12] cdaa=ec with [17] daa=dbdad:

Critical pair: cdbdad=ec.

Referenced by [30].

Overlap of [3] caa=d with [11] aaa=cdad:

Critical pair: ccdad=da.

Referenced by [27], [28], [29], [60].

Overlap of [9] dbaa=cad with [11] aaa=cdad:

Critical pair: dbcdad=cada.

Reduce RHS:

Referenced by [33], [34], [62].

Overlap of [14] ebaa=add with [11] aaa=cdad:

Critical pair: ebcdad=adda.

Flip LHS and RHS.

Referenced by [63].

Overlap of [13] dbdac=d with [24] ccdad=da:

Critical pair: dbdada=dcdad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36], [65].

Overlap of [24] ccdad=da with [4] ada=e:

Critical pair: ccde=daa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [30], [31], [35], [50], [54], [66].

Overlap of [24] ccdad=da with [8] adc=eb:

Critical pair: ccdeb=dac.

Flip LHS and RHS.

Referenced by [37], [46], [47], [51], [55], [67].

Simplify [23] cdbdad=ec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [31], [32], [33], [55], [72], [74], [75], [76], [77], [78], [81].

Overlap of [30] ec=cccde with [5] cdac=a:

Critical pair: ea=cccdedac.

Reduce RHS:

Referenced by [32], [36], [53].

Overlap of [30] ec=cccde with [6] cac=db:

Critical pair: edb=cccdeac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [68].

Overlap of [25] dbcdad=ce with [8] adc=eb:

Critical pair: dbcdeb=cec.

Reduce RHS:

Defines rule #4.

Overlap of [25] dbcdad=ce with [25] dbcdad=ce:

Critical pair: dbcdace=cebcdad.

Reduce LHS:

Referenced by [56], [69].

Simplify [17] daa=dbdad.

Reduce RHS:

Referenced by [36].

Overlap of [35] daa=ccde with [11] aaa=cdad:

Critical pair: dcdad=ccdea.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [53].

Overlap of [5] cdac=a with [29] dac=ccdeb:

Critical pair: cccdeb=a.

Flip LHS and RHS.

Defines rule #34.

Referenced by [38], [39], [40], [41], [42], [43], [44], [45], [48], [49], [52], [56], [57], [58], [59], [60], [61], [62], [63], [64], [65], [66], [67], [69], [70], [71].

Overlap of [6] cac=db with [37] a=cccdeb:

Critical pair: ccccdebc=db.

Defines rule #16.

Referenced by [68], [80].

Simplify [7] cae=dda.

Reduce RHS:

Referenced by [40].

Overlap of [39] cae=ddcccdeb with [37] a=cccdeb:

Critical pair: ccccdebe=ddcccdeb.

Defines rule #19.

Referenced by [80], [83].

Overlap of [8] adc=eb with [37] a=cccdeb:

Critical pair: cccdebdc=eb.

Defines rule #18.

Referenced by [72], [73], [76], [77], [78], [79], [81], [82], [84].

Simplify [9] dbaa=cad.

Reduce RHS:

Referenced by [43].

Overlap of [42] dbaa=ccccdebd with [37] a=cccdeb:

Critical pair: dbcccdeba=ccccdebd.

Reduce LHS:

Defines rule #26.

Referenced by [84].

Simplify [10] cadb=dbac.

Reduce RHS:

Referenced by [45].

Overlap of [44] cadb=dbcccdebc with [37] a=cccdeb:

Critical pair: ccccdebdb=dbcccdebc.

Defines rule #17.

Referenced by [82].

Overlap of [13] dbdac=d with [29] dac=ccdeb:

Critical pair: dbccdeb=d.

Defines rule #6.

Referenced by [74].

Overlap of [15] ebdac=e with [29] dac=ccdeb:

Critical pair: ebccdeb=e.

Defines rule #25.

Referenced by [76].

Simplify [16] addb=ebac.

Reduce RHS:

Referenced by [49].

Overlap of [48] addb=ebcccdebc with [37] a=cccdeb:

Critical pair: cccdebddb=ebcccdebc.

Flip LHS and RHS.

Defines rule #30.

Referenced by [83].

Simplify [18] ddac=dbdbdad.

Reduce RHS:

Referenced by [51].

Overlap of [50] ddac=dbccde with [29] dac=ccdeb:

Critical pair: dccdeb=dbccde.

Defines rule #5.

Referenced by [73].

Simplify [19] eaa=ebdad.

Reduce RHS:

Referenced by [53].

Overlap of [52] eaa=ebdcccdebd with [31] ea=cccdebccde:

Critical pair: cccdebccdea=ebdcccdebd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Simplify [20] edac=ebdbdad.

Reduce RHS:

Referenced by [55].

Overlap of [54] edac=ebccde with [29] dac=ccdeb:

Critical pair: eccdeb=ebccde.

Reduce LHS:

Referenced by [72], [74].

Simplify [21] cadda=dbae.

Reduce RHS:

Referenced by [57].

Overlap of [56] cadda=cebcdcccdebd with [37] a=cccdeb:

Critical pair: ccccdebdda=cebcdcccdebd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [69].

Simplify [22] addda=ebae.

Reduce RHS:

Referenced by [59].

Overlap of [58] addda=ebcccdebe with [37] a=cccdeb:

Critical pair: cccdebddda=ebcccdebe.

Reduce LHS:

Flip LHS and RHS.

Defines rule #32.

Simplify [24] ccdad=da.

Reduce RHS:

Referenced by [61].

Overlap of [60] ccdad=dcccdeb with [37] a=cccdeb:

Critical pair: ccdcccdebd=dcccdeb.

Defines rule #13.

Overlap of [25] dbcdad=ce with [37] a=cccdeb:

Critical pair: dbcdcccdebd=ce.

Defines rule #14.

Simplify [26] adda=ebcdad.

Reduce RHS:

Referenced by [64].

Overlap of [63] adda=ebcdcccdebd with [37] a=cccdeb:

Critical pair: cccdebdda=ebcdcccdebd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [27] dcdad=dbde with [37] a=cccdeb:

Critical pair: dcdcccdebd=dbde.

Defines rule #12.

Referenced by [78].

Overlap of [28] dbdad=ccde with [37] a=cccdeb:

Critical pair: dbdcccdebd=ccde.

Defines rule #11.

Referenced by [77].

Overlap of [29] dac=ccdeb with [37] a=cccdeb:

Critical pair: dcccdebc=ccdeb.

Defines rule #15.

Referenced by [68], [74], [76].

Overlap of [32] cccdcccdebccdcccde=edb with [67] dcccdebc=ccdeb:

Critical pair: cccccdebcdcccde=edb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [74].

Simplify [34] dbae=cebcdad.

Reduce RHS:

Referenced by [70].

Overlap of [69] dbae=ccccdebddcccdeb with [37] a=cccdeb:

Critical pair: dbcccdebe=ccccdebddcccdeb.

Flip LHS and RHS.

Defines rule #27.

Overlap of [2] ab=c with [37] a=cccdeb:

Critical pair: cccdebb=c.

Defines rule #9.

Overlap of [30] ec=cccde with [41] cccdebdc=eb:

Critical pair: eeb=cccdeccdebdc.

Reduce RHS:

Flip LHS and RHS.

Referenced by [75].

Overlap of [41] cccdebdc=eb with [51] dccdeb=dbccde:

Critical pair: cccdebdbccde=ebcdeb.

Flip LHS and RHS.

Defines rule #24.

Overlap of [68] edb=cdbdcccde with [46] dbccdeb=d:

Critical pair: ed=cdbdcccdeccdeb.

Reduce RHS:

Defines rule #7.

Referenced by [75], [76], [80].

Overlap of [72] cccdebccdedc=eeb with [74] ed=cdcde:

Critical pair: cccdebccdcdcdec=eeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [67] dcccdebc=ccdeb with [41] cccdebdc=eb:

Critical pair: dcccdebeb=ccdebccdebdc.

Reduce RHS:

Defines rule #21.

Overlap of [66] dbdcccdebd=ccde with [41] cccdebdc=eb:

Critical pair: dbdeb=ccdec.

Reduce RHS:

Defines rule #2.

Overlap of [65] dcdcccdebd=dbde with [41] cccdebdc=eb:

Critical pair: dcdeb=dbdec.

Reduce RHS:

Defines rule #3.

Referenced by [79].

Overlap of [41] cccdebdc=eb with [78] dcdeb=dbdcccde:

Critical pair: cccdebdbdcccde=ebdeb.

Flip LHS and RHS.

Defines rule #23.

Overlap of [40] ccccdebe=ddcccdeb with [74] ed=cdcde:

Critical pair: ccccdebcdcde=ddcccdebd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [81].

Overlap of [80] ddcccdebd=dbdcde with [41] cccdebdc=eb:

Critical pair: ddeb=dbdcdec.

Reduce RHS:

Defines rule #1.

Overlap of [41] cccdebdc=eb with [45] ccccdebdb=dbcccdebc:

Critical pair: cccdebddbcccdebc=ebcccdebdb.

Flip LHS and RHS.

Defines rule #31.

Overlap of [49] ebcccdebc=cccdebddb with [40] ccccdebe=ddcccdeb:

Critical pair: ebcccdebddcccdeb=cccdebddbcccdebe.

Defines rule #33.

Overlap of [43] dbcccdebcccdeb=ccccdebd with [41] cccdebdc=eb:

Critical pair: dbcccdebeb=ccccdebddc.

Defines rule #22.