Certificate for #3073 ⟨a, b | aabababbbba=1⟩

Completion settings:

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

Axiom: aabababbbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [19], [21], [23], [24], [27], [30], [38], [46], [49], [52].

Axiom: bababbbb=d.

Referenced by [4], [12], [17], [20], [25], [28], [29], [30].

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

Defines rule #3.

Referenced by [14], [32], [33], [39], [40].

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.

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

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

Critical pair: cd=aada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [9], [10].

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

Critical pair: adaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [10], [11], [13], [19], [22], [34], [35].

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

Critical pair: aadada=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [17], [30], [34], [36], [41], [42], [44], [47], [48], [50], [51], [53].

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [19], [30], [32], [33], [38], [46], [49], [52].

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

Critical pair: bababbbd=dababbbb.

Flip LHS and RHS.

Referenced by [13], [26].

Overlap of [9] cd=1 with [12] dababbbb=bababbbd:

Critical pair: cbababbbd=ababbbb.

Flip LHS and RHS.

Referenced by [14].

Overlap of [2] aaa=c with [13] ababbbb=cbababbbd:

Critical pair: aacbababbbd=cbabbbb.

Reduce LHS:

Referenced by [15].

Overlap of [11] dc=1 with [14] caabababbbd=cbabbbb:

Critical pair: dcbabbbb=aabababbbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [15] aabababbbd=babbbb with [11] dc=1:

Critical pair: aabababbb=babbbbc.

Referenced by [17], [18], [32].

Overlap of [16] aabababbb=babbbbc with [3] bababbbb=d:

Critical pair: aad=babbbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [16] aabababbb=babbbbc with [17] babbbbcb=daa:

Critical pair: aabababbdaa=babbbbcabbbbcb.

Flip LHS and RHS.

Referenced by [33].

Overlap of [17] babbbbcb=daa with [17] babbbbcb=daa:

Critical pair: babbbbcdaa=daaabbbbcb.

Reduce LHS:

Reduce RHS:

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

Overlap of [3] bababbbb=d with [19] babbbbaa=bbbbcb:

Critical pair: bababbbbbbbcb=dabbbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [19] babbbbaa=bbbbcb with [2] aaa=c:

Critical pair: babbbbc=bbbbcba.

Referenced by [25].

Overlap of [9] cd=1 with [20] dabbbbaa=dbbbcb:

Critical pair: cdbbbcb=abbbbaa.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [20] dabbbbaa=dbbbcb with [2] aaa=c:

Critical pair: dabbbbc=dbbbcba.

Referenced by [26].

Overlap of [2] aaa=c with [22] abbbbaa=bbbcb:

Critical pair: aabbbcb=cbbbbaa.

Defines rule #15.

Overlap of [3] bababbbb=d with [22] abbbbaa=bbbcb:

Critical pair: babbbbcb=daa.

Reduce LHS:

Defines rule #20.

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

Overlap of [12] dababbbb=bababbbd with [22] abbbbaa=bbbcb:

Critical pair: dabbbbcb=bababbbdaa.

Reduce LHS:

Defines rule #17.

Referenced by [44], [45].

Overlap of [22] abbbbaa=bbbcb with [2] aaa=c:

Critical pair: abbbbc=bbbcba.

Referenced by [33], [34].

Overlap of [3] bababbbb=d with [25] bbbbcbab=daa:

Critical pair: bababdaa=dbcbab.

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [3] bababbbb=d with [25] bbbbcbab=daa:

Critical pair: bababbdaa=dbbcbab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [42], [43].

Overlap of [25] bbbbcbab=daa with [3] bababbbb=d:

Critical pair: bbbbcbad=daaababbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [32], [33].

Overlap of [25] bbbbcbab=daa with [19] babbbbaa=bbbbcb:

Critical pair: bbbbcbbbbcb=daabbbaa.

Defines rule #29.

Simplify [16] aabababbb=babbbbc.

Reduce RHS:

Defines rule #19.

Overlap of [18] babbbbcabbbbcb=aabababbdaa with [30] babbbb=bbbbcbda:

Critical pair: bbbbcbdacabbbbcb=aabababbdaa.

Reduce LHS:

Defines rule #16.

Overlap of [27] abbbbc=bbbcba with [9] cd=1:

Critical pair: abbbb=bbbcbad.

Reduce RHS:

Defines rule #13.

Referenced by [37], [43], [45].

Overlap of [9] cd=1 with [28] dbcbab=bababdaa:

Critical pair: cbababdaa=bcbab.

Referenced by [38].

Overlap of [10] ad=da with [28] dbcbab=bababdaa:

Critical pair: abababdaa=dabcbab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [41].

Overlap of [28] dbcbab=bababdaa with [34] abbbb=bbbcbda:

Critical pair: dbcbbbbcbda=bababdaabbb.

Referenced by [46].

Overlap of [35] cbababdaa=bcbab with [2] aaa=c:

Critical pair: cbababdc=bcbaba.

Reduce LHS:

Defines rule #6.

Referenced by [39].

Overlap of [5] ac=ca with [38] cbabab=bcbaba:

Critical pair: abcbaba=cababab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [40].

Overlap of [5] ac=ca with [39] cababab=abcbaba:

Critical pair: aabcbaba=caababab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [10] ad=da with [36] dabcbab=abababdaa:

Critical pair: aabababdaa=daabcbab.

Flip LHS and RHS.

Defines rule #11.

Overlap of [10] ad=da with [29] dbbcbab=bababbdaa:

Critical pair: abababbdaa=dabbcbab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [29] dbbcbab=bababbdaa with [34] abbbb=bbbcbda:

Critical pair: dbbcbbbbcbda=bababbdaabbb.

Referenced by [49].

Overlap of [10] ad=da with [26] dbbbcbab=bababbbdaa:

Critical pair: abababbbdaa=dabbbcbab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [26] dbbbcbab=bababbbdaa with [34] abbbb=bbbcbda:

Critical pair: dbbbcbbbbcbda=bababbbdaabbb.

Referenced by [52].

Overlap of [37] dbcbbbbcbda=bababdaabbb with [2] aaa=c:

Critical pair: dbcbbbbcbdc=bababdaabbbaa.

Reduce LHS:

Defines rule #21.

Referenced by [47].

Overlap of [10] ad=da with [46] dbcbbbbcb=bababdaabbbaa:

Critical pair: abababdaabbbaa=dabcbbbbcb.

Flip LHS and RHS.

Defines rule #22.

Referenced by [48].

Overlap of [10] ad=da with [47] dabcbbbbcb=abababdaabbbaa:

Critical pair: aabababdaabbbaa=daabcbbbbcb.

Flip LHS and RHS.

Defines rule #23.

Overlap of [43] dbbcbbbbcbda=bababbdaabbb with [2] aaa=c:

Critical pair: dbbcbbbbcbdc=bababbdaabbbaa.

Reduce LHS:

Defines rule #24.

Referenced by [50].

Overlap of [10] ad=da with [49] dbbcbbbbcb=bababbdaabbbaa:

Critical pair: abababbdaabbbaa=dabbcbbbbcb.

Flip LHS and RHS.

Defines rule #25.

Referenced by [51].

Overlap of [10] ad=da with [50] dabbcbbbbcb=abababbdaabbbaa:

Critical pair: aabababbdaabbbaa=daabbcbbbbcb.

Flip LHS and RHS.

Defines rule #26.

Overlap of [45] dbbbcbbbbcbda=bababbbdaabbb with [2] aaa=c:

Critical pair: dbbbcbbbbcbdc=bababbbdaabbbaa.

Reduce LHS:

Defines rule #27.

Referenced by [53].

Overlap of [10] ad=da with [52] dbbbcbbbbcb=bababbbdaabbbaa:

Critical pair: abababbbdaabbbaa=dabbbcbbbbcb.

Flip LHS and RHS.

Defines rule #28.