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

Completion settings:

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

Axiom: aaabaabbaba=1.

Referenced by [4].

Axiom: abbab=c.

Referenced by [4], [8], [9], [14], [18], [22].

Axiom: abac=d.

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

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

Critical pair: aaabaca=1.

Reduce LHS:

Referenced by [5], [6], [7], [10], [12].

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

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [7], [12].

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

Critical pair: aadd=bac.

Flip LHS and RHS.

Defines rule #4.

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

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

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [9], [10], [11], [16], [17], [25], [29], [34], [36], [37], [38], [42], [44].

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

Critical pair: abbd=cac.

Flip LHS and RHS.

Defines rule #5.

Referenced by [10], [29], [34], [36].

Overlap of [7] da=ad with [2] abbab=c:

Critical pair: dc=adbbab.

Flip LHS and RHS.

Referenced by [13].

Overlap of [6] bac=aadd with [8] cac=abbd:

Critical pair: baabbd=aaddac.

Reduce RHS:

Referenced by [11], [15].

Overlap of [10] baabbd=dc with [7] da=ad:

Critical pair: baabbad=dca.

Referenced by [16].

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

Critical pair: aaad=1.

Defines rule #2.

Referenced by [13], [17], [21], [23], [24], [25], [26], [28], [29], [30], [31], [34], [38], [39], [40], [41], [42], [43], [44].

Overlap of [12] aaad=1 with [9] adbbab=dc:

Critical pair: aadc=bbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [14], [15], [20], [26].

Overlap of [13] bbab=aadc with [2] abbab=c:

Critical pair: bbc=aadcbab.

Defines rule #13.

Overlap of [13] bbab=aadc with [10] baabbd=dc:

Critical pair: bbadc=aadcaabbd.

Defines rule #16.

Overlap of [11] baabbad=dca with [7] da=ad:

Critical pair: baabbaad=dcaa.

Referenced by [17].

Overlap of [16] baabbaad=dcaa with [7] da=ad:

Critical pair: baabbaaad=dcaaa.

Reduce LHS:

Defines rule #9.

Referenced by [18], [19], [20], [32].

Overlap of [17] baabb=dcaaa with [2] abbab=c:

Critical pair: bac=dcaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [17] baabb=dcaaa with [6] bac=aadd:

Critical pair: baabaadd=dcaaaac.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [17] baabb=dcaaa with [13] bbab=aadc:

Critical pair: baabaadc=dcaaabab.

Defines rule #19.

Overlap of [12] aaad=1 with [18] dcaaaab=aadd:

Critical pair: aaaaadd=caaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [22], [23], [25], [31].

Overlap of [21] caaaab=aad with [2] abbab=c:

Critical pair: caaac=aadbab.

Defines rule #6.

Referenced by [23].

Overlap of [22] caaac=aadbab with [21] caaaab=aad:

Critical pair: caaaaad=aadbabaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [12] aaad=1 with [23] aadbabaaaab=caa:

Critical pair: acaa=babaaaab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [25], [26], [27], [33].

Overlap of [21] caaaab=aad with [24] babaaaab=acaa:

Critical pair: caaaaacaa=aadabaaaab.

Reduce RHS:

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

Overlap of [24] babaaaab=acaa with [13] bbab=aadc:

Critical pair: babaaaaaadc=acaabab.

Reduce LHS:

Defines rule #21.

Overlap of [24] babaaaab=acaa with [24] babaaaab=acaa:

Critical pair: babaaaaacaa=acaaabaaaab.

Referenced by [40].

Overlap of [12] aaad=1 with [19] dcaaaac=baabaadd:

Critical pair: aaabaabaadd=caaaac.

Flip LHS and RHS.

Defines rule #7.

Referenced by [38].

Overlap of [19] dcaaaac=baabaadd with [8] cac=abbd:

Critical pair: dcaaaaabbd=baabaaddac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [25] caaaaacaa=baaaab with [12] aaad=1:

Critical pair: caaaaac=baaaabad.

Defines rule #8.

Referenced by [34], [35], [36], [38].

Overlap of [25] caaaaacaa=baaaab with [21] caaaab=aad:

Critical pair: caaaaaaad=baaaabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [32], [33].

Overlap of [17] baabb=dcaaa with [31] baaaabaab=caaaa:

Critical pair: baabcaaaa=dcaaaaaaabaab.

Referenced by [41].

Overlap of [24] babaaaab=acaa with [31] baaaabaab=caaaa:

Critical pair: babaaaacaaaa=acaaaaaabaab.

Referenced by [43].

Overlap of [8] cac=abbd with [30] caaaaac=baaaabad:

Critical pair: cabaaaabad=abbdaaaaac.

Reduce RHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [25] caaaaacaa=baaaab with [30] caaaaac=baaaabad:

Critical pair: caaaaabaaaabad=baaaabaaac.

Flip LHS and RHS.

Defines rule #22.

Overlap of [30] caaaaac=baaaabad with [8] cac=abbd:

Critical pair: caaaaaabbd=baaaabadac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [7] da=ad with [34] abbaac=cabaaaabad:

Critical pair: dcabaaaabad=adbbaac.

Flip LHS and RHS.

Referenced by [39].

Overlap of [30] caaaaac=baaaabad with [28] caaaac=aaabaabaadd:

Critical pair: caaaaaaaabaabaadd=baaaabadaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [12] aaad=1 with [37] adbbaac=dcabaaaabad:

Critical pair: aadcabaaaabad=bbaac.

Flip LHS and RHS.

Defines rule #17.

Overlap of [27] babaaaaacaa=acaaabaaaab with [12] aaad=1:

Critical pair: babaaaaac=acaaabaaaabad.

Defines rule #24.

Overlap of [32] baabcaaaa=dcaaaaaaabaab with [12] aaad=1:

Critical pair: baabca=dcaaaaaaabaabd.

Referenced by [42].

Overlap of [41] baabca=dcaaaaaaabaabd with [12] aaad=1:

Critical pair: baabc=dcaaaaaaabaabdaad.

Reduce RHS:

Defines rule #14.

Overlap of [33] babaaaacaaaa=acaaaaaabaab with [12] aaad=1:

Critical pair: babaaaaca=acaaaaaabaabd.

Referenced by [44].

Overlap of [43] babaaaaca=acaaaaaabaabd with [12] aaad=1:

Critical pair: babaaaac=acaaaaaabaabdaad.

Reduce RHS:

Defines rule #23.