Certificate for #3182 ⟨a, b | abaaaabbaba=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. babaab=c
  2. abc=d

Axiom: abaaaabbaba=1.

Referenced by [5], [6], [7], [8], [9], [10], [11], [14], [15], [16].

Axiom: babaab=c.

Referenced by [4], [7], [8], [12], [13], [25].

Axiom: abc=d.

Referenced by [4], [7], [9], [14], [26], [30].

Overlap of [2] babaab=c with [3] abc=d:

Critical pair: babad=cc.

Referenced by [21].

Overlap of [1] abaaaabbaba=1 with [1] abaaaabbaba=1:

Critical pair: abaaaabb=aaabbaba.

Flip LHS and RHS.

Referenced by [6], [33].

Overlap of [1] abaaaabbaba=1 with [1] abaaaabbaba=1:

Critical pair: abaaaabbab=baaaabbaba.

Reduce RHS:

Referenced by [9], [10], [11], [15], [16].

Overlap of [1] abaaaabbaba=1 with [2] babaab=c:

Critical pair: abaaaabc=ab.

Reduce LHS:

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

Overlap of [1] abaaaabbaba=1 with [2] babaab=c:

Critical pair: abaaaabbac=baab.

Referenced by [34].

Overlap of [1] abaaaabbaba=1 with [3] abc=d:

Critical pair: abaaaabbabd=bc.

Reduce LHS:

Referenced by [17].

Overlap of [1] abaaaabbaba=1 with [7] abaaad=ab:

Critical pair: abaaaabbab=aad.

Reduce LHS:

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

Overlap of [1] abaaaabbaba=1 with [7] abaaad=ab:

Critical pair: abaaaabbabab=baaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [2] babaab=c with [7] abaaad=ab:

Critical pair: babaab=caaad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [2] babaab=c with [11] baaad=aadab:

Critical pair: babaaaadab=caaad.

Reduce RHS:

Referenced by [14].

Overlap of [1] abaaaabbaba=1 with [13] babaaaadab=c:

Critical pair: abaaaabc=aaadab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [14] aaadab=ab with [1] abaaaabbaba=1:

Critical pair: aaad=abaaaabbaba.

Reduce RHS:

Referenced by [18].

Overlap of [1] abaaaabbaba=1 with [6] abaaaabbab=baabaaaabb:

Critical pair: baabaaaabba=1.

Reduce LHS:

Referenced by [18], [19], [22], [32], [33].

Overlap of [9] baabaaaabbd=bc with [10] baabaaaabb=aad:

Critical pair: aadd=bc.

Flip LHS and RHS.

Referenced by [24].

Simplify [15] aaad=aada.

Reduce RHS:

Referenced by [20].

Overlap of [16] aada=1 with [16] aada=1:

Critical pair: aad=ada.

Referenced by [20].

Simplify [18] aaad=1.

Reduce LHS:

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

Overlap of [4] babad=cc with [20] adaa=1:

Critical pair: bab=ccaa.

Defines rule #6.

Referenced by [25], [26], [27], [33], [35], [49], [51].

Overlap of [20] adaa=1 with [16] aada=1:

Critical pair: ad=da.

Defines rule #1.

Referenced by [23], [24], [31], [33], [39], [40], [41], [51], [52], [53].

Overlap of [20] adaa=1 with [22] ad=da:

Critical pair: daaa=1.

Defines rule #2.

Referenced by [36], [38], [39], [40], [41], [46], [47], [52], [56], [58], [59].

Simplify [17] bc=aadd.

Reduce RHS:

Defines rule #3.

Referenced by [28], [33], [40].

Overlap of [2] babaab=c with [21] bab=ccaa:

Critical pair: ccaaaab=c.

Referenced by [30].

Overlap of [21] bab=ccaa with [3] abc=d:

Critical pair: bd=ccaac.

Flip LHS and RHS.

Defines rule #10.

Referenced by [28], [29], [42], [57].

Overlap of [21] bab=ccaa with [21] bab=ccaa:

Critical pair: baccaa=ccaaab.

Flip LHS and RHS.

Defines rule #17.

Overlap of [24] bc=ddaa with [26] ccaac=bd:

Critical pair: bbd=ddaacaac.

Referenced by [36].

Overlap of [26] ccaac=bd with [26] ccaac=bd:

Critical pair: ccaabd=bdcaac.

Referenced by [38].

Overlap of [3] abc=d with [25] ccaaaab=c:

Critical pair: abc=dcaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [22] ad=da with [30] dcaaaab=d:

Critical pair: ad=dacaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [16] aada=1 with [31] dacaaaab=da:

Critical pair: aada=caaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [35], [39], [44], [48].

Overlap of [5] aaabbaba=abaaaabb with [21] bab=ccaa:

Critical pair: aaabccaaa=abaaaabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [8] abaaaabbac=baab with [33] abaaaabb=daacaaa:

Critical pair: daacaaaac=baab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [39], [40].

Overlap of [32] caaaab=1 with [21] bab=ccaa:

Critical pair: caaaaccaa=ab.

Referenced by [37], [43].

Overlap of [28] bbd=ddaacaac with [23] daaa=1:

Critical pair: bb=ddaacaacaaa.

Defines rule #5.

Overlap of [35] caaaaccaa=ab with [35] caaaaccaa=ab:

Critical pair: caaaacab=abaaccaa.

Defines rule #14.

Overlap of [29] ccaabd=bdcaac with [23] daaa=1:

Critical pair: ccaab=bdcaacaaa.

Defines rule #15.

Overlap of [32] caaaab=1 with [34] baab=daacaaaac:

Critical pair: caaaadaacaaaac=aab.

Reduce LHS:

Defines rule #12.

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

Overlap of [34] baab=daacaaaac with [24] bc=ddaa:

Critical pair: baaddaa=daacaaaacc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [22] ad=da with [40] daacaaaacc=bda:

Critical pair: abda=daaacaaaacc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [42].

Overlap of [41] caaaacc=abda with [26] ccaac=bd:

Critical pair: caaaacbd=abdacaac.

Referenced by [46].

Overlap of [35] caaaaccaa=ab with [39] caaacaaaac=aab:

Critical pair: caaaacaab=abacaaaac.

Defines rule #16.

Overlap of [39] caaacaaaac=aab with [32] caaaab=1:

Critical pair: caaacaaaa=aabaaaab.

Flip LHS and RHS.

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

Overlap of [39] caaacaaaac=aab with [39] caaacaaaac=aab:

Critical pair: caaacaaaaaab=aabaaacaaaac.

Defines rule #22.

Overlap of [42] caaaacbd=abdacaac with [23] daaa=1:

Critical pair: caaaacb=abdacaacaaa.

Defines rule #13.

Overlap of [23] daaa=1 with [44] aabaaaab=caaacaaaa:

Critical pair: dacaaacaaaa=baaaab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [51].

Overlap of [32] caaaab=1 with [44] aabaaaab=caaacaaaa:

Critical pair: caacaaacaaaa=aaaab.

Referenced by [52].

Overlap of [44] aabaaaab=caaacaaaa with [21] bab=ccaa:

Critical pair: aabaaaaccaa=caaacaaaaab.

Flip LHS and RHS.

Defines rule #20.

Overlap of [44] aabaaaab=caaacaaaa with [44] aabaaaab=caaacaaaa:

Critical pair: aabaacaaacaaaa=caaacaaaaaaaab.

Flip LHS and RHS.

Defines rule #24.

Overlap of [21] bab=ccaa with [47] baaaab=dacaaacaaaa:

Critical pair: badacaaacaaaa=ccaaaaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [48] caacaaacaaaa=aaaab with [22] ad=da:

Critical pair: caacaaacaaada=aaaabd.

Reduce LHS:

Referenced by [53], [54], [55].

Overlap of [52] caacaaaca=aaaabd with [22] ad=da:

Critical pair: caacaaacda=aaaabdd.

Referenced by [56].

Overlap of [52] caacaaaca=aaaabd with [39] caaacaaaac=aab:

Critical pair: caacaaaaab=aaaabdaacaaaac.

Defines rule #19.

Overlap of [52] caacaaaca=aaaabd with [52] caacaaaca=aaaabd:

Critical pair: caacaaaaaaabd=aaaabdacaaaca.

Referenced by [59].

Overlap of [53] caacaaacda=aaaabdd with [23] daaa=1:

Critical pair: caacaaac=aaaabddaa.

Defines rule #11.

Referenced by [57].

Overlap of [56] caacaaac=aaaabddaa with [26] ccaac=bd:

Critical pair: caacaaabd=aaaabddaacaac.

Referenced by [58].

Overlap of [57] caacaaabd=aaaabddaacaac with [23] daaa=1:

Critical pair: caacaaab=aaaabddaacaacaaa.

Defines rule #18.

Overlap of [55] caacaaaaaaabd=aaaabdacaaaca with [23] daaa=1:

Critical pair: caacaaaaaaab=aaaabdacaaacaaaa.

Defines rule #23.