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

Completion settings:

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

Axiom: aaababaabba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #2.

Referenced by [5], [6], [7], [17], [18], [21], [24], [27], [28], [29], [31], [36], [37], [43], [45], [50], [53], [55].

Axiom: babaabb=d.

Defines rule #14.

Referenced by [4], [14], [18], [26], [32], [39].

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 #1.

Referenced by [12], [19], [24], [29], [32], [37], [38], [41], [42], [44], [47], [50], [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 [2] aaaa=c:

Critical pair: aaadc=aaa.

Referenced by [9].

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #3.

Referenced by [13], [17], [25], [27], [28], [30], [31], [32], [35], [36], [37], [38], [39], [40], [42], [52].

Overlap of [4] aaada=1 with [7] aaadc=aaa:

Critical pair: aaadaaa=aadc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10].

Overlap of [4] aaada=1 with [9] aadc=aa:

Critical pair: aaadaa=adc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] aaada=1 with [10] adc=a:

Critical pair: aaada=dc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [15], [18], [22], [28], [48], [54].

Overlap of [11] dc=1 with [5] ca=ac:

Critical pair: dac=a.

Referenced by [13].

Overlap of [12] dac=a with [8] cd=1:

Critical pair: da=ad.

Defines rule #5.

Referenced by [14], [16], [26], [28], [32], [35], [39], [46], [48], [54].

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

Critical pair: babaabd=dabaabb.

Reduce RHS:

Defines rule #12.

Referenced by [15], [16], [33].

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

Critical pair: babaab=adbaabbc.

Flip LHS and RHS.

Referenced by [17].

Overlap of [14] babaabd=adbaabb with [13] da=ad:

Critical pair: babaabad=adbaabba.

Defines rule #13.

Referenced by [35].

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

Critical pair: aaababaab=cdbaabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [18], [19], [24], [28].

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

Critical pair: baaaababaab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [20], [23].

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

Critical pair: baabbac=aaababaaba.

Defines rule #9.

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

Critical pair: bcbabaa=cbabaab.

Referenced by [21].

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

Critical pair: bcbabc=cbabaabaa.

Flip LHS and RHS.

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

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

Critical pair: dbcbabc=babaabaa.

Flip LHS and RHS.

Defines rule #11.

Referenced by [29], [32], [34], [35], [37], [39], [47].

Overlap of [18] bcbabaab=1 with [21] cbabaabaa=bcbabc:

Critical pair: bbcbabc=aa.

Referenced by [25].

Overlap of [21] cbabaabaa=bcbabc with [17] baabbc=aaababaab:

Critical pair: cbabaaaaababaab=bcbabcbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [41].

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

Critical pair: bbcbab=aad.

Referenced by [26], [27].

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

Critical pair: bbcbad=aadabaabb.

Reduce RHS:

Referenced by [27], [28].

Overlap of [25] bbcbab=aad with [26] bbcbad=aaadbaabb:

Critical pair: bbcbaaaadbaabb=aadbcbad.

Reduce LHS:

Defines rule #27.

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

Critical pair: bbcba=aaadbaabbc.

Reduce RHS:

Defines rule #7.

Referenced by [29], [32], [38], [43], [50], [55].

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

Critical pair: bbcbc=aababaabaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

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

Critical pair: aadbcbaba=bbcbcd.

Reduce RHS:

Referenced by [31], [32], [33], [34].

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

Critical pair: aabbcb=cdbcbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [32], [49], [50], [55].

Overlap of [22] babaabaa=dbcbabc with [30] aadbcbaba=bbcb:

Critical pair: babaababbcb=dbcbabcadbcbaba.

Reduce RHS:

Referenced by [39].

Overlap of [30] aadbcbaba=bbcb with [14] babaabd=adbaabb:

Critical pair: aadbcbaadbaabb=bbcbbaabd.

Flip LHS and RHS.

Defines rule #25.

Referenced by [46].

Overlap of [30] aadbcbaba=bbcb with [22] babaabaa=dbcbabc:

Critical pair: aadbcbadbcbabc=bbcbbaabaa.

Flip LHS and RHS.

Defines rule #24.

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

Critical pair: babaabaad=adbaabbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

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

Critical pair: aaadbcbab=cdbaabbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [37], [38].

Overlap of [22] babaabaa=dbcbabc with [36] baabbaa=aaadbcbab:

Critical pair: babaaaaadbcbab=dbcbabcbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [40].

Overlap of [28] bbcba=aababaab with [36] baabbaa=aaadbcbab:

Critical pair: bbcaaadbcbab=aababaababbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [45].

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

Critical pair: babaabaadbbaaa=dabaababbcb.

Reduce LHS:

Reduce RHS:

Referenced by [42].

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

Critical pair: cbababcbab=bcbabcbbaa.

Flip LHS and RHS.

Defines rule #22.

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

Critical pair: bcbabcbbac=cbabacbabaaba.

Defines rule #19.

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

Critical pair: cadbaababbcb=bcbabbbaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [43].

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

Critical pair: bcbabbbc=abaababbcba.

Reduce RHS:

Defines rule #15.

Referenced by [44].

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

Critical pair: bcbabbbac=abaabaaababaaba.

Defines rule #18.

Referenced by [47].

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

Critical pair: aabbaaabcbab=cbabaababbaa.

Flip LHS and RHS.

Referenced by [48].

Overlap of [33] bbcbbaabd=aadbcbaadbaabb with [13] da=ad:

Critical pair: bbcbbaabad=aadbcbaadbaabba.

Defines rule #26.

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

Critical pair: bcbabbbaac=abaabaaababaabaa.

Reduce RHS:

Referenced by [52].

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

Critical pair: daabbaaabcbab=babaababbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [49], [50].

Overlap of [31] bcbaba=aabbcb with [48] babaababbaa=aadbbaaabcbab:

Critical pair: bcbaaadbbaaabcbab=aabbcbbaababbaa.

Flip LHS and RHS.

Referenced by [53].

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

Critical pair: babaababbc=aadbbaaabcbabaa.

Reduce RHS:

Defines rule #17.

Referenced by [51].

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

Critical pair: babaababbac=aadbbaaacbabaaba.

Defines rule #20.

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

Critical pair: bcbabbbaa=abaabaaadbcbabcd.

Reduce RHS:

Defines rule #21.

Overlap of [2] aaaa=c with [49] 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.