Certificate for #1451 ⟨a, b | aabbababba=1⟩

Completion settings:

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

Axiom: aabbababba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [16], [17], [18], [20], [21], [24], [26], [31], [35], [38], [41].

Axiom: bbababb=d.

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

Overlap of [1] aabbababba=1 with [3] bbababb=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 [14], [27], [28], [36], [43].

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

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], [17], [24], [32], [33], [39], [40], [42].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [18], [20], [21], [24], [26], [27], [29], [35].

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

Critical pair: bbabad=dababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

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

Critical pair: cbbabda=ababb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [27], [30].

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

Critical pair: aacbbabda=cbabb.

Reduce LHS:

Referenced by [15].

Overlap of [11] dc=1 with [14] caabbabda=cbabb:

Critical pair: dcbabb=aabbabda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [15] aabbabda=babb with [2] aaa=c:

Critical pair: aabbabdc=babbaa.

Reduce LHS:

Defines rule #8.

Referenced by [17], [19].

Overlap of [16] aabbab=babbaa with [3] bbababb=d:

Critical pair: aad=babbaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18], [20], [22].

Overlap of [17] babbcbb=daa with [17] babbcbb=daa:

Critical pair: babbcbdaa=daaabbcbb.

Reduce RHS:

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

Overlap of [16] aabbab=babbaa with [18] babbcbdaa=bbcbb:

Critical pair: aabbbcbb=babbaabcbdaa.

Defines rule #15.

Overlap of [17] babbcbb=daa with [18] babbcbdaa=bbcbb:

Critical pair: babbcbbbcbb=daaabbcbdaa.

Reduce LHS:

Reduce RHS:

Referenced by [23], [24], [25].

Overlap of [18] babbcbdaa=bbcbb with [2] aaa=c:

Critical pair: babbcbdc=bbcbba.

Reduce LHS:

Referenced by [22], [25], [34].

Overlap of [17] babbcbb=daa with [21] babbcb=bbcbba:

Critical pair: bbcbbab=daa.

Defines rule #14.

Referenced by [25].

Overlap of [9] cd=1 with [20] daabcbb=bbcbdaa:

Critical pair: cbbcbdaa=aabcbb.

Flip LHS and RHS.

Defines rule #9.

Overlap of [10] ad=da with [20] daabcbb=bbcbdaa:

Critical pair: abbcbdaa=daaabcbb.

Reduce RHS:

Referenced by [26].

Overlap of [18] babbcbdaa=bbcbb with [20] daabcbb=bbcbdaa:

Critical pair: babbcbbbcbdaa=bbcbbbcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [24] abbcbdaa=bcbb with [2] aaa=c:

Critical pair: abbcbdc=bcbba.

Reduce LHS:

Defines rule #6.

Referenced by [27], [37].

Overlap of [13] ababb=cbbabda with [26] abbcb=bcbba:

Critical pair: abbcbba=cbbabdacb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [28], [29], [30].

Overlap of [5] ac=ca with [27] cbbabab=bcbbaba:

Critical pair: abcbbaba=cabbabab.

Flip LHS and RHS.

Defines rule #12.

Overlap of [11] dc=1 with [27] cbbabab=bcbbaba:

Critical pair: dbcbbaba=bbabab.

Referenced by [31].

Overlap of [27] cbbabab=bcbbaba with [13] ababb=cbbabda:

Critical pair: cbbabcbbabda=bcbbabaabb.

Referenced by [35].

Overlap of [29] dbcbbaba=bbabab with [2] aaa=c:

Critical pair: dbcbbabc=bbababaa.

Referenced by [32].

Overlap of [31] dbcbbabc=bbababaa with [9] cd=1:

Critical pair: dbcbbab=bbababaad.

Reduce RHS:

Defines rule #11.

Referenced by [33], [34].

Overlap of [10] ad=da with [32] dbcbbab=bbababdaa:

Critical pair: abbababdaa=dabcbbab.

Flip LHS and RHS.

Defines rule #13.

Overlap of [32] dbcbbab=bbababdaa with [21] babbcb=bbcbba:

Critical pair: dbcbbbcbba=bbababdaabcb.

Referenced by [38].

Overlap of [30] cbbabcbbabda=bcbbabaabb with [2] aaa=c:

Critical pair: cbbabcbbabdc=bcbbabaabbaa.

Reduce LHS:

Defines rule #16.

Referenced by [36], [37].

Overlap of [5] ac=ca with [35] cbbabcbbab=bcbbabaabbaa:

Critical pair: abcbbabaabbaa=cabbabcbbab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [35] cbbabcbbab=bcbbabaabbaa with [26] abbcb=bcbba:

Critical pair: cbbabcbbbcbba=bcbbabaabbaabcb.

Referenced by [41].

Overlap of [34] dbcbbbcbba=bbababdaabcb with [2] aaa=c:

Critical pair: dbcbbbcbbc=bbababdaabcbaa.

Referenced by [39].

Overlap of [38] dbcbbbcbbc=bbababdaabcbaa with [9] cd=1:

Critical pair: dbcbbbcbb=bbababdaabcbaad.

Reduce RHS:

Defines rule #17.

Referenced by [40].

Overlap of [10] ad=da with [39] dbcbbbcbb=bbababdaabcbdaa:

Critical pair: abbababdaabcbdaa=dabcbbbcbb.

Flip LHS and RHS.

Defines rule #19.

Overlap of [37] cbbabcbbbcbba=bcbbabaabbaabcb with [2] aaa=c:

Critical pair: cbbabcbbbcbbc=bcbbabaabbaabcbaa.

Referenced by [42].

Overlap of [41] cbbabcbbbcbbc=bcbbabaabbaabcbaa with [9] cd=1:

Critical pair: cbbabcbbbcbb=bcbbabaabbaabcbaad.

Reduce RHS:

Defines rule #21.

Referenced by [43].

Overlap of [5] ac=ca with [42] cbbabcbbbcbb=bcbbabaabbaabcbdaa:

Critical pair: abcbbabaabbaabcbdaa=cabbabcbbbcbb.

Flip LHS and RHS.

Defines rule #22.