Certificate for #3121 ⟨a, b | aabbabababa=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. bbababab=d

Axiom: aabbabababa=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

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

Axiom: bbababab=d.

Defines rule #13.

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

Overlap of [1] aabbabababa=1 with [3] bbababab=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], [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.

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

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

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

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

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

Critical pair: bbababad=dbababab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [14].

Overlap of [9] cd=1 with [12] dbababab=bbababda:

Critical pair: cbbababda=bababab.

Referenced by [15].

Overlap of [10] ad=da with [12] dbababab=bbababda:

Critical pair: abbababda=dabababab.

Flip LHS and RHS.

Defines rule #11.

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

Critical pair: cbbababdc=babababaa.

Reduce LHS:

Defines rule #8.

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

Overlap of [5] ac=ca with [15] cbbabab=babababaa:

Critical pair: ababababaa=cabbabab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [24].

Overlap of [15] cbbabab=babababaa with [3] bbababab=d:

Critical pair: cd=babababaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] cbbabab=babababaa with [17] babababcb=1:

Critical pair: cbba=babababaaababcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

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

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

Critical pair: aacbba=cbcb.

Reduce LHS:

Referenced by [21].

Overlap of [15] cbbabab=babababaa with [18] abcb=cbba:

Critical pair: cbbabcbba=babababaacb.

Reduce LHS:

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.

Referenced by [24].

Overlap of [5] ac=ca with [16] cabbabab=ababababaa:

Critical pair: aababababaa=caabbabab.

Reduce RHS:

Referenced by [25].

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

Critical pair: aababababc=cbcbbaba.

Referenced by [26].

Overlap of [25] aababababc=cbcbbaba with [9] cd=1:

Critical pair: aabababab=cbcbbabad.

Reduce RHS:

Defines rule #12.

Overlap of [20] cbbcbbaba=babababcaab with [2] aaa=c:

Critical pair: cbbcbbabc=babababcaabaa.

Referenced by [28], [29].

Overlap of [27] cbbcbbabc=babababcaabaa with [9] cd=1:

Critical pair: cbbcbbab=babababcaabaad.

Reduce RHS:

Defines rule #14.

Referenced by [30].

Overlap of [27] cbbcbbabc=babababcaabaa with [18] abcb=cbba:

Critical pair: cbbcbbcbba=babababcaabaab.

Referenced by [31].

Overlap of [5] ac=ca with [28] cbbcbbab=babababcaabdaa:

Critical pair: ababababcaabdaa=cabbcbbab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [29] cbbcbbcbba=babababcaabaab with [2] aaa=c:

Critical pair: cbbcbbcbbc=babababcaabaabaa.

Referenced by [32].

Overlap of [31] cbbcbbcbbc=babababcaabaabaa with [9] cd=1:

Critical pair: cbbcbbcbb=babababcaabaabaad.

Reduce RHS:

Defines rule #16.

Referenced by [33].

Overlap of [5] ac=ca with [32] cbbcbbcbb=babababcaabaabdaa:

Critical pair: ababababcaabaabdaa=cabbcbbcbb.

Flip LHS and RHS.

Defines rule #17.