Certificate for #3253 ⟨a, b | ababbaabaab=1⟩

Completion settings:

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

Axiom: ababbaabaab=1.

Referenced by [4].

Axiom: babb=c.

Referenced by [5].

Axiom: ab=d.

Referenced by [4], [5], [6], [11], [15], [28], [30].

Overlap of [1] ababbaabaab=1 with [3] ab=d:

Critical pair: dabbaabaab=1.

Reduce LHS:

Referenced by [8].

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

Critical pair: bdb=c.

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

Overlap of [3] ab=d with [5] bdb=c:

Critical pair: ac=ddb.

Flip LHS and RHS.

Referenced by [8], [9], [16], [17], [18], [21], [30], [35].

Overlap of [5] bdb=c with [5] bdb=c:

Critical pair: bdc=cdb.

Flip LHS and RHS.

Referenced by [13], [18], [30].

Simplify [4] ddbadad=1.

Reduce LHS:

Referenced by [9], [10], [11], [14], [17], [34].

Overlap of [8] acadad=1 with [6] ddb=ac:

Critical pair: acadaac=db.

Referenced by [10], [36].

Overlap of [9] acadaac=db with [9] acadaac=db:

Critical pair: acadadb=dbadaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11], [12], [13], [14], [19].

Overlap of [8] acadad=1 with [10] dbadaac=b:

Critical pair: acadab=badaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [20].

Overlap of [5] bdb=c with [10] dbadaac=b:

Critical pair: bb=cadaac.

Referenced by [21].

Overlap of [7] cdb=bdc with [10] dbadaac=b:

Critical pair: cb=bdcadaac.

Flip LHS and RHS.

Referenced by [22].

Overlap of [10] dbadaac=b with [8] acadad=1:

Critical pair: dbada=badad.

Flip LHS and RHS.

Referenced by [15], [16], [17], [18].

Overlap of [3] ab=d with [14] badad=dbada:

Critical pair: adbada=dadad.

Referenced by [24].

Overlap of [5] bdb=c with [14] badad=dbada:

Critical pair: bddbada=cadad.

Reduce LHS:

Referenced by [25].

Overlap of [6] ddb=ac with [14] badad=dbada:

Critical pair: dddbada=acadad.

Reduce LHS:

Reduce RHS:

Referenced by [25], [27], [29], [31], [38].

Overlap of [7] cdb=bdc with [14] badad=dbada:

Critical pair: cddbada=bdcadad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [10] dbadaac=b with [11] badaac=acadd:

Critical pair: dacadd=b.

Flip LHS and RHS.

Referenced by [20], [21], [22], [23], [24], [25], [26], [35], [36], [39].

Overlap of [11] badaac=acadd with [19] b=dacadd:

Critical pair: dacaddadaac=acadd.

Referenced by [40].

Overlap of [12] bb=cadaac with [19] b=dacadd:

Critical pair: dacaddb=cadaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

Simplify [13] bdcadaac=cb.

Reduce RHS:

Referenced by [23].

Overlap of [22] bdcadaac=cdacadd with [19] b=dacadd:

Critical pair: dacadddcadaac=cdacadd.

Reduce LHS:

Referenced by [42].

Overlap of [15] adbada=dadad with [19] b=dacadd:

Critical pair: addacaddada=dadad.

Referenced by [32].

Overlap of [16] bacada=cadad with [19] b=dacadd:

Critical pair: dacaddacada=cadad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [18] bdcadad=cacada with [19] b=dacadd:

Critical pair: dacadddcadad=cacada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [17] dacada=1 with [17] dacada=1:

Critical pair: daca=cada.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [27] cada=daca with [3] ab=d:

Critical pair: cadd=dacab.

Reduce RHS:

Referenced by [29], [30], [31], [33].

Overlap of [27] cada=daca with [17] dacada=1:

Critical pair: ca=dacacada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [28] cadd=dacd with [6] ddb=ac:

Critical pair: caac=dacdb.

Reduce RHS:

Referenced by [37], [43].

Overlap of [28] cadd=dacd with [17] dacada=1:

Critical pair: cad=dacdacada.

Reduce RHS:

Referenced by [32], [34], [35], [36], [37], [38], [39], [40], [41], [42], [43], [44].

Simplify [24] addacaddada=dadad.

Reduce LHS:

Referenced by [33].

Overlap of [28] cadd=dacd with [32] addadacdada=dadad:

Critical pair: cdadad=dacdadacdada.

Flip LHS and RHS.

Referenced by [45].

Overlap of [8] acadad=1 with [31] cad=dac:

Critical pair: adacad=1.

Reduce LHS:

Defines rule #3.

Referenced by [44], [45], [50], [51], [53], [56], [58].

Overlap of [6] ddb=ac with [19] b=dacadd:

Critical pair: dddacadd=ac.

Reduce LHS:

Referenced by [45].

Simplify [9] acadaac=db.

Reduce RHS:

Referenced by [37].

Overlap of [36] acadaac=ddadacd with [31] cad=dac:

Critical pair: adacaac=ddadacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [49], [51], [53], [54].

Overlap of [17] dacada=1 with [31] cad=dac:

Critical pair: dadaca=1.

Referenced by [46].

Simplify [19] b=dacadd.

Reduce RHS:

Referenced by [55].

Simplify [20] dacaddadaac=acadd.

Reduce RHS:

Referenced by [41].

Overlap of [40] dacaddadaac=adacd with [31] cad=dac:

Critical pair: dadacdadaac=adacd.

Referenced by [53].

Simplify [23] dacaddddacaac=cdacadd.

Reduce RHS:

Referenced by [43].

Overlap of [42] dacaddddacaac=cdadacd with [31] cad=dac:

Critical pair: dadacdddacaac=cdadacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [45].

Overlap of [29] dadadacdddacad=ca with [34] adadac=1:

Critical pair: ddddacad=ca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [45], [46], [47], [50], [51], [52], [53], [56], [58].

Overlap of [33] dacdadacdada=cdadad with [43] cdadacd=dadacdddadddc:

Critical pair: dadadacdddadddcada=cdadad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [57].

Simplify [38] dadaca=1.

Reduce LHS:

Referenced by [47].

Overlap of [46] dadaddddadac=1 with [44] ca=ddddadac:

Critical pair: dadaddddadaddddadac=a.

Reduce LHS:

Defines rule #2.

Referenced by [48], [49], [50], [51], [53], [54], [55], [57], [58].

Overlap of [47] dadaddd=a with [47] dadaddd=a:

Critical pair: dadadda=aadaddd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [56].

Overlap of [47] dadaddd=a with [37] ddadacd=adadddc:

Critical pair: dadadadadddc=aadacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [44] ca=ddddadac with [49] aadacd=dadaac:

Critical pair: cdadaac=ddddadacadacd.

Reduce RHS:

Referenced by [51], [52].

Overlap of [37] ddadacd=adadddc with [50] cdadaac=ddddacd:

Critical pair: ddadaddddacd=adadddcadaac.

Reduce LHS:

Reduce RHS:

Referenced by [53].

Overlap of [50] cdadaac=ddddacd with [44] ca=ddddadac:

Critical pair: cdadaaddddadac=ddddacda.

Referenced by [54].

Simplify [41] dadacdadaac=adacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [55], [58].

Overlap of [52] cdadaaddddadac=ddddacda with [37] ddadacd=adadddc:

Critical pair: cdadaaddadadddc=ddddacdad.

Reduce LHS:

Referenced by [56].

Simplify [39] b=dadacd.

Reduce RHS:

Defines rule #6.

Overlap of [54] cdadaadac=ddddacdad with [44] ca=ddddadac:

Critical pair: cdadaadaddddadac=ddddacdada.

Reduce LHS:

Referenced by [57].

Overlap of [56] cdaddadadd=ddddacdada with [47] dadaddd=a:

Critical pair: cdada=ddddacdadad.

Reduce RHS:

Referenced by [58].

Overlap of [57] cdada=ddddaddddaddddaddddadac with [34] adadac=1:

Critical pair: cd=ddddaddddaddddaddddadacdac.

Reduce RHS:

Defines rule #5.