Certificate for #3062 ⟨a, b | aababaabbba=1⟩

Completion settings:

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

Axiom: aababaabbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [16], [19], [25], [26], [28], [42], [43], [44], [47], [54], [56], [57], [58], [60], [62].

Axiom: babaabbb=d.

Defines rule #14.

Referenced by [4], [11], [16], [18], [24], [29], [31], [37].

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

Flip LHS and RHS.

Defines rule #3.

Referenced by [15], [21], [26], [35], [44], [56], [58].

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.

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [19], [21], [25], [42], [43], [46], [47], [57], [59].

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

Critical pair: aadaad=da.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [10], [11], [12], [19], [29], [30], [37], [38], [43], [55], [61], [63].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [16], [20], [22], [23], [38], [43], [55], [56], [61], [63].

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

Critical pair: babaabbd=dabaabbb.

Reduce RHS:

Defines rule #9.

Referenced by [12], [13], [25], [32], [48].

Overlap of [11] babaabbd=adbaabbb with [9] da=ad:

Critical pair: babaabbad=adbaabbba.

Referenced by [21].

Overlap of [11] babaabbd=adbaabbb with [10] dc=1:

Critical pair: babaabb=adbaabbbc.

Flip LHS and RHS.

Referenced by [14], [15].

Overlap of [2] aaa=c with [13] adbaabbbc=babaabb:

Critical pair: aababaabb=cdbaabbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [16], [26], [33], [43].

Overlap of [13] adbaabbbc=babaabb with [5] ca=ac:

Critical pair: adbaabbbac=babaabba.

Referenced by [36].

Overlap of [3] babaabbb=d with [14] baabbbc=aababaabb:

Critical pair: baaababaabb=dc.

Reduce LHS:

Reduce RHS:

Referenced by [17].

Overlap of [16] bcbabaabb=1 with [16] bcbabaabb=1:

Critical pair: bcbabaab=cbabaabb.

Referenced by [18], [21].

Overlap of [17] bcbabaab=cbabaabb with [3] babaabbb=d:

Critical pair: bcbabaad=cbabaabbabaabbb.

Reduce RHS:

Referenced by [19], [20].

Overlap of [18] bcbabaad=cbabaabd with [9] da=ad:

Critical pair: bcbabaaad=cbabaabda.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [18] bcbabaad=cbabaabd with [10] dc=1:

Critical pair: bcbabaa=cbabaabdc.

Reduce RHS:

Defines rule #7.

Referenced by [56].

Overlap of [17] bcbabaab=cbabaabb with [19] cbabaabad=bcbab:

Critical pair: bbcbab=cbabaabbad.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28], [29], [30], [31], [32], [33], [34], [35], [39], [40].

Overlap of [19] cbabaabad=bcbab with [10] dc=1:

Critical pair: cbabaaba=bcbabc.

Referenced by [23], [24], [25], [26], [27], [35].

Overlap of [10] dc=1 with [22] cbabaaba=bcbabc:

Critical pair: dbcbabc=babaaba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [27], [34], [41], [49], [56].

Overlap of [22] cbabaaba=bcbabc with [3] babaabbb=d:

Critical pair: cbabaad=bcbabcbaabbb.

Flip LHS and RHS.

Defines rule #22.

Overlap of [22] cbabaaba=bcbabc with [11] babaabbd=adbaabbb:

Critical pair: cbabaaadbaabbb=bcbabcbaabbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [22] cbabaaba=bcbabc with [14] baabbbc=aababaabb:

Critical pair: cbabaaaababaabb=bcbabcabbbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [22] cbabaaba=bcbabc with [23] babaaba=dbcbabc:

Critical pair: cbabaadbcbabc=bcbabcbaaba.

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aaa=c with [21] abaabbba=bbcbab:

Critical pair: aabbcbab=cbaabbba.

Flip LHS and RHS.

Referenced by [38], [45].

Overlap of [3] babaabbb=d with [21] abaabbba=bbcbab:

Critical pair: bbbcbab=da.

Reduce RHS:

Referenced by [37], [42].

Overlap of [9] da=ad with [21] abaabbba=bbcbab:

Critical pair: dbbcbab=adbaabbba.

Flip LHS and RHS.

Referenced by [36].

Overlap of [21] abaabbba=bbcbab with [3] babaabbb=d:

Critical pair: abaabbd=bbcbabbaabbb.

Flip LHS and RHS.

Defines rule #34.

Overlap of [21] abaabbba=bbcbab with [11] babaabbd=adbaabbb:

Critical pair: abaabbadbaabbb=bbcbabbaabbd.

Flip LHS and RHS.

Defines rule #27.

Overlap of [21] abaabbba=bbcbab with [14] baabbbc=aababaabb:

Critical pair: abaabbaababaabb=bbcbababbbc.

Flip LHS and RHS.

Referenced by [51].

Overlap of [21] abaabbba=bbcbab with [23] babaaba=dbcbabc:

Critical pair: abaabbdbcbabc=bbcbabbaaba.

Flip LHS and RHS.

Defines rule #21.

Overlap of [22] cbabaaba=bcbabc with [21] abaabbba=bbcbab:

Critical pair: cbababbcbab=bcbabcabbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Referenced by [53].

Overlap of [15] adbaabbbac=babaabba with [30] adbaabbba=dbbcbab:

Critical pair: dbbcbabc=babaabba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [40], [41], [44], [45], [50].

Overlap of [29] bbbcbab=ad with [3] babaabbb=d:

Critical pair: bbbcbad=adabaabbb.

Reduce RHS:

Referenced by [42], [43].

Overlap of [10] dc=1 with [28] cbaabbba=aabbcbab:

Critical pair: daabbcbab=baabbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [39].

Overlap of [21] abaabbba=bbcbab with [38] baabbba=aadbbcbab:

Critical pair: abaabbaadbbcbab=bbcbababbba.

Flip LHS and RHS.

Referenced by [52].

Overlap of [21] abaabbba=bbcbab with [36] babaabba=dbbcbabc:

Critical pair: abaabbdbbcbabc=bbcbabbaabba.

Flip LHS and RHS.

Defines rule #32.

Overlap of [23] babaaba=dbcbabc with [36] babaabba=dbbcbabc:

Critical pair: babaadbbcbabc=dbcbabcbaabba.

Flip LHS and RHS.

Referenced by [59].

Overlap of [29] bbbcbab=ad with [37] bbbcbad=aadbaabbb:

Critical pair: bbbcbaaadbaabbb=adbbcbad.

Reduce LHS:

Defines rule #33.

Overlap of [37] bbbcbad=aadbaabbb with [10] dc=1:

Critical pair: bbbcba=aadbaabbbc.

Reduce RHS:

Defines rule #12.

Referenced by [44], [45], [56], [58].

Overlap of [43] bbbcba=ababaabb with [2] aaa=c:

Critical pair: bbbcbc=ababaabbaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [43] bbbcba=ababaabb with [28] cbaabbba=aabbcbab:

Critical pair: bbbaabbcbab=ababaabbabbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [57].

Overlap of [44] adbbcbabac=bbbcbc with [8] cd=1:

Critical pair: adbbcbaba=bbbcbcd.

Reduce RHS:

Referenced by [47], [48], [49], [50].

Overlap of [2] aaa=c with [46] adbbcbaba=bbbcb:

Critical pair: aabbbcb=cdbbcbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [51], [52], [53], [56], [58].

Overlap of [46] adbbcbaba=bbbcb with [11] babaabbd=adbaabbb:

Critical pair: adbbcbaadbaabbb=bbbcbbaabbd.

Flip LHS and RHS.

Defines rule #26.

Overlap of [46] adbbcbaba=bbbcb with [23] babaaba=dbcbabc:

Critical pair: adbbcbadbcbabc=bbbcbbaaba.

Flip LHS and RHS.

Defines rule #20.

Overlap of [46] adbbcbaba=bbbcb with [36] babaabba=dbbcbabc:

Critical pair: adbbcbadbbcbabc=bbbcbbaabba.

Flip LHS and RHS.

Defines rule #31.

Overlap of [33] bbcbababbbc=abaabbaababaabb with [47] bbcbaba=aabbbcb:

Critical pair: aabbbcbbbbc=abaabbaababaabb.

Referenced by [60].

Overlap of [39] bbcbababbba=abaabbaadbbcbab with [47] bbcbaba=aabbbcb:

Critical pair: aabbbcbbbba=abaabbaadbbcbab.

Referenced by [62].

Overlap of [47] bbcbaba=aabbbcb with [35] bcbabacbbba=cbababbcbab:

Critical pair: bcbababbcbab=aabbbcbcbbba.

Flip LHS and RHS.

Referenced by [54].

Overlap of [2] aaa=c with [53] aabbbcbcbbba=bcbababbcbab:

Critical pair: abcbababbcbab=cbbbcbcbbba.

Flip LHS and RHS.

Referenced by [55].

Overlap of [10] dc=1 with [54] cbbbcbcbbba=abcbababbcbab:

Critical pair: dabcbababbcbab=bbbcbcbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Referenced by [56].

Overlap of [55] bbbcbcbbba=adbcbababbcbab with [2] aaa=c:

Critical pair: bbbcbcbbbc=adbcbababbcbabaa.

Reduce RHS:

Defines rule #24.

Overlap of [2] aaa=c with [45] adbbcbabcbbba=bbbaabbcbab:

Critical pair: aabbbaabbcbab=cdbbcbabcbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #30.

Referenced by [58].

Overlap of [57] bbcbabcbbba=aabbbaabbcbab with [2] aaa=c:

Critical pair: bbcbabcbbbc=aabbbaabbcbabaa.

Reduce RHS:

Defines rule #25.

Overlap of [8] cd=1 with [41] dbcbabcbaabba=babaadbbcbabc:

Critical pair: cbabaadbbcbabc=bcbabcbaabba.

Flip LHS and RHS.

Defines rule #19.

Overlap of [2] aaa=c with [51] aabbbcbbbbc=abaabbaababaabb:

Critical pair: aabaabbaababaabb=cbbbcbbbbc.

Flip LHS and RHS.

Referenced by [61].

Overlap of [10] dc=1 with [60] cbbbcbbbbc=aabaabbaababaabb:

Critical pair: daabaabbaababaabb=bbbcbbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [2] aaa=c with [52] aabbbcbbbba=abaabbaadbbcbab:

Critical pair: aabaabbaadbbcbab=cbbbcbbbba.

Flip LHS and RHS.

Referenced by [63].

Overlap of [10] dc=1 with [62] cbbbcbbbba=aabaabbaadbbcbab:

Critical pair: daabaabbaadbbcbab=bbbcbbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.