Certificate for #3068 ⟨a, b | aababababba=1⟩

Completion settings:

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

Axiom: aababababba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [19], [22], [24], [25], [27], [31].

Axiom: babababb=d.

Defines rule #13.

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

Overlap of [1] aababababba=1 with [3] babababb=d:

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [19], [20], [24], [30], [33].

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

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aad=ada.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [6] cda=a with [4] aada=1:

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [21], [24].

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

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [12], [23], [26], [28], [32].

Overlap of [9] da=ad with [2] aaa=c:

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [15], [18], [23], [26], [28], [32].

Overlap of [3] babababb=d with [3] babababb=d:

Critical pair: babababd=dabababb.

Reduce RHS:

Defines rule #9.

Referenced by [12], [13].

Overlap of [11] babababd=adbababb with [9] da=ad:

Critical pair: babababad=adbababba.

Defines rule #11.

Overlap of [11] babababd=adbababb with [10] dc=1:

Critical pair: bababab=adbababbc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] adbababbc=bababab:

Critical pair: aabababab=cdbababbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [15], [16], [20].

Overlap of [3] babababb=d with [14] bababbc=aabababab:

Critical pair: baaabababab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [17].

Overlap of [14] bababbc=aabababab with [5] ca=ac:

Critical pair: bababbac=aababababa.

Defines rule #10.

Referenced by [24].

Overlap of [15] bcbababab=1 with [3] babababb=d:

Critical pair: bcbad=abb.

Referenced by [18].

Overlap of [17] bcbad=abb with [10] dc=1:

Critical pair: bcba=abbc.

Defines rule #6.

Referenced by [19], [20], [29].

Overlap of [18] bcba=abbc with [2] aaa=c:

Critical pair: bcbc=abbcaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [18] bcba=abbc with [14] bababbc=aabababab:

Critical pair: bcaabababab=abbcbabbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [19] abbaac=bcbc with [8] cd=1:

Critical pair: abbaa=bcbcd.

Reduce RHS:

Referenced by [22].

Overlap of [2] aaa=c with [21] abbaa=bcb:

Critical pair: aabcb=cbbaa.

Flip LHS and RHS.

Referenced by [23].

Overlap of [10] dc=1 with [22] cbbaa=aabcb:

Critical pair: daabcb=bbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [24].

Overlap of [16] bababbac=aababababa with [5] ca=ac:

Critical pair: bababbaac=aababababaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [2] aaa=c with [24] aababababaa=babbcbc:

Critical pair: ababbcbc=cbabababaa.

Flip LHS and RHS.

Referenced by [26].

Overlap of [10] dc=1 with [25] cbabababaa=ababbcbc:

Critical pair: dababbcbc=babababaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [2] aaa=c with [20] ababbcbbc=baacbababab:

Critical pair: aabaacbababab=cbabbcbbc.

Flip LHS and RHS.

Referenced by [28], [29].

Overlap of [10] dc=1 with [27] cbabbcbbc=aabaacbababab:

Critical pair: daabaacbababab=babbcbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [30].

Overlap of [18] bcba=abbc with [27] cbabbcbbc=aabaacbababab:

Critical pair: baabaacbababab=abbcbbcbbc.

Flip LHS and RHS.

Referenced by [31].

Overlap of [28] babbcbbc=aadbaacbababab with [5] ca=ac:

Critical pair: babbcbbac=aadbaacbabababa.

Defines rule #15.

Overlap of [2] aaa=c with [29] abbcbbcbbc=baabaacbababab:

Critical pair: aabaabaacbababab=cbbcbbcbbc.

Flip LHS and RHS.

Referenced by [32].

Overlap of [10] dc=1 with [31] cbbcbbcbbc=aabaabaacbababab:

Critical pair: daabaabaacbababab=bbcbbcbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [33].

Overlap of [32] bbcbbcbbc=aadbaabaacbababab with [5] ca=ac:

Critical pair: bbcbbcbbac=aadbaabaacbabababa.

Defines rule #17.