Certificate for #2972 ⟨a, b | aaabbababba=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. aaaa=c
  2. bbababb=d

Axiom: aaabbababba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [7], [9], [11], [19], [24], [27], [29], [30], [32], [33], [35], [38], [40], [41], [42], [49], [53], [58].

Axiom: bbababb=d.

Referenced by [4], [21], [22], [30], [31].

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

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12], [14], [16].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [12], [15], [24], [35], [39], [43], [45], [50], [54], [59], [60].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10], [11], [13], [14].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

Referenced by [10], [12], [16].

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [15].

Overlap of [7] cada=aa with [4] aaada=1:

Critical pair: cad=aaaada.

Reduce RHS:

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

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [16], [17].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Referenced by [15], [16].

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaada=1 with [8] aaad=aada:

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [17], [18], [23], [26].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [15] cddaa=ada with [16] cd=1:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [19].

Simplify [17] adaaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [20], [27], [28], [29], [32], [33], [35], [38], [39], [40], [42], [49], [53], [58].

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [21], [30], [33], [46], [48], [52], [55], [56], [57].

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

Critical pair: bbabad=dababb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23].

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

Critical pair: bbababd=dbababb.

Flip LHS and RHS.

Referenced by [25].

Overlap of [16] cd=1 with [21] dababb=bbabda:

Critical pair: cbbabda=ababb.

Flip LHS and RHS.

Defines rule #7.

Referenced by [24], [25], [31], [35], [39], [44].

Overlap of [2] aaaa=c with [23] ababb=cbbabda:

Critical pair: aaacbbabda=cbabb.

Reduce LHS:

Referenced by [28].

Simplify [22] dbababb=bbababd.

Reduce LHS:

Referenced by [26], [27].

Overlap of [16] cd=1 with [25] dbcbbabda=bbababd:

Critical pair: cbbababd=bcbbabda.

Referenced by [35].

Overlap of [25] dbcbbabda=bbababd with [2] aaaa=c:

Critical pair: dbcbbabdc=bbababdaaa.

Reduce LHS:

Defines rule #11.

Referenced by [46], [47].

Overlap of [19] dc=1 with [24] caaabbabda=cbabb:

Critical pair: dcbabb=aaabbabda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [28] aaabbabda=babb with [2] aaaa=c:

Critical pair: aaabbabdc=babbaaa.

Reduce LHS:

Defines rule #8.

Referenced by [30], [36].

Overlap of [29] aaabbab=babbaaa with [3] bbababb=d:

Critical pair: aaad=babbaaaabb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [3] bbababb=d with [23] ababb=cbbabda:

Critical pair: bbcbbabda=d.

Referenced by [32].

Overlap of [31] bbcbbabda=d with [2] aaaa=c:

Critical pair: bbcbbabdc=daaa.

Reduce LHS:

Defines rule #16.

Referenced by [33], [34], [37], [40].

Overlap of [32] bbcbbab=daaa with [32] bbcbbab=daaa:

Critical pair: bbcbbadaaa=daaabcbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [30] babbcbb=daaa with [32] bbcbbab=daaa:

Critical pair: babbcbdaaa=daaabcbbab.

Reduce RHS:

Referenced by [35], [36], [37], [38].

Overlap of [23] ababb=cbbabda with [34] babbcbdaaa=bbcbb:

Critical pair: abbcbb=cbbabdacbdaaa.

Reduce RHS:

Referenced by [39], [40].

Overlap of [29] aaabbab=babbaaa with [34] babbcbdaaa=bbcbb:

Critical pair: aaabbbcbb=babbaaabcbdaaa.

Defines rule #17.

Overlap of [32] bbcbbab=daaa with [34] babbcbdaaa=bbcbb:

Critical pair: bbcbbbcbb=daaabcbdaaa.

Defines rule #24.

Overlap of [34] babbcbdaaa=bbcbb with [2] aaaa=c:

Critical pair: babbcbdc=bbcbba.

Reduce LHS:

Referenced by [39], [40].

Overlap of [23] ababb=cbbabda with [38] babbcb=bbcbba:

Critical pair: abbcbba=cbbabdacb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [43], [44].

Overlap of [35] abbcbb=bcbbab with [32] bbcbbab=daaa:

Critical pair: abbcbdaaa=bcbbabbcbbab.

Reduce RHS:

Referenced by [41], [42].

Overlap of [2] aaaa=c with [40] abbcbdaaa=bcbb:

Critical pair: aaabcbb=cbbcbdaaa.

Defines rule #9.

Overlap of [40] abbcbdaaa=bcbb with [2] aaaa=c:

Critical pair: abbcbdc=bcbba.

Reduce LHS:

Defines rule #6.

Referenced by [47], [51].

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

Critical pair: abcbbaba=cabbabab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [45].

Overlap of [39] cbbabab=bcbbaba with [23] ababb=cbbabda:

Critical pair: cbbabcbbabda=bcbbabaabb.

Referenced by [49].

Overlap of [5] ac=ca with [43] cabbabab=abcbbaba:

Critical pair: aabcbbaba=caabbabab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [20] ad=da with [27] dbcbbab=bbababdaaa:

Critical pair: abbababdaaa=dabcbbab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [48].

Overlap of [27] dbcbbab=bbababdaaa with [42] abbcb=bcbba:

Critical pair: dbcbbbcbba=bbababdaaabcb.

Referenced by [52].

Overlap of [20] ad=da with [46] dabcbbab=abbababdaaa:

Critical pair: aabbababdaaa=daabcbbab.

Flip LHS and RHS.

Defines rule #15.

Overlap of [44] cbbabcbbabda=bcbbabaabb with [2] aaaa=c:

Critical pair: cbbabcbbabdc=bcbbabaabbaaa.

Reduce LHS:

Defines rule #18.

Referenced by [50], [51].

Overlap of [5] ac=ca with [49] cbbabcbbab=bcbbabaabbaaa:

Critical pair: abcbbabaabbaaa=cabbabcbbab.

Flip LHS and RHS.

Defines rule #20.

Referenced by [54].

Overlap of [49] cbbabcbbab=bcbbabaabbaaa with [42] abbcb=bcbba:

Critical pair: cbbabcbbbcbba=bcbbabaabbaaabcb.

Referenced by [57].

Overlap of [47] dbcbbbcbba=bbababdaaabcb with [20] ad=da:

Critical pair: dbcbbbcbbda=bbababdaaabcbd.

Referenced by [53].

Overlap of [52] dbcbbbcbbda=bbababdaaabcbd with [2] aaaa=c:

Critical pair: dbcbbbcbbdc=bbababdaaabcbdaaa.

Reduce LHS:

Defines rule #19.

Referenced by [55].

Overlap of [5] ac=ca with [50] cabbabcbbab=abcbbabaabbaaa:

Critical pair: aabcbbabaabbaaa=caabbabcbbab.

Flip LHS and RHS.

Defines rule #22.

Overlap of [20] ad=da with [53] dbcbbbcbb=bbababdaaabcbdaaa:

Critical pair: abbababdaaabcbdaaa=dabcbbbcbb.

Flip LHS and RHS.

Defines rule #21.

Referenced by [56].

Overlap of [20] ad=da with [55] dabcbbbcbb=abbababdaaabcbdaaa:

Critical pair: aabbababdaaabcbdaaa=daabcbbbcbb.

Flip LHS and RHS.

Defines rule #23.

Overlap of [51] cbbabcbbbcbba=bcbbabaabbaaabcb with [20] ad=da:

Critical pair: cbbabcbbbcbbda=bcbbabaabbaaabcbd.

Referenced by [58].

Overlap of [57] cbbabcbbbcbbda=bcbbabaabbaaabcbd with [2] aaaa=c:

Critical pair: cbbabcbbbcbbdc=bcbbabaabbaaabcbdaaa.

Reduce LHS:

Defines rule #25.

Referenced by [59].

Overlap of [5] ac=ca with [58] cbbabcbbbcbb=bcbbabaabbaaabcbdaaa:

Critical pair: abcbbabaabbaaabcbdaaa=cabbabcbbbcbb.

Flip LHS and RHS.

Defines rule #26.

Referenced by [60].

Overlap of [5] ac=ca with [59] cabbabcbbbcbb=abcbbabaabbaaabcbdaaa:

Critical pair: aabcbbabaabbaaabcbdaaa=caabbabcbbbcbb.

Flip LHS and RHS.

Defines rule #27.