Certificate for #3034 ⟨a, b | aabaabaabba=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. baabaabb=d

Axiom: aabaabaabba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [13], [14], [17], [18], [20], [26], [28], [32], [34].

Axiom: baabaabb=d.

Defines rule #11.

Referenced by [4], [11], [14], [16], [27].

Overlap of [1] aabaabaabba=1 with [3] baabaabb=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 [15], [17], [24], [27], [28], [29].

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], [11].

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

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [13], [17], [18], [28], [34].

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], [18], [23], [30], [33].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [12], [14], [19], [23], [30], [33].

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

Critical pair: baabaabd=daabaabb.

Reduce RHS:

Defines rule #9.

Referenced by [12], [17], [21], [28].

Overlap of [11] baabaabd=aadbaabb with [10] dc=1:

Critical pair: baabaab=aadbaabbc.

Flip LHS and RHS.

Referenced by [13].

Overlap of [2] aaa=c with [12] aadbaabbc=baabaab:

Critical pair: abaabaab=cdbaabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [14], [15], [22], [24].

Overlap of [3] baabaabb=d with [13] baabbc=abaabaab:

Critical pair: baaabaabaab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17].

Overlap of [13] baabbc=abaabaab with [5] ca=ac:

Critical pair: baabbac=abaabaaba.

Referenced by [25].

Overlap of [14] bcbaabaab=1 with [3] baabaabb=d:

Critical pair: bcbaad=aabb.

Referenced by [18], [19].

Overlap of [14] bcbaabaab=1 with [11] baabaabd=aadbaabb:

Critical pair: bcbaaaadbaabb=aabd.

Reduce LHS:

Defines rule #19.

Overlap of [16] bcbaad=aabb with [9] da=ad:

Critical pair: bcbaaad=aabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20], [21], [22], [25].

Overlap of [16] bcbaad=aabb with [10] dc=1:

Critical pair: bcbaa=aabbc.

Defines rule #7.

Referenced by [24].

Overlap of [2] aaa=c with [18] aabba=bcb:

Critical pair: abcb=cbba.

Flip LHS and RHS.

Referenced by [23].

Overlap of [18] aabba=bcb with [11] baabaabd=aadbaabb:

Critical pair: aabaadbaabb=bcbabaabd.

Flip LHS and RHS.

Defines rule #15.

Overlap of [18] aabba=bcb with [13] baabbc=abaabaab:

Critical pair: aababaabaab=bcbabbc.

Flip LHS and RHS.

Defines rule #13.

Overlap of [10] dc=1 with [20] cbba=abcb:

Critical pair: dabcb=bba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [31].

Overlap of [19] bcbaa=aabbc with [13] baabbc=abaabaab:

Critical pair: bcabaabaab=aabbcbbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [15] baabbac=abaabaaba with [18] aabba=bcb:

Critical pair: bbcbc=abaabaaba.

Flip LHS and RHS.

Referenced by [26], [27], [28], [29].

Overlap of [2] aaa=c with [25] abaabaaba=bbcbc:

Critical pair: aabbcbc=cbaabaaba.

Flip LHS and RHS.

Referenced by [30].

Overlap of [25] abaabaaba=bbcbc with [3] baabaabb=d:

Critical pair: abaad=bbcbcabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [25] abaabaaba=bbcbc with [11] baabaabd=aadbaabb:

Critical pair: abaaaadbaabb=bbcbcabd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [25] abaabaaba=bbcbc with [25] abaabaaba=bbcbc:

Critical pair: ababbcbc=bbcbcaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [10] dc=1 with [26] cbaabaaba=aabbcbc:

Critical pair: daabbcbc=baabaaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [31].

Overlap of [23] bba=adbcb with [30] baabaaba=aadbbcbc:

Critical pair: baadbbcbc=adbcbabaaba.

Flip LHS and RHS.

Referenced by [34].

Overlap of [2] aaa=c with [24] aabbcbbc=bacbaabaab:

Critical pair: abacbaabaab=cbbcbbc.

Flip LHS and RHS.

Referenced by [33].

Overlap of [10] dc=1 with [32] cbbcbbc=abacbaabaab:

Critical pair: dabacbaabaab=bbcbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [2] aaa=c with [31] adbcbabaaba=baadbbcbc:

Critical pair: aabaadbbcbc=cdbcbabaaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.