Certificate for #682 ⟨a, b | aabbababa=1⟩

Completion settings:

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

Axiom: aabbababa=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [17], [18], [19], [22], [25], [27].

Axiom: bbabab=d.

Defines rule #13.

Referenced by [4], [12], [17].

Overlap of [1] aabbababa=1 with [3] bbabab=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.

Defines rule #3.

Referenced by [16], [19], [20], [24], [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.

Referenced by [8], [9], [10], [11].

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

Critical pair: cd=aada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: adaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [17], [23], [26], [28].

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

Critical pair: aadada=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12], [14], [23], [26], [28].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [21].

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

Critical pair: bbabad=dbabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [14].

Overlap of [9] cd=1 with [12] dbabab=bbabda:

Critical pair: cbbabda=babab.

Referenced by [15].

Overlap of [10] ad=da with [12] dbabab=bbabda:

Critical pair: abbabda=dababab.

Flip LHS and RHS.

Defines rule #11.

Overlap of [13] cbbabda=babab with [2] aaa=c:

Critical pair: cbbabdc=bababaa.

Reduce LHS:

Defines rule #8.

Referenced by [16], [17], [18], [20].

Overlap of [5] ac=ca with [15] cbbab=bababaa:

Critical pair: abababaa=cabbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [24].

Overlap of [15] cbbab=bababaa with [3] bbabab=d:

Critical pair: cd=bababaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] cbbab=bababaa with [17] bababcb=1:

Critical pair: cbba=bababaaababcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [19], [20].

Overlap of [2] aaa=c with [18] abcb=cbba:

Critical pair: aacbba=cbcb.

Reduce LHS:

Referenced by [21], [24].

Overlap of [15] cbbab=bababaa with [18] abcb=cbba:

Critical pair: cbbcbba=bababaacb.

Reduce RHS:

Referenced by [27].

Overlap of [11] dc=1 with [19] caabba=cbcb:

Critical pair: dcbcb=aabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

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

Critical pair: aabbc=bcbaa.

Referenced by [23].

Overlap of [22] aabbc=bcbaa with [9] cd=1:

Critical pair: aabb=bcbaad.

Reduce RHS:

Defines rule #7.

Overlap of [5] ac=ca with [16] cabbab=abababaa:

Critical pair: aabababaa=caabbab.

Reduce RHS:

Referenced by [25].

Overlap of [24] aabababaa=cbcbb with [2] aaa=c:

Critical pair: aabababc=cbcbba.

Referenced by [26].

Overlap of [25] aabababc=cbcbba with [9] cd=1:

Critical pair: aababab=cbcbbad.

Reduce RHS:

Defines rule #12.

Overlap of [20] cbbcbba=bababcaab with [2] aaa=c:

Critical pair: cbbcbbc=bababcaabaa.

Referenced by [28].

Overlap of [27] cbbcbbc=bababcaabaa with [9] cd=1:

Critical pair: cbbcbb=bababcaabaad.

Reduce RHS:

Defines rule #14.

Referenced by [29].

Overlap of [5] ac=ca with [28] cbbcbb=bababcaabdaa:

Critical pair: abababcaabdaa=cabbcbb.

Flip LHS and RHS.

Defines rule #15.