Certificate for #2922 ⟨a, b | aaabaabbaba=1⟩

Completion settings:

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

Axiom: aaabaabbaba=1.

Referenced by [4].

Axiom: abbab=c.

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

Axiom: abac=d.

Referenced by [4], [6], [10].

Overlap of [1] aaabaabbaba=1 with [2] abbab=c:

Critical pair: aaabaca=1.

Reduce LHS:

Referenced by [5], [6], [7], [8], [11].

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

Critical pair: aad=ada.

Referenced by [6], [7], [8], [11], [12].

Overlap of [4] aada=1 with [3] abac=d:

Critical pair: aadd=bac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] aada=1 with [5] aad=ada:

Critical pair: adaa=1.

Referenced by [8], [9].

Overlap of [4] aada=1 with [5] aad=ada:

Critical pair: aadada=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [9], [11], [12], [15], [18], [20], [21], [22], [23], [24], [25], [27], [29], [32], [38], [39], [43], [44], [45].

Simplify [7] adaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [13], [16], [18], [20], [22], [23], [24], [25], [26], [27], [28], [29], [30], [32], [33], [37], [38], [40], [41], [42], [43], [44], [46].

Overlap of [2] abbab=c with [3] abac=d:

Critical pair: abbd=cac.

Flip LHS and RHS.

Defines rule #5.

Referenced by [13], [28], [33], [36].

Overlap of [4] aada=1 with [2] abbab=c:

Critical pair: aadc=bbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [14], [15], [18], [19], [23], [27].

Simplify [6] bac=adad.

Reduce RHS:

Defines rule #4.

Referenced by [13], [17], [18], [32].

Overlap of [12] bac=ddaa with [10] cac=abbd:

Critical pair: baabbd=ddaaac.

Reduce RHS:

Referenced by [15], [16].

Overlap of [11] bbab=daac with [2] abbab=c:

Critical pair: bbc=daacbab.

Defines rule #13.

Overlap of [11] bbab=daac with [13] baabbd=dc:

Critical pair: bbadc=daacaabbd.

Reduce LHS:

Defines rule #18.

Overlap of [13] baabbd=dc with [9] daaa=1:

Critical pair: baabb=dcaaa.

Defines rule #9.

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

Overlap of [16] baabb=dcaaa with [12] bac=ddaa:

Critical pair: baabddaa=dcaaaac.

Flip LHS and RHS.

Referenced by [28], [41].

Overlap of [16] baabb=dcaaa with [11] bbab=daac:

Critical pair: baadaac=dcaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [16] baabb=dcaaa with [11] bbab=daac:

Critical pair: baabdaac=dcaaabab.

Defines rule #21.

Overlap of [8] ad=da with [18] dcaaaab=ddaa:

Critical pair: addaa=dacaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [8] ad=da with [20] dacaaaab=d:

Critical pair: ad=daacaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [8] ad=da with [21] daacaaaab=da:

Critical pair: ada=daaacaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [23], [24], [26], [29], [30].

Overlap of [22] caaaab=daa with [11] bbab=daac:

Critical pair: caaaadaac=daabab.

Reduce LHS:

Defines rule #6.

Referenced by [24], [34].

Overlap of [23] caaac=daabab with [22] caaaab=daa:

Critical pair: caaadaa=daababaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [8] ad=da with [24] daababaaaab=caa:

Critical pair: acaa=daaababaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [26], [27], [31].

Overlap of [22] caaaab=daa with [25] babaaaab=acaa:

Critical pair: caaaaacaa=daaabaaaab.

Reduce RHS:

Referenced by [29], [35].

Overlap of [25] babaaaab=acaa with [11] bbab=daac:

Critical pair: babaaaadaac=acaabab.

Reduce LHS:

Defines rule #19.

Overlap of [17] dcaaaac=baabddaa with [10] cac=abbd:

Critical pair: dcaaaaabbd=baabddaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [26] caaaaacaa=baaaab with [22] caaaab=daa:

Critical pair: caaaaadaa=baaaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [30], [31], [32].

Overlap of [22] caaaab=daa with [29] baaaabaab=caaaa:

Critical pair: caaaacaaaa=daaaaaabaab.

Reduce RHS:

Referenced by [38].

Overlap of [25] babaaaab=acaa with [29] baaaabaab=caaaa:

Critical pair: babaaaacaaaa=acaaaaaabaab.

Referenced by [44].

Overlap of [29] baaaabaab=caaaa with [12] bac=ddaa:

Critical pair: baaaabaaddaa=caaaaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [33], [34], [35], [36], [42].

Overlap of [10] cac=abbd with [32] caaaaac=baaaabda:

Critical pair: cabaaaabda=abbdaaaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [23] caaac=daabab with [32] caaaaac=baaaabda:

Critical pair: caaabaaaabda=daababaaaaac.

Flip LHS and RHS.

Referenced by [43].

Overlap of [26] caaaaacaa=baaaab with [32] caaaaac=baaaabda:

Critical pair: caaaaabaaaabda=baaaabaaac.

Flip LHS and RHS.

Defines rule #20.

Overlap of [32] caaaaac=baaaabda with [10] cac=abbd:

Critical pair: caaaaaabbd=baaaabdaac.

Flip LHS and RHS.

Defines rule #22.

Overlap of [9] daaa=1 with [33] abbaac=cabaaaabda:

Critical pair: daacabaaaabda=bbaac.

Flip LHS and RHS.

Defines rule #16.

Overlap of [30] caaaacaaaa=aaabaab with [8] ad=da:

Critical pair: caaaacaaada=aaabaabd.

Reduce LHS:

Referenced by [39].

Overlap of [38] caaaaca=aaabaabd with [8] ad=da:

Critical pair: caaaacda=aaabaabdd.

Referenced by [40].

Overlap of [39] caaaacda=aaabaabdd with [9] daaa=1:

Critical pair: caaaac=aaabaabddaa.

Defines rule #7.

Referenced by [41], [42].

Overlap of [17] dcaaaac=baabddaa with [40] caaaac=aaabaabddaa:

Critical pair: dcaaaaaaabaabddaa=baabddaaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [32] caaaaac=baaaabda with [40] caaaac=aaabaabddaa:

Critical pair: caaaaaaaabaabddaa=baaaabdaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [8] ad=da with [34] daababaaaaac=caaabaaaabda:

Critical pair: acaaabaaaabda=daaababaaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [31] babaaaacaaaa=acaaaaaabaab with [8] ad=da:

Critical pair: babaaaacaaada=acaaaaaabaabd.

Reduce LHS:

Referenced by [45].

Overlap of [44] babaaaaca=acaaaaaabaabd with [8] ad=da:

Critical pair: babaaaacda=acaaaaaabaabdd.

Referenced by [46].

Overlap of [45] babaaaacda=acaaaaaabaabdd with [9] daaa=1:

Critical pair: babaaaac=acaaaaaabaabddaa.

Defines rule #23.