Certificate for #3074 ⟨a, b | aababbaaaab=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. ba=d

Axiom: aababbaaaab=1.

Referenced by [4].

Axiom: babb=c.

Referenced by [5].

Axiom: ba=d.

Referenced by [4], [5], [6], [8], [9], [10], [16].

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

Critical pair: aadbbaaaab=1.

Reduce LHS:

Referenced by [7].

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

Critical pair: dbb=c.

Referenced by [6], [12].

Overlap of [5] dbb=c with [3] ba=d:

Critical pair: dbd=ca.

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

Simplify [4] aadbdaaab=1.

Reduce LHS:

Referenced by [8], [9], [13], [17].

Overlap of [3] ba=d with [7] aacaaaab=1:

Critical pair: b=dacaaaab.

Flip LHS and RHS.

Referenced by [15].

Overlap of [7] aacaaaab=1 with [3] ba=d:

Critical pair: aacaaaad=a.

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

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

Critical pair: ba=dacaaaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [9] aacaaaad=a with [6] dbd=ca:

Critical pair: aacaaaaca=abd.

Referenced by [19].

Overlap of [10] dacaaaad=d with [5] dbb=c:

Critical pair: dacaaaac=dbb.

Reduce RHS:

Referenced by [13], [14].

Overlap of [12] dacaaaac=c with [7] aacaaaab=1:

Critical pair: dacaa=caaaab.

Flip LHS and RHS.

Referenced by [15], [17].

Overlap of [12] dacaaaac=c with [9] aacaaaad=a:

Critical pair: dacaaa=caaaad.

Flip LHS and RHS.

Referenced by [28].

Simplify [8] dacaaaab=b.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [18], [19], [29].

Overlap of [3] ba=d with [15] b=dadacaa:

Critical pair: dadacaaa=d.

Referenced by [22].

Overlap of [7] aacaaaab=1 with [13] caaaab=dacaa:

Critical pair: aadacaa=1.

Referenced by [20], [21], [23], [24], [31].

Overlap of [6] dbd=ca with [15] b=dadacaa:

Critical pair: ddadacaad=ca.

Referenced by [25].

Simplify [11] aacaaaaca=abd.

Reduce RHS:

Referenced by [30].

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

Critical pair: aadac=dacaa.

Flip LHS and RHS.

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

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

Critical pair: aadaca=adacaa.

Reduce RHS:

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

Simplify [16] dadacaaa=d.

Reduce LHS:

Referenced by [26], [34].

Overlap of [20] dacaa=aadac with [17] aadacaa=1:

Critical pair: dac=aadacdacaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [20] dacaa=aadac with [17] aadacaa=1:

Critical pair: daca=aadacadacaa.

Reduce RHS:

Referenced by [25], [26], [28], [29], [30], [31], [33], [34], [37].

Simplify [18] ddadacaad=ca.

Reduce LHS:

Referenced by [26], [35].

Overlap of [25] ddaaadacd=ca with [24] daca=adac:

Critical pair: ddaaadacadac=caaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [20] dacaa=aadac with [26] caaca=dddac:

Critical pair: dadddac=aadacca.

Flip LHS and RHS.

Referenced by [32], [33].

Simplify [14] caaaad=dacaaa.

Reduce RHS:

Referenced by [34].

Simplify [15] b=dadacaa.

Reduce RHS:

Defines rule #6.

Simplify [19] aacaaaaca=adadacaad.

Reduce RHS:

Referenced by [33].

Overlap of [17] aadacaa=1 with [24] daca=adac:

Critical pair: aaadaca=1.

Reduce LHS:

Defines rule #3.

Referenced by [32], [34], [40], [41], [43], [46].

Overlap of [31] aaaadac=1 with [27] aadacca=dadddac:

Critical pair: aadadddac=ca.

Flip LHS and RHS.

Defines rule #4.

Referenced by [33], [34], [35], [37], [38], [39], [40], [41], [43].

Simplify [30] aacaaaaca=adaaadacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [28] caaaad=aaadac with [33] adaaadacd=aaaadaddadadddac:

Critical pair: caaaaaaadaddadadddac=aaadacaaadacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36], [43].

Simplify [25] ddaaadacd=ca.

Reduce RHS:

Referenced by [36].

Overlap of [35] ddaaadacd=aadadddac with [34] aadacd=aadaddaadaddadadddac:

Critical pair: ddaaadaddaadaddadadddac=aadadddac.

Referenced by [43].

Overlap of [24] daca=adac with [32] ca=aadadddac:

Critical pair: daaadadddac=adac.

Referenced by [38], [39], [40], [41].

Overlap of [37] daaadadddac=adac with [32] ca=aadadddac:

Critical pair: daaadadddaaadadddac=adaca.

Reduce LHS:

Reduce RHS:

Referenced by [39].

Overlap of [38] daaadaddadac=aadac with [32] ca=aadadddac:

Critical pair: daaadaddadaaadadddac=aadaca.

Reduce LHS:

Reduce RHS:

Referenced by [40].

Overlap of [39] daaadaddaadac=aaadac with [32] ca=aadadddac:

Critical pair: daaadaddaadaaadadddac=aaadaca.

Reduce LHS:

Reduce RHS:

Referenced by [41].

Overlap of [40] daaadaddaaadac=1 with [32] ca=aadadddac:

Critical pair: daaadaddaaadaaadadddac=a.

Reduce LHS:

Defines rule #2.

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

Overlap of [41] daaadadd=a with [41] daaadadd=a:

Critical pair: daaadada=aaaadadd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [43].

Overlap of [32] ca=aadadddac with [42] aaaadadd=daaadada:

Critical pair: cdaaadada=aadadddacaaadadd.

Reduce RHS:

Referenced by [44].

Overlap of [43] cdaaadada=dd with [41] daaadadd=a:

Critical pair: cdaaadaa=ddaadadd.

Referenced by [45].

Overlap of [44] cdaaadaa=ddaadadd with [41] daaadadd=a:

Critical pair: cdaaaa=ddaadaddadadd.

Referenced by [46].

Overlap of [45] cdaaaa=ddaadaddadadd with [31] aaaadac=1:

Critical pair: cd=ddaadaddadadddac.

Defines rule #5.