Certificate for #1414 ⟨a, b | aabaabbbba=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. baabbbb=d

Axiom: aabaabbbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [14], [15], [19], [23], [31], [40].

Axiom: baabbbb=d.

Defines rule #15.

Referenced by [4], [11], [15], [18], [22].

Overlap of [1] aabaabbbba=1 with [3] baabbbb=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 [22], [23], [24], [27], [30], [35], [38], [39], [41].

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], [11].

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

Critical pair: cd=aada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [18], [23], [29], [30], [31], [37], [38], [39], [40], [41].

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].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [15], [20], [25], [28].

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

Critical pair: baabbbd=daabbbb.

Reduce RHS:

Defines rule #11.

Referenced by [12], [13], [16], [23], [32].

Overlap of [11] baabbbd=aadbbbb with [9] da=ad:

Critical pair: baabbbad=aadbbbba.

Referenced by [29].

Overlap of [11] baabbbd=aadbbbb with [10] dc=1:

Critical pair: baabbb=aadbbbbc.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] aadbbbbc=baabbb:

Critical pair: abaabbb=cdbbbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [15].

Overlap of [3] baabbbb=d with [14] bbbbc=abaabbb:

Critical pair: baaabaabbb=dc.

Reduce LHS:

Reduce RHS:

Referenced by [16], [17].

Overlap of [15] bcbaabbb=1 with [11] baabbbd=aadbbbb:

Critical pair: bcbaabbaadbbbb=aabbbd.

Referenced by [30].

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

Critical pair: bcbaabb=cbaabbb.

Referenced by [18], [26].

Overlap of [17] bcbaabb=cbaabbb with [17] bcbaabb=cbaabbb:

Critical pair: bcbaabcbaabbb=cbaabbbcbaabb.

Reduce LHS:

Reduce RHS:

Defines rule #7.

Referenced by [19], [21], [30].

Overlap of [18] bcbaa=cbaab with [2] aaa=c:

Critical pair: bcbc=cbaaba.

Flip LHS and RHS.

Referenced by [20], [21], [22], [23], [24], [27].

Overlap of [10] dc=1 with [19] cbaaba=bcbc:

Critical pair: dbcbc=baaba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [24], [33], [35].

Overlap of [18] bcbaa=cbaab with [19] cbaaba=bcbc:

Critical pair: bbcbc=cbaabba.

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [19] cbaaba=bcbc with [3] baabbbb=d:

Critical pair: cbaad=bcbcabbbb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [19] cbaaba=bcbc with [11] baabbbd=aadbbbb:

Critical pair: cbaaaadbbbb=bcbcabbbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [19] cbaaba=bcbc with [20] baaba=dbcbc:

Critical pair: cbaadbcbc=bcbcaba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [10] dc=1 with [21] cbaabba=bbcbc:

Critical pair: dbbcbc=baabba.

Flip LHS and RHS.

Defines rule #8.

Referenced by [27], [34].

Overlap of [17] bcbaabb=cbaabbb with [21] cbaabba=bbcbc:

Critical pair: bbbcbc=cbaabbba.

Flip LHS and RHS.

Referenced by [28], [30].

Overlap of [19] cbaaba=bcbc with [25] baabba=dbbcbc:

Critical pair: cbaadbbcbc=bcbcabba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [10] dc=1 with [26] cbaabbba=bbbcbc:

Critical pair: dbbbcbc=baabbba.

Flip LHS and RHS.

Defines rule #13.

Referenced by [29], [35], [36].

Overlap of [12] baabbbad=aadbbbba with [28] baabbba=dbbbcbc:

Critical pair: dbbbcbcd=aadbbbba.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [16] bcbaabbaadbbbb=aabbbd with [18] bcbaa=cbaab:

Critical pair: cbaabbbaadbbbb=aabbbd.

Reduce LHS:

Defines rule #23.

Overlap of [2] aaa=c with [29] aadbbbba=dbbbcb:

Critical pair: adbbbcb=cdbbbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [36].

Overlap of [29] aadbbbba=dbbbcb with [11] baabbbd=aadbbbb:

Critical pair: aadbbbaadbbbb=dbbbcbabbbd.

Flip LHS and RHS.

Referenced by [41].

Overlap of [29] aadbbbba=dbbbcb with [20] baaba=dbcbc:

Critical pair: aadbbbdbcbc=dbbbcbaba.

Flip LHS and RHS.

Referenced by [38].

Overlap of [29] aadbbbba=dbbbcb with [25] baabba=dbbcbc:

Critical pair: aadbbbdbbcbc=dbbbcbabba.

Flip LHS and RHS.

Referenced by [39].

Overlap of [20] baaba=dbcbc with [28] baabbba=dbbbcbc:

Critical pair: baadbbbcbc=dbcbcabbba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [31] bbbba=adbbbcb with [28] baabbba=dbbbcbc:

Critical pair: bbbdbbbcbc=adbbbcbabbba.

Flip LHS and RHS.

Referenced by [40].

Overlap of [8] cd=1 with [35] dbcbacbbba=baadbbbcbc:

Critical pair: cbaadbbbcbc=bcbacbbba.

Flip LHS and RHS.

Defines rule #17.

Overlap of [8] cd=1 with [33] dbbbcbaba=aadbbbdbcbc:

Critical pair: caadbbbdbcbc=bbbcbaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [8] cd=1 with [34] dbbbcbabba=aadbbbdbbcbc:

Critical pair: caadbbbdbbcbc=bbbcbabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [2] aaa=c with [36] adbbbcbabbba=bbbdbbbcbc:

Critical pair: aabbbdbbbcbc=cdbbbcbabbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [8] cd=1 with [32] dbbbcbabbbd=aadbbbaadbbbb:

Critical pair: caadbbbaadbbbb=bbbcbabbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.