Certificate for #3069 ⟨a, b | aabababbaab=1⟩

Completion settings:

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

Axiom: aabababbaab=1.

Referenced by [4].

Axiom: bb=c.

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

Axiom: ba=d.

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

Overlap of [1] aabababbaab=1 with [3] ba=d:

Critical pair: aadbabbaab=1.

Reduce LHS:

Referenced by [7], [8], [9], [11], [12], [24].

Overlap of [2] bb=c with [2] bb=c:

Critical pair: bc=cb.

Flip LHS and RHS.

Referenced by [13], [25].

Overlap of [2] bb=c with [3] ba=d:

Critical pair: bd=ca.

Referenced by [16].

Overlap of [3] ba=d with [4] aaddcaab=1:

Critical pair: b=daddcaab.

Flip LHS and RHS.

Referenced by [14].

Overlap of [4] aaddcaab=1 with [2] bb=c:

Critical pair: aaddcaac=b.

Referenced by [13], [27].

Overlap of [4] aaddcaab=1 with [3] ba=d:

Critical pair: aaddcaad=a.

Referenced by [10], [11], [18].

Overlap of [3] ba=d with [9] aaddcaad=a:

Critical pair: ba=daddcaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12], [13].

Overlap of [9] aaddcaad=a with [4] aaddcaab=1:

Critical pair: aaddc=adcaab.

Flip LHS and RHS.

Referenced by [21].

Overlap of [10] daddcaad=d with [4] aaddcaab=1:

Critical pair: daddc=ddcaab.

Flip LHS and RHS.

Referenced by [14], [19].

Overlap of [10] daddcaad=d with [8] aaddcaac=b:

Critical pair: daddcb=ddcaac.

Reduce LHS:

Referenced by [23].

Simplify [7] daddcaab=b.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [15], [16], [19], [21], [23], [24], [25], [26], [27].

Overlap of [3] ba=d with [14] b=dadaddc:

Critical pair: dadaddca=d.

Referenced by [17].

Overlap of [6] bd=ca with [14] b=dadaddc:

Critical pair: dadaddcd=ca.

Flip LHS and RHS.

Referenced by [17], [19], [20], [21], [22], [23], [24], [28], [42], [43], [48].

Simplify [15] dadaddca=d.

Reduce LHS:

Referenced by [18], [20], [22], [30], [34], [42].

Overlap of [9] aaddcaad=a with [17] dadadddadaddcd=d:

Critical pair: aaddcaad=aadadddadaddcd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24], [32], [35].

Simplify [12] ddcaab=daddc.

Reduce LHS:

Referenced by [20].

Overlap of [19] dddadaddcdadadaddc=daddc with [16] ca=dadaddcd:

Critical pair: dddadaddcdadadadddadaddcd=daddca.

Reduce LHS:

Reduce RHS:

Referenced by [24], [29], [32], [34], [35], [38], [40], [42].

Simplify [11] adcaab=aaddc.

Reduce LHS:

Referenced by [22].

Overlap of [21] addadaddcdadadaddc=aaddc with [16] ca=dadaddcd:

Critical pair: addadaddcdadadadddadaddcd=aaddca.

Reduce LHS:

Reduce RHS:

Referenced by [29], [35], [43].

Simplify [13] daddbc=ddcaac.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [31], [37].

Overlap of [4] aaddcaab=1 with [16] ca=dadaddcd:

Critical pair: aadddadaddcdab=1.

Reduce LHS:

Defines rule #3.

Referenced by [36], [41], [44], [55], [56], [58], [61].

Simplify [5] cb=bc.

Reduce RHS:

Referenced by [26].

Overlap of [25] cb=dadaddcc with [14] b=dadaddc:

Critical pair: cdadaddc=dadaddcc.

Referenced by [46].

Simplify [8] aaddcaac=b.

Reduce RHS:

Referenced by [28].

Overlap of [27] aaddcaac=dadaddc with [16] ca=dadaddcd:

Critical pair: aadddadaddcdac=dadaddc.

Reduce LHS:

Referenced by [31].

Overlap of [20] dddadaddcdad=dadddadaddcd with [22] addadaddcdad=aadddadaddcd:

Critical pair: dddadaddcdaadddadaddcd=dadddadaddcddadaddcdad.

Flip LHS and RHS.

Referenced by [30], [33].

Overlap of [17] dadadddadaddcd=d with [29] dadddadaddcddadaddcdad=dddadaddcdaadddadaddcd:

Critical pair: dadddadaddcdaadddadaddcd=ddadaddcdad.

Referenced by [31], [32].

Overlap of [30] dadddadaddcdaadddadaddcd=ddadaddcdad with [23] dddadaddcdac=dadddadaddcc:

Critical pair: dadddadaddcdaadadddadaddcc=ddadaddcdadac.

Reduce LHS:

Referenced by [33].

Overlap of [30] dadddadaddcdaadddadaddcd=ddadaddcdad with [20] dddadaddcdad=dadddadaddcd:

Critical pair: dadddadaddcdaadadddadaddcd=ddadaddcdadad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34], [35].

Overlap of [29] dadddadaddcddadaddcdad=dddadaddcdaadddadaddcd with [31] dadddadaddcddadaddc=ddadaddcdadac:

Critical pair: ddadaddcdadacdad=dddadaddcdaadddadaddcd.

Referenced by [49].

Overlap of [20] dddadaddcdad=dadddadaddcd with [32] ddadaddcdadad=dadddadaddcda:

Critical pair: ddadddadaddcda=dadddadaddcdad.

Reduce RHS:

Referenced by [39].

Overlap of [22] addadaddcdad=aadddadaddcd with [32] ddadaddcdadad=dadddadaddcda:

Critical pair: adadddadaddcda=aadddadaddcdad.

Reduce RHS:

Referenced by [36].

Overlap of [35] adadddadaddcda=a with [24] aadaddc=1:

Critical pair: adadddadaddcd=aadaddc.

Reduce RHS:

Referenced by [37], [38], [39], [45].

Overlap of [36] adadddadaddcd=1 with [23] dddadaddcdac=dadddadaddcc:

Critical pair: adadddadaddcdadddadaddcc=ddadaddcdac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [36] adadddadaddcd=1 with [20] dddadaddcdad=dadddadaddcd:

Critical pair: adadddadaddcdadddadaddcd=ddadaddcdad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [43], [50], [51].

Overlap of [36] adadddadaddcd=1 with [34] ddadddadaddcda=d:

Critical pair: adadddadaddcd=dadddadaddcda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40], [41].

Overlap of [20] dddadaddcdad=dadddadaddcd with [39] dadddadaddcda=1:

Critical pair: dddadaddc=dadddadaddcdddadaddcda.

Flip LHS and RHS.

Referenced by [53].

Overlap of [39] dadddadaddcda=1 with [24] aadaddc=1:

Critical pair: dadddadaddcd=adaddc.

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

Overlap of [20] dddadaddcdad=dadddadaddcd with [41] dadddadaddcd=adaddc:

Critical pair: dddadaddcadaddc=dadddadaddcdddadaddcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [38] ddadaddcdad=adddadaddcd with [22] addadaddcdad=aadddadaddcd:

Critical pair: ddadaddcdaadddadaddcd=adddadaddcddadaddcdad.

Reduce RHS:

Referenced by [49].

Overlap of [24] aadaddc=1 with [42] adaddcddadaddcd=ddddaddc:

Critical pair: addddaddc=ddadaddcd.

Flip LHS and RHS.

Referenced by [47].

Overlap of [36] adadddadaddcd=1 with [42] adaddcddadaddcd=ddddaddc:

Critical pair: adadddddddaddc=dadaddcd.

Flip LHS and RHS.

Referenced by [47], [48], [49], [51], [52], [54].

Overlap of [41] dadddadaddcd=adaddc with [42] adaddcddadaddcd=ddddaddc:

Critical pair: dadddddddaddc=adaddcdadaddcd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [50].

Simplify [44] ddadaddcd=addddaddc.

Reduce LHS:

Referenced by [49], [50], [51], [52], [53], [54], [55], [56].

Simplify [16] ca=dadaddcd.

Reduce RHS:

Defines rule #5.

Referenced by [50], [52], [53], [55], [56], [58].

Simplify [33] ddadaddcdadacdad=dddadaddcdaadddadaddcd.

Reduce RHS:

Referenced by [50].

Overlap of [49] ddadaddcdadacdad=daddddaddddaddc with [38] ddadaddcdad=adddadaddcd:

Critical pair: adddadaddcdacdad=daddddaddddaddc.

Reduce LHS:

Referenced by [58].

Simplify [38] ddadaddcdad=adddadaddcd.

Reduce RHS:

Referenced by [52].

Overlap of [51] ddadaddcdad=adaddddaddc with [45] dadaddcd=adadddddddaddc:

Critical pair: dadadddddddaddcad=adaddddaddc.

Reduce LHS:

Referenced by [58].

Overlap of [40] dadddadaddcdddadaddcda=dddadaddc with [41] dadddadaddcd=adaddc:

Critical pair: adaddcddadaddcda=dddadaddc.

Reduce LHS:

Referenced by [55].

Overlap of [41] dadddadaddcd=adaddc with [45] dadaddcd=adadddddddaddc:

Critical pair: daddadadddddddaddc=adaddc.

Reduce LHS:

Referenced by [55], [56].

Overlap of [54] dadaddddaddc=adaddc with [48] ca=adadddddddaddc:

Critical pair: dadaddddaddadadddddddaddc=adaddca.

Reduce LHS:

Reduce RHS:

Referenced by [56].

Overlap of [55] dadadddadaddc=1 with [48] ca=adadddddddaddc:

Critical pair: dadadddadaddadadddddddaddc=a.

Reduce LHS:

Defines rule #1.

Referenced by [57], [58], [59], [60].

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

Critical pair: dadadda=aadaddd.

Flip LHS and RHS.

Defines rule #2.

Referenced by [58].

Overlap of [48] ca=adadddddddaddc with [57] aadaddd=dadadda:

Critical pair: cdadadda=adadddddddaddcadaddd.

Reduce RHS:

Referenced by [59].

Overlap of [58] cdadadda=d with [56] dadaddd=a:

Critical pair: cdadada=ddaddd.

Referenced by [60].

Overlap of [59] cdadada=ddaddd with [56] dadaddd=a:

Critical pair: cdaa=ddadddddd.

Referenced by [61].

Overlap of [60] cdaa=ddadddddd with [24] aadaddc=1:

Critical pair: cd=ddadddddddaddc.

Defines rule #4.