Certificate for #3827 ⟨a, b | abbbabaaab=a⟩

Completion settings:

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

Axiom: abbbabaaab=a.

Referenced by [5].

Axiom: ab=c.

Referenced by [5], [6], [14], [22].

Axiom: ac=d.

Referenced by [5], [7], [8], [14], [19], [23], [24].

Axiom: bcada=e.

Referenced by [6], [7], [9], [15].

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

Critical pair: cbbabaaab=a.

Reduce LHS:

Referenced by [8], [9], [10], [12], [16].

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

Critical pair: bcadc=eb.

Referenced by [11].

Overlap of [4] bcada=e with [3] ac=d:

Critical pair: bcadd=ec.

Referenced by [10], [17].

Overlap of [3] ac=d with [5] cbbcad=a:

Critical pair: aa=dbbcad.

Referenced by [9], [13].

Overlap of [5] cbbcad=a with [4] bcada=e:

Critical pair: cbe=aa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [5] cbbcad=a with [7] bcadd=ec:

Critical pair: cbec=ad.

Flip LHS and RHS.

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

Simplify [6] bcadc=eb.

Reduce LHS:

Referenced by [12], [20], [31].

Overlap of [11] bccbecc=eb with [5] cbbcad=a:

Critical pair: bccbeca=ebbbcad.

Reduce RHS:

Referenced by [15].

Simplify [8] aa=dbbcad.

Reduce RHS:

Referenced by [14].

Overlap of [13] aa=cbe with [2] ab=c:

Critical pair: ac=cbeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [19], [20], [25], [27], [33], [36], [38], [48].

Overlap of [4] bcada=e with [10] ad=cbec:

Critical pair: bccbeca=e.

Reduce LHS:

Referenced by [26].

Overlap of [5] cbbcad=a with [10] ad=cbec:

Critical pair: cbbccbec=a.

Flip LHS and RHS.

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

Overlap of [7] bcadd=ec with [16] a=cbbccbec:

Critical pair: bccbbccbecdd=ec.

Referenced by [32].

Overlap of [10] ad=cbec with [16] a=cbbccbec:

Critical pair: cbbccbecd=cbec.

Referenced by [19], [32].

Overlap of [3] ac=d with [14] cbeb=d:

Critical pair: ad=dbeb.

Reduce LHS:

Referenced by [20], [21], [26], [31], [32].

Overlap of [11] bccbecc=eb with [14] cbeb=d:

Critical pair: bccbecd=ebbeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [34], [35], [36], [40].

Simplify [16] a=cbbccbec.

Reduce RHS:

Defines rule #15.

Referenced by [22], [23], [24].

Overlap of [2] ab=c with [21] a=cbbcdbeb:

Critical pair: cbbcdbebb=c.

Defines rule #12.

Referenced by [24], [29], [35], [41].

Overlap of [3] ac=d with [21] a=cbbcdbeb:

Critical pair: cbbcdbebc=d.

Referenced by [24], [25].

Overlap of [3] ac=d with [22] cbbcdbebb=c:

Critical pair: ac=dbbcdbebb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30].

Overlap of [23] cbbcdbebc=d with [14] cbeb=d:

Critical pair: cbbcdbebd=dbeb.

Defines rule #11.

Referenced by [39], [40].

Simplify [15] ebbbccbec=e.

Reduce LHS:

Defines rule #22.

Referenced by [27], [28], [29], [30], [34], [37], [38], [39], [41], [48].

Overlap of [14] cbeb=d with [26] ebbbcdbeb=e:

Critical pair: cbe=dbbcdbeb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [34], [35], [36], [38], [39], [40].

Overlap of [26] ebbbcdbeb=e with [26] ebbbcdbeb=e:

Critical pair: ebbbcdbe=ebbcdbeb.

Flip LHS and RHS.

Defines rule #21.

Overlap of [22] cbbcdbebb=c with [26] ebbbcdbeb=e:

Critical pair: cbbcdbe=cbcdbeb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [41], [48].

Overlap of [24] dbbcdbebb=d with [26] ebbbcdbeb=e:

Critical pair: dbbcdbe=dbcdbeb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [38], [39].

Overlap of [11] bccbecc=eb with [19] cbec=dbeb:

Critical pair: bcdbebc=eb.

Defines rule #14.

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

Overlap of [17] bccbbccbecdd=ec with [18] cbbccbecd=cbec:

Critical pair: bccbecd=ec.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [33], [39].

Overlap of [32] ec=bcdbebd with [14] cbeb=d:

Critical pair: ed=bcdbebdbeb.

Flip LHS and RHS.

Referenced by [42].

Overlap of [26] ebbbcdbeb=e with [20] ebbeb=bcdbebd:

Critical pair: ebbbcdbbcdbebd=ebeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37], [43].

Overlap of [22] cbbcdbebb=c with [20] ebbeb=bcdbebd:

Critical pair: cbbcdbbcdbebd=ceb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [27] dbbcdbeb=cbe with [20] ebbeb=bcdbebd:

Critical pair: dbbcdbbcdbebd=cbebeb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [26] ebbbcdbeb=e with [34] ebeb=ebbbccbed:

Critical pair: ebbbcdbebbbccbed=eeb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [30] dbcdbeb=dbbcdbe with [26] ebbbcdbeb=e:

Critical pair: dbcdbe=dbbcdbebbcdbeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [39].

Overlap of [38] dcdbeb=dbcdbe with [26] ebbbcdbeb=e:

Critical pair: dcdbe=dbcdbebbcdbeb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [40], [42].

Overlap of [25] cbbcdbebd=dbeb with [39] dbebdbeb=dcdbe:

Critical pair: cbbcdcdbe=dbebbeb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [43], [44], [45], [46].

Overlap of [29] cbcdbeb=cbbcdbe with [26] ebbbcdbeb=e:

Critical pair: cbcdbe=cbbcdbebbcdbeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [47], [48].

Overlap of [33] bcdbebdbeb=ed with [39] dbebdbeb=dcdbe:

Critical pair: bcdcdbe=ed.

Flip LHS and RHS.

Defines rule #1.

Simplify [34] ebeb=ebbbccbed.

Reduce RHS:

Defines rule #17.

Simplify [35] ceb=cbbccbed.

Reduce RHS:

Defines rule #4.

Simplify [36] deb=dbbccbed.

Reduce RHS:

Defines rule #2.

Simplify [37] eeb=ebbccbed.

Reduce RHS:

Defines rule #16.

Overlap of [31] bcdbebc=eb with [41] ccdbeb=cbcdbe:

Critical pair: bcdbebcbcdbe=ebcdbeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [49].

Overlap of [41] ccdbeb=cbcdbe with [26] ebbbcdbeb=e:

Critical pair: ccdbe=cbcdbebbcdbeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Overlap of [31] bcdbebc=eb with [47] ebcdbeb=ebbcdbe:

Critical pair: bcdbebbcdbe=ebdbeb.

Flip LHS and RHS.

Defines rule #19.