Certificate for #1419 ⟨a, b | aababaabba=1⟩

Completion settings:

• Auxiliary generators:
  1. c = aaa
  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: aababaabba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [16], [18], [22], [26], [28], [30], [32], [36], [41], [42], [43], [44], [45], [46], [47], [51].

Axiom: babaabb=d.

Defines rule #12.

Referenced by [4], [11], [15], [21], [24].

Overlap of [1] aababaabba=1 with [3] babaabb=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 [28], [32], [33], [45], [47], [50].

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], [16], [22], [23], [26], [29], [30], [32], [33], [35], [36], [42], [44], [46], [50], [51].

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], [24], [39], [42], [48], [49], [51].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [15], [19], [27], [48], [49], [52].

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

Critical pair: babaabd=dabaabb.

Reduce RHS:

Defines rule #7.

Referenced by [12], [13], [16], [22], [31], [37].

Overlap of [11] babaabd=adbaabb with [9] da=ad:

Critical pair: babaabad=adbaabba.

Referenced by [29].

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

Critical pair: babaab=adbaabbc.

Flip LHS and RHS.

Referenced by [14], [27].

Overlap of [2] aaa=c with [13] adbaabbc=babaab:

Critical pair: aababaab=cdbaabbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [15].

Overlap of [3] babaabb=d with [14] baabbc=aababaab:

Critical pair: baaababaab=dc.

Reduce LHS:

Reduce RHS:

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

Overlap of [15] bcbabaab=1 with [11] babaabd=adbaabb:

Critical pair: bcbabaaadbaabb=abaabd.

Reduce LHS:

Defines rule #26.

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

Critical pair: bcbabaa=cbabaab.

Referenced by [18].

Overlap of [17] bcbabaa=cbabaab with [2] aaa=c:

Critical pair: bcbabc=cbabaaba.

Flip LHS and RHS.

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

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

Critical pair: dbcbabc=babaaba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [25], [28], [29], [32], [33], [38].

Overlap of [15] bcbabaab=1 with [18] cbabaaba=bcbabc:

Critical pair: bbcbabc=a.

Referenced by [23].

Overlap of [18] cbabaaba=bcbabc with [3] babaabb=d:

Critical pair: cbabaad=bcbabcbaabb.

Flip LHS and RHS.

Defines rule #27.

Overlap of [18] cbabaaba=bcbabc with [11] babaabd=adbaabb:

Critical pair: cbabaaadbaabb=bcbabcbaabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [20] bbcbabc=a with [8] cd=1:

Critical pair: bbcbab=ad.

Referenced by [24], [26].

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

Critical pair: bbcbad=adabaabb.

Reduce RHS:

Referenced by [26], [27].

Overlap of [18] cbabaaba=bcbabc with [19] babaaba=dbcbabc:

Critical pair: cbabaadbcbabc=bcbabcbaaba.

Flip LHS and RHS.

Defines rule #24.

Overlap of [23] bbcbab=ad with [24] bbcbad=aadbaabb:

Critical pair: bbcbaaadbaabb=adbcbad.

Reduce LHS:

Defines rule #25.

Overlap of [24] bbcbad=aadbaabb with [10] dc=1:

Critical pair: bbcba=aadbaabbc.

Reduce RHS:

Defines rule #9.

Referenced by [28], [33], [42], [45], [47].

Overlap of [27] bbcba=ababaab with [2] aaa=c:

Critical pair: bbcbc=ababaabaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [12] babaabad=adbaabba with [19] babaaba=dbcbabc:

Critical pair: dbcbabcd=adbaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [30], [31].

Overlap of [2] aaa=c with [29] adbaabba=dbcbab:

Critical pair: aadbcbab=cdbaabba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [29] adbaabba=dbcbab with [11] babaabd=adbaabb:

Critical pair: adbaabadbaabb=dbcbabbaabd.

Flip LHS and RHS.

Referenced by [50].

Overlap of [19] babaaba=dbcbabc with [30] baabba=aadbcbab:

Critical pair: babaaaadbcbab=dbcbabcabba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [27] bbcba=ababaab with [30] baabba=aadbcbab:

Critical pair: bbcaadbcbab=ababaababba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46].

Overlap of [30] baabba=aadbcbab with [30] baabba=aadbcbab:

Critical pair: baabaadbcbab=aadbcbababba.

Flip LHS and RHS.

Referenced by [40].

Overlap of [28] adbcbabac=bbcbc with [8] cd=1:

Critical pair: adbcbaba=bbcbcd.

Reduce RHS:

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

Overlap of [2] aaa=c with [35] adbcbaba=bbcb:

Critical pair: aabbcb=cdbcbaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [39], [42], [45], [47].

Overlap of [35] adbcbaba=bbcb with [11] babaabd=adbaabb:

Critical pair: adbcbaadbaabb=bbcbbaabd.

Flip LHS and RHS.

Defines rule #16.

Overlap of [35] adbcbaba=bbcb with [19] babaaba=dbcbabc:

Critical pair: adbcbadbcbabc=bbcbbaaba.

Flip LHS and RHS.

Defines rule #22.

Overlap of [32] dbcbabacbba=bababcbab with [36] bcbaba=aabbcb:

Critical pair: daabbcbcbba=bababcbab.

Reduce LHS:

Referenced by [44].

Overlap of [34] aadbcbababba=baabaadbcbab with [35] adbcbaba=bbcb:

Critical pair: abbcbbba=baabaadbcbab.

Referenced by [41], [42].

Overlap of [2] aaa=c with [40] abbcbbba=baabaadbcbab:

Critical pair: aabaabaadbcbab=cbbcbbba.

Flip LHS and RHS.

Referenced by [49].

Overlap of [40] abbcbbba=baabaadbcbab with [2] aaa=c:

Critical pair: abbcbbbc=baabaadbcbabaa.

Reduce RHS:

Referenced by [43].

Overlap of [2] aaa=c with [42] abbcbbbc=baabaababaab:

Critical pair: aabaabaababaab=cbbcbbbc.

Flip LHS and RHS.

Referenced by [48].

Overlap of [2] aaa=c with [39] aadbbcbcbba=bababcbab:

Critical pair: abababcbab=cdbbcbcbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [45].

Overlap of [44] bbcbcbba=abababcbab with [2] aaa=c:

Critical pair: bbcbcbbc=abababcbabaa.

Reduce RHS:

Defines rule #14.

Overlap of [2] aaa=c with [33] adbcbabcbba=bbaabcbab:

Critical pair: aabbaabcbab=cdbcbabcbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Referenced by [47].

Overlap of [46] bcbabcbba=aabbaabcbab with [2] aaa=c:

Critical pair: bcbabcbbc=aabbaabcbabaa.

Reduce RHS:

Defines rule #15.

Overlap of [10] dc=1 with [43] cbbcbbbc=aabaabaababaab:

Critical pair: daabaabaababaab=bbcbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [10] dc=1 with [41] cbbcbbba=aabaabaadbcbab:

Critical pair: daabaabaadbcbab=bbcbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [8] cd=1 with [31] dbcbabbaabd=adbaabadbaabb:

Critical pair: cadbaabadbaabb=bcbabbaabd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [51].

Overlap of [50] bcbabbaabd=abaabadbaabb with [9] da=ad:

Critical pair: bcbabbaabad=abaabadbaabba.

Reduce RHS:

Referenced by [52].

Overlap of [51] bcbabbaabad=abaabdbcbab with [10] dc=1:

Critical pair: bcbabbaaba=abaabdbcbabc.

Defines rule #23.