Certificate for #3817 ⟨a, b | abbabbaaab=a⟩

Completion settings:

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

Axiom: abbabbaaab=a.

Referenced by [5].

Axiom: ab=c.

Referenced by [5], [6], [7], [10], [12], [37].

Axiom: cba=d.

Referenced by [5], [6], [8], [9], [10], [15], [17], [42], [44].

Axiom: daca=e.

Referenced by [7], [11], [14], [16], [18].

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

Critical pair: cbabbaaab=a.

Reduce LHS:

Referenced by [9].

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

Critical pair: cbc=db.

Flip LHS and RHS.

Defines rule #1.

Referenced by [9], [45], [65], [69], [70], [71], [72], [73].

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

Critical pair: dacc=eb.

Referenced by [8], [13], [14], [21], [23].

Overlap of [7] dacc=eb with [3] cba=d:

Critical pair: dacd=ebba.

Flip LHS and RHS.

Referenced by [24].

Simplify [5] dbbaac=a.

Reduce LHS:

Referenced by [10], [11], [12], [13], [14], [22].

Overlap of [9] cbdac=a with [3] cba=d:

Critical pair: cbdad=aba.

Reduce RHS:

Referenced by [20].

Overlap of [9] cbdac=a with [4] daca=e:

Critical pair: cbe=aa.

Flip LHS and RHS.

Referenced by [12], [15], [16].

Overlap of [9] cbdac=a with [9] cbdac=a:

Critical pair: cbdaa=abdac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [9] cbdac=a with [7] dacc=eb:

Critical pair: cbeb=ac.

Flip LHS and RHS.

Referenced by [14], [17], [18], [19].

Overlap of [7] dacc=eb with [9] cbdac=a:

Critical pair: daca=ebbdac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [3] cba=d with [11] aa=cbe:

Critical pair: cbcbe=da.

Flip LHS and RHS.

Referenced by [16], [18], [19], [20], [21], [22], [23], [24], [27], [29].

Overlap of [4] daca=e with [11] aa=cbe:

Critical pair: daccbe=ea.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [3] cba=d with [13] ac=cbeb:

Critical pair: cbcbeb=dc.

Defines rule #11.

Referenced by [36], [39], [40], [52], [53], [55], [56], [59], [60], [61], [62], [63], [66], [67], [68], [70], [71], [72], [73].

Overlap of [4] daca=e with [13] ac=cbeb:

Critical pair: daccbeb=ec.

Reduce LHS:

Referenced by [32].

Overlap of [15] da=cbcbe with [13] ac=cbeb:

Critical pair: dcbeb=cbcbec.

Defines rule #13.

Referenced by [28], [46], [48], [49], [51], [54], [59], [60], [63], [68], [72].

Simplify [10] cbdad=ca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21], [26].

Overlap of [7] dacc=eb with [20] ca=cbcbcbed:

Critical pair: daccbcbcbed=eba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [9] cbdac=a with [15] da=cbcbe:

Critical pair: cbcbcbec=a.

Flip LHS and RHS.

Defines rule #23.

Referenced by [25], [26], [29], [31], [34], [37], [42], [44].

Overlap of [7] dacc=eb with [15] da=cbcbe:

Critical pair: cbcbecc=eb.

Defines rule #14.

Referenced by [30], [32], [33], [36], [46], [50], [51], [57], [58].

Simplify [8] ebba=dacd.

Reduce RHS:

Referenced by [25].

Overlap of [24] ebba=cbcbecd with [22] a=cbcbcbec:

Critical pair: ebbcbcbcbec=cbcbecd.

Defines rule #34.

Overlap of [20] ca=cbcbcbed with [22] a=cbcbcbec:

Critical pair: ccbcbcbec=cbcbcbed.

Flip LHS and RHS.

Defines rule #19.

Overlap of [12] cdac=cbdcbe with [15] da=cbcbe:

Critical pair: ccbcbec=cbdcbe.

Defines rule #4.

Referenced by [50], [51].

Overlap of [14] ebbdcbeb=e with [19] dcbeb=cbcbec:

Critical pair: ebbcbcbec=e.

Defines rule #33.

Referenced by [38], [39], [41], [48], [51], [52], [54], [55], [59], [60], [61], [63], [66], [68].

Overlap of [15] da=cbcbe with [22] a=cbcbcbec:

Critical pair: dcbcbcbec=cbcbe.

Defines rule #9.

Simplify [16] ea=cbcbeccbe.

Reduce RHS:

Referenced by [31].

Overlap of [30] ea=ebbe with [22] a=cbcbcbec:

Critical pair: ecbcbcbec=ebbe.

Defines rule #32.

Referenced by [42], [49], [54], [72].

Overlap of [18] cbcbeccbeb=ec with [23] cbcbecc=eb:

Critical pair: ebbeb=ec.

Defines rule #38.

Referenced by [35], [47].

Simplify [21] eba=cbcbeccbcbcbed.

Reduce RHS:

Referenced by [34].

Overlap of [33] eba=ebbcbcbed with [22] a=cbcbcbec:

Critical pair: ebcbcbcbec=ebbcbcbed.

Flip LHS and RHS.

Defines rule #48.

Overlap of [32] ebbeb=ec with [32] ebbeb=ec:

Critical pair: ebbec=ecbeb.

Flip LHS and RHS.

Referenced by [39], [40], [64].

Overlap of [23] cbcbecc=eb with [17] cbcbeb=dc:

Critical pair: cbcbecdc=ebbcbeb.

Flip LHS and RHS.

Defines rule #39.

Overlap of [2] ab=c with [22] a=cbcbcbec:

Critical pair: cbcbcbecb=c.

Defines rule #15.

Referenced by [38], [40], [43], [53], [56], [62], [67].

Overlap of [28] ebbcbcbec=e with [37] cbcbcbecb=c:

Critical pair: ebbcbcbec=ebcbcbecb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [42], [43], [46].

Overlap of [28] ebbcbcbec=e with [35] ecbeb=ebbec:

Critical pair: ebbcbcbebbec=ebeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48], [74].

Overlap of [37] cbcbcbecb=c with [35] ecbeb=ebbec:

Critical pair: cbcbcbebbec=ceb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41], [45], [75].

Overlap of [28] ebbcbcbec=e with [40] ceb=cbdcbec:

Critical pair: ebbcbcbecbdcbec=eeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [76].

Overlap of [38] ebcbcbecb=e with [3] cba=d:

Critical pair: ebcbcbed=ea.

Reduce RHS:

Defines rule #47.

Overlap of [38] ebcbcbecb=e with [37] cbcbcbecb=c:

Critical pair: ebcbcbec=ecbcbecb.

Flip LHS and RHS.

Referenced by [47], [48].

Overlap of [3] cba=d with [22] a=cbcbcbec:

Critical pair: cbcbcbcbec=d.

Defines rule #5.

Referenced by [45], [49], [51], [54], [65], [69], [70], [71], [72], [73].

Overlap of [44] cbcbcbcbec=d with [40] ceb=cbdcbec:

Critical pair: cbcbcbcbecbdcbec=deb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [77].

Overlap of [19] dcbeb=cbcbec with [38] ebcbcbecb=e:

Critical pair: dcbe=cbcbeccbcbecb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [47], [48], [49].

Overlap of [32] ebbeb=ec with [46] ebbcbecb=dcbe:

Critical pair: ebbdcbe=ecbcbecb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #31.

Referenced by [54], [59], [60], [63], [68].

Overlap of [39] ebeb=ebbdcbec with [46] ebbcbecb=dcbe:

Critical pair: ebdcbe=ebbdcbecbcbecb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [52], [53], [54], [59].

Overlap of [46] ebbcbecb=dcbe with [44] cbcbcbcbec=d:

Critical pair: ebbcbed=dcbecbcbcbec.

Reduce RHS:

Defines rule #46.

Referenced by [71], [72].

Overlap of [23] cbcbecc=eb with [27] ccbcbec=cbdcbe:

Critical pair: cbcbecbdcbe=ebbcbec.

Flip LHS and RHS.

Defines rule #30.

Referenced by [72], [73].

Overlap of [27] ccbcbec=cbdcbe with [44] cbcbcbcbec=d:

Critical pair: ccbcbed=cbdcbebcbcbcbec.

Reduce RHS:

Defines rule #18.

Overlap of [28] ebbcbcbec=e with [48] ecbcbec=ebdcbe:

Critical pair: ebbcbcbebdcbe=ebcbec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [37] cbcbcbecb=c with [48] ecbcbec=ebdcbe:

Critical pair: cbcbcbebdcbe=ccbec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [58].

Overlap of [48] ecbcbec=ebdcbe with [44] cbcbcbcbec=d:

Critical pair: ecbcbed=ebdcbebcbcbcbec.

Reduce RHS:

Defines rule #45.

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

Overlap of [28] ebbcbcbec=e with [54] ecbcbed=ebe:

Critical pair: ebbcbcbebe=ebcbed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #44.

Overlap of [37] cbcbcbecb=c with [54] ecbcbed=ebe:

Critical pair: cbcbcbebe=ccbed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [57].

Overlap of [23] cbcbecc=eb with [56] ccbed=cbdce:

Critical pair: cbcbecbdce=ebbed.

Flip LHS and RHS.

Defines rule #43.

Referenced by [70].

Overlap of [23] cbcbecc=eb with [53] ccbec=cbdcdcbe:

Critical pair: cbcbecbdcdcbe=ebbec.

Flip LHS and RHS.

Defines rule #27.

Referenced by [64].

Overlap of [47] ebcbcbec=ebbdcbe with [48] ecbcbec=ebdcbe:

Critical pair: ebcbcbebdcbe=ebbdcbebcbec.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

Referenced by [66], [67], [68].

Overlap of [47] ebcbcbec=ebbdcbe with [54] ecbcbed=ebe:

Critical pair: ebcbcbebe=ebbdcbebcbed.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #42.

Referenced by [61], [62], [63].

Overlap of [28] ebbcbcbec=e with [60] ecbed=ebdce:

Critical pair: ebbcbcbebdce=ebed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #41.

Overlap of [37] cbcbcbecb=c with [60] ecbed=ebdce:

Critical pair: cbcbcbebdce=ced.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [65].

Overlap of [47] ebcbcbec=ebbdcbe with [60] ecbed=ebdce:

Critical pair: ebcbcbebdce=ebbdcbebed.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #40.

Simplify [35] ecbeb=ebbec.

Reduce RHS:

Defines rule #37.

Referenced by [72].

Overlap of [44] cbcbcbcbec=d with [62] ced=cbdcdce:

Critical pair: cbcbcbcbecbdcdce=ded.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [28] ebbcbcbec=e with [59] ecbec=ebdcdcbe:

Critical pair: ebbcbcbebdcdcbe=ebec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [37] cbcbcbecb=c with [59] ecbec=ebdcdcbe:

Critical pair: cbcbcbebdcdcbe=cec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [69].

Overlap of [47] ebcbcbec=ebbdcbe with [59] ecbec=ebdcdcbe:

Critical pair: ebcbcbebdcdcbe=ebbdcbebec.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [44] cbcbcbcbec=d with [67] cec=cbdcdcdcbe:

Critical pair: cbcbcbcbecbdcdcdcbe=dec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [17] cbcbeb=dc with [57] ebbed=cbcbecbdce:

Critical pair: cbcbcbcbecbdce=dcbed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [17] cbcbeb=dc with [49] ebbcbed=cbcbecbe:

Critical pair: cbcbcbcbecbe=dcbcbed.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [49] ebbcbed=cbcbecbe with [6] db=cbc:

Critical pair: ebbcbecbc=cbcbecbeb.

Reduce LHS:

Reduce RHS:

Defines rule #7.

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

Overlap of [17] cbcbeb=dc with [50] ebbcbec=cbcbecbdcbe:

Critical pair: cbcbcbcbecbdcbe=dcbcbec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Simplify [39] ebeb=ebbdcbec.

Reduce RHS:

Defines rule #36.

Simplify [40] ceb=cbdcbec.

Reduce RHS:

Defines rule #10.

Simplify [41] eeb=ebdcbec.

Reduce RHS:

Defines rule #35.

Simplify [45] deb=cbcdcbec.

Reduce RHS:

Defines rule #12.