Certificate for #2932 ⟨a, b | aaababaabba=1⟩

Completion settings:

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

Axiom: aaababaabba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [15], [16], [19], [22], [25], [27], [29], [34], [35], [41], [44], [45], [49], [53], [55].

Axiom: babaabb=d.

Defines rule #14.

Referenced by [4], [12], [16], [24], [31], [37].

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

Critical pair: aaada=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [17], [22], [27], [31], [35], [36], [39], [40], [42], [46], [49], [51], [55], [56].

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

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aaad=aada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [15], [23], [25], [28], [29], [31], [33], [34], [35], [36], [37], [38], [40], [52].

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

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] aada=aaad with [7] aada=aaad:

Critical pair: aadaaad=aaadada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12], [13], [24], [31], [33], [37], [43], [47], [50], [54].

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

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #1.

Referenced by [14], [16], [20], [26], [47], [50], [54].

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

Critical pair: babaabd=dabaabb.

Reduce RHS:

Defines rule #7.

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

Overlap of [12] babaabd=adbaabb with [10] da=ad:

Critical pair: babaabad=adbaabba.

Defines rule #11.

Referenced by [33].

Overlap of [12] babaabd=adbaabb with [11] dc=1:

Critical pair: babaab=adbaabbc.

Flip LHS and RHS.

Referenced by [15], [26].

Overlap of [2] aaaa=c with [14] adbaabbc=babaab:

Critical pair: aaababaab=cdbaabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [16], [17], [22].

Overlap of [3] babaabb=d with [15] baabbc=aaababaab:

Critical pair: baaaababaab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [18], [21].

Overlap of [15] baabbc=aaababaab with [5] ca=ac:

Critical pair: baabbac=aaababaaba.

Defines rule #10.

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

Critical pair: bcbabaa=cbabaab.

Referenced by [19].

Overlap of [18] bcbabaa=cbabaab with [2] aaaa=c:

Critical pair: bcbabc=cbabaabaa.

Flip LHS and RHS.

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

Overlap of [11] dc=1 with [19] cbabaabaa=bcbabc:

Critical pair: dbcbabc=babaabaa.

Flip LHS and RHS.

Defines rule #13.

Referenced by [27], [31], [32], [33], [35], [37], [46].

Overlap of [16] bcbabaab=1 with [19] cbabaabaa=bcbabc:

Critical pair: bbcbabc=aa.

Referenced by [23].

Overlap of [19] cbabaabaa=bcbabc with [15] baabbc=aaababaab:

Critical pair: cbabaaaaababaab=bcbabcbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [39].

Overlap of [21] bbcbabc=aa with [8] cd=1:

Critical pair: bbcbab=aad.

Referenced by [24], [25].

Overlap of [23] bbcbab=aad with [3] babaabb=d:

Critical pair: bbcbad=aadabaabb.

Reduce RHS:

Referenced by [25], [26].

Overlap of [23] bbcbab=aad with [24] bbcbad=aaadbaabb:

Critical pair: bbcbaaaadbaabb=aadbcbad.

Reduce LHS:

Defines rule #27.

Overlap of [24] bbcbad=aaadbaabb with [11] dc=1:

Critical pair: bbcba=aaadbaabbc.

Reduce RHS:

Defines rule #8.

Referenced by [27], [31], [36], [41], [49], [55].

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

Critical pair: bbcbc=aababaabaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [28].

Overlap of [27] aadbcbabac=bbcbc with [8] cd=1:

Critical pair: aadbcbaba=bbcbcd.

Reduce RHS:

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

Overlap of [2] aaaa=c with [28] aadbcbaba=bbcb:

Critical pair: aabbcb=cdbcbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [31], [32], [48], [49], [55].

Overlap of [28] aadbcbaba=bbcb with [12] babaabd=adbaabb:

Critical pair: aadbcbaadbaabb=bbcbbaabd.

Flip LHS and RHS.

Defines rule #18.

Referenced by [43].

Overlap of [20] babaabaa=dbcbabc with [28] aadbcbaba=bbcb:

Critical pair: babaababbcb=dbcbabcadbcbaba.

Reduce RHS:

Referenced by [37].

Overlap of [29] bcbaba=aabbcb with [20] babaabaa=dbcbabc:

Critical pair: bcbadbcbabc=aabbcbbaabaa.

Flip LHS and RHS.

Referenced by [45].

Overlap of [13] babaabad=adbaabba with [10] da=ad:

Critical pair: babaabaad=adbaabbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [2] aaaa=c with [33] adbaabbaa=dbcbab:

Critical pair: aaadbcbab=cdbaabbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [35], [36].

Overlap of [20] babaabaa=dbcbabc with [34] baabbaa=aaadbcbab:

Critical pair: babaaaaadbcbab=dbcbabcbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [38].

Overlap of [26] bbcba=aababaab with [34] baabbaa=aaadbcbab:

Critical pair: bbcaaadbcbab=aababaababbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [44].

Overlap of [3] babaabb=d with [31] babaababbcb=aadbbaaa:

Critical pair: babaabaadbbaaa=dabaababbcb.

Reduce LHS:

Reduce RHS:

Referenced by [40].

Overlap of [8] cd=1 with [35] dbcbabcbbaa=bababcbab:

Critical pair: cbababcbab=bcbabcbbaa.

Flip LHS and RHS.

Defines rule #24.

Overlap of [22] bcbabcbbc=cbabacbabaab with [5] ca=ac:

Critical pair: bcbabcbbac=cbabacbabaaba.

Defines rule #20.

Overlap of [8] cd=1 with [37] dbcbabbbaaa=adbaababbcb:

Critical pair: cadbaababbcb=bcbabbbaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [41].

Overlap of [40] bcbabbbaaa=abaababbcb with [2] aaaa=c:

Critical pair: bcbabbbc=abaababbcba.

Reduce RHS:

Defines rule #15.

Referenced by [42].

Overlap of [41] bcbabbbc=abaabaaababaab with [5] ca=ac:

Critical pair: bcbabbbac=abaabaaababaaba.

Defines rule #19.

Referenced by [46].

Overlap of [30] bbcbbaabd=aadbcbaadbaabb with [10] da=ad:

Critical pair: bbcbbaabad=aadbcbaadbaabba.

Defines rule #22.

Overlap of [2] aaaa=c with [36] aababaababbaa=bbaaabcbab:

Critical pair: aabbaaabcbab=cbabaababbaa.

Flip LHS and RHS.

Referenced by [47].

Overlap of [2] aaaa=c with [32] aabbcbbaabaa=bcbadbcbabc:

Critical pair: aabcbadbcbabc=cbbcbbaabaa.

Flip LHS and RHS.

Referenced by [50].

Overlap of [42] bcbabbbac=abaabaaababaaba with [5] ca=ac:

Critical pair: bcbabbbaac=abaabaaababaabaa.

Reduce RHS:

Referenced by [52].

Overlap of [11] dc=1 with [44] cbabaababbaa=aabbaaabcbab:

Critical pair: daabbaaabcbab=babaababbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [48], [49].

Overlap of [29] bcbaba=aabbcb with [47] babaababbaa=aadbbaaabcbab:

Critical pair: bcbaaadbbaaabcbab=aabbcbbaababbaa.

Flip LHS and RHS.

Referenced by [53].

Overlap of [47] babaababbaa=aadbbaaabcbab with [2] aaaa=c:

Critical pair: babaababbc=aadbbaaabcbabaa.

Reduce RHS:

Defines rule #17.

Referenced by [51].

Overlap of [11] dc=1 with [45] cbbcbbaabaa=aabcbadbcbabc:

Critical pair: daabcbadbcbabc=bbcbbaabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [49] babaababbc=aadbbaaacbabaab with [5] ca=ac:

Critical pair: babaababbac=aadbbaaacbabaaba.

Defines rule #21.

Overlap of [46] bcbabbbaac=abaabaaadbcbabc with [8] cd=1:

Critical pair: bcbabbbaa=abaabaaadbcbabcd.

Reduce RHS:

Defines rule #23.

Overlap of [2] aaaa=c with [48] aabbcbbaababbaa=bcbaaadbbaaabcbab:

Critical pair: aabcbaaadbbaaabcbab=cbbcbbaababbaa.

Flip LHS and RHS.

Referenced by [54].

Overlap of [11] dc=1 with [53] cbbcbbaababbaa=aabcbaaadbbaaabcbab:

Critical pair: daabcbaaadbbaaabcbab=bbcbbaababbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.

Referenced by [55].

Overlap of [54] bbcbbaababbaa=aadbcbaaadbbaaabcbab with [2] aaaa=c:

Critical pair: bbcbbaababbc=aadbcbaaadbbaaabcbabaa.

Reduce RHS:

Defines rule #28.

Referenced by [56].

Overlap of [55] bbcbbaababbc=aadbcbaaadbbaaacbabaab with [5] ca=ac:

Critical pair: bbcbbaababbac=aadbcbaaadbbaaacbabaaba.

Defines rule #29.