Certificate for #3060 ⟨a, b | aababaabbaa=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. babaabb=d

Axiom: aababaabbaa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [8], [9], [10], [19], [22], [25], [29], [30], [31], [33], [40], [42], [48], [53], [56], [57], [58], [60].

Axiom: babaabb=d.

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

Overlap of [1] aababaabbaa=1 with [3] babaabb=d:

Critical pair: aadaa=1.

Referenced by [6], [7], [9], [10].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [17], [35], [36], [41], [42], [50], [54], [59], [62].

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

Critical pair: aad=daa.

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

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

Critical pair: aada=adaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [2] aaaa=c with [6] aad=daa:

Critical pair: aadaa=cd.

Reduce LHS:

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

Overlap of [4] aadaa=1 with [6] aad=daa:

Critical pair: daaaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [21], [23], [32], [34], [38], [49], [61].

Overlap of [4] aadaa=1 with [6] aad=daa:

Critical pair: aadadaa=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [23], [28], [32], [37], [38], [39], [42], [51], [52], [61].

Simplify [8] dc=cd.

Reduce RHS:

Defines rule #2.

Referenced by [15], [18], [40], [42], [43], [48], [50], [53], [56], [57], [58], [59].

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

Critical pair: babaabd=dabaabb.

Flip LHS and RHS.

Referenced by [13].

Overlap of [9] cd=1 with [12] dabaabb=babaabd:

Critical pair: cbabaabd=abaabb.

Flip LHS and RHS.

Referenced by [14], [20], [28].

Overlap of [3] babaabb=d with [13] abaabb=cbabaabd:

Critical pair: bcbabaabd=d.

Referenced by [15].

Overlap of [14] bcbabaabd=d with [11] dc=1:

Critical pair: bcbabaab=dc.

Reduce RHS:

Referenced by [16], [20], [24].

Overlap of [15] bcbabaab=1 with [15] bcbabaab=1:

Critical pair: bcbabaa=cbabaab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [17], [18], [20], [25], [26], [28], [30], [35].

Overlap of [5] ac=ca with [16] cbabaab=bcbabaa:

Critical pair: abcbabaa=cababaab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [41].

Overlap of [11] dc=1 with [16] cbabaab=bcbabaa:

Critical pair: dbcbabaa=babaab.

Referenced by [19], [20].

Overlap of [18] dbcbabaa=babaab with [2] aaaa=c:

Critical pair: dbcbabc=babaabaa.

Referenced by [38].

Overlap of [18] dbcbabaa=babaab with [16] cbabaab=bcbabaa:

Critical pair: dbbcbabaa=babaabb.

Reduce RHS:

Referenced by [21].

Overlap of [9] cd=1 with [20] dbbcbabaa=d:

Critical pair: cd=bbcbabaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [21] bbcbabaa=1 with [2] aaaa=c:

Critical pair: bbcbabc=aa.

Referenced by [23], [24].

Overlap of [22] bbcbabc=aa with [9] cd=1:

Critical pair: bbcbab=aad.

Reduce RHS:

Defines rule #14.

Referenced by [34], [44], [50], [59].

Overlap of [22] bbcbabc=aa with [15] bcbabaab=1:

Critical pair: bbcba=aababaab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [25], [26], [27], [36].

Overlap of [2] aaaa=c with [24] aababaab=bbcba:

Critical pair: aabbcba=cbabaab.

Reduce RHS:

Referenced by [31].

Overlap of [16] cbabaab=bcbabaa with [24] aababaab=bbcba:

Critical pair: cbabbbcba=bcbabaaabaab.

Referenced by [52].

Overlap of [24] aababaab=bbcba with [24] aababaab=bbcba:

Critical pair: aababbbcba=bbcbaabaab.

Referenced by [51].

Simplify [13] abaabb=cbabaabd.

Reduce RHS:

Defines rule #9.

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

Overlap of [2] aaaa=c with [28] abaabb=bcbabdaa:

Critical pair: aaabcbabdaa=cbaabb.

Referenced by [42].

Overlap of [16] cbabaab=bcbabaa with [28] abaabb=bcbabdaa:

Critical pair: cbababcbabdaa=bcbabaaaabb.

Reduce RHS:

Referenced by [53].

Overlap of [25] aabbcba=bcbabaa with [2] aaaa=c:

Critical pair: aabbcbc=bcbabaaaaa.

Reduce RHS:

Referenced by [32].

Overlap of [31] aabbcbc=bcbabca with [9] cd=1:

Critical pair: aabbcb=bcbabcad.

Reduce RHS:

Referenced by [33], [34], [49].

Overlap of [2] aaaa=c with [32] aabbcb=bcbaba:

Critical pair: aabcbaba=cbbcb.

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

Overlap of [32] aabbcb=bcbaba with [23] bbcbab=daa:

Critical pair: aabbcdaa=bcbababcbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [16] cbabaab=bcbabaa with [33] aabcbaba=cbbcb:

Critical pair: cbabcbbcb=bcbabaacbaba.

Reduce RHS:

Defines rule #16.

Overlap of [24] aababaab=bbcba with [33] aabcbaba=cbbcb:

Critical pair: aababcbbcb=bbcbacbaba.

Reduce RHS:

Defines rule #25.

Overlap of [33] aabcbaba=cbbcb with [10] ad=da:

Critical pair: aabcbabda=cbbcbd.

Referenced by [40].

Overlap of [19] dbcbabc=babaabaa with [9] cd=1:

Critical pair: dbcbab=babaabaad.

Reduce RHS:

Defines rule #7.

Referenced by [39], [45].

Overlap of [10] ad=da with [38] dbcbab=babaabdaa:

Critical pair: ababaabdaa=dabcbab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [46].

Overlap of [37] aabcbabda=cbbcbd with [2] aaaa=c:

Critical pair: aabcbabdc=cbbcbdaaa.

Reduce LHS:

Defines rule #12.

Referenced by [42], [47].

Overlap of [17] cababaab=abcbabaa with [33] aabcbaba=cbbcb:

Critical pair: cababcbbcb=abcbabaacbaba.

Reduce RHS:

Defines rule #20.

Overlap of [29] aaabcbabdaa=cbaabb with [40] aabcbab=cbbcbdaaa:

Critical pair: acbbcbdaaadaa=cbaabb.

Reduce LHS:

Referenced by [43].

Overlap of [11] dc=1 with [42] cabbcbda=cbaabb:

Critical pair: dcbaabb=abbcbda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44], [45], [46], [47], [48].

Overlap of [23] bbcbab=daa with [43] abbcbda=baabb:

Critical pair: bbcbbaabb=daabcbda.

Defines rule #27.

Referenced by [49].

Overlap of [38] dbcbab=babaabdaa with [43] abbcbda=baabb:

Critical pair: dbcbbaabb=babaabdaabcbda.

Defines rule #18.

Overlap of [39] dabcbab=ababaabdaa with [43] abbcbda=baabb:

Critical pair: dabcbbaabb=ababaabdaabcbda.

Defines rule #22.

Overlap of [40] aabcbab=cbbcbdaaa with [43] abbcbda=baabb:

Critical pair: aabcbbaabb=cbbcbdaaabcbda.

Defines rule #23.

Overlap of [43] abbcbda=baabb with [2] aaaa=c:

Critical pair: abbcbdc=baabbaaa.

Reduce LHS:

Defines rule #8.

Referenced by [55], [58].

Overlap of [32] aabbcb=bcbaba with [44] bbcbbaabb=daabcbda:

Critical pair: aabbcdaabcbda=bcbababcbbaabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [59].

Overlap of [23] bbcbab=daa with [34] bcbababcbab=aabbaa:

Critical pair: bbcbaaabbaa=daacbababcbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [27] aababbbcba=bbcbaabaab with [10] ad=da:

Critical pair: aababbbcbda=bbcbaabaabd.

Referenced by [56].

Overlap of [26] cbabbbcba=bcbabaaabaab with [10] ad=da:

Critical pair: cbabbbcbda=bcbabaaabaabd.

Referenced by [57].

Overlap of [30] cbababcbabdaa=bcbabcbb with [2] aaaa=c:

Critical pair: cbababcbabdc=bcbabcbbaa.

Reduce LHS:

Defines rule #17.

Referenced by [54], [55].

Overlap of [5] ac=ca with [53] cbababcbab=bcbabcbbaa:

Critical pair: abcbabcbbaa=cabababcbab.

Flip LHS and RHS.

Defines rule #21.

Overlap of [53] cbababcbab=bcbabcbbaa with [48] abbcb=baabbaaa:

Critical pair: cbababcbbaabbaaa=bcbabcbbaabcb.

Referenced by [60].

Overlap of [51] aababbbcbda=bbcbaabaabd with [2] aaaa=c:

Critical pair: aababbbcbdc=bbcbaabaabdaaa.

Reduce LHS:

Defines rule #24.

Referenced by [58].

Overlap of [52] cbabbbcbda=bcbabaaabaabd with [2] aaaa=c:

Critical pair: cbabbbcbdc=bcbabaaabaabdaaa.

Reduce LHS:

Defines rule #15.

Overlap of [2] aaaa=c with [56] aababbbcb=bbcbaabaabdaaa:

Critical pair: aaabbcbaabaabdaaa=cababbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [23] bbcbab=daa with [49] bcbababcbbaabb=aabbaabcbda:

Critical pair: bbcbaaabbaabcbda=daacbababcbbaabb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Overlap of [55] cbababcbbaabbaaa=bcbabcbbaabcb with [2] aaaa=c:

Critical pair: cbababcbbaabbc=bcbabcbbaabcba.

Referenced by [61].

Overlap of [60] cbababcbbaabbc=bcbabcbbaabcba with [9] cd=1:

Critical pair: cbababcbbaabb=bcbabcbbaabcbad.

Reduce RHS:

Defines rule #28.

Referenced by [62].

Overlap of [5] ac=ca with [61] cbababcbbaabb=bcbabcbbaabcbda:

Critical pair: abcbabcbbaabcbda=cabababcbbaabb.

Flip LHS and RHS.

Defines rule #29.