Certificate for #1467 ⟨a, b | aabbbbaaba=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. bbbbaab=d

Axiom: aabbbbaaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [14], [16], [20], [22], [40], [42], [43], [44].

Axiom: bbbbaab=d.

Defines rule #15.

Referenced by [4], [12], [16], [21].

Overlap of [1] aabbbbaaba=1 with [3] bbbbaab=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 [15], [21], [22], [25], [28], [29], [31].

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

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], [16], [23], [26], [30].

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

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

Critical pair: aada=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [14], [22], [29], [33], [38], [39], [40], [41], [42], [43], [44].

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

Critical pair: bbbbaad=dbbbaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [13], [17], [22], [34].

Overlap of [9] cd=1 with [12] dbbbaab=bbbbdaa:

Critical pair: cbbbbdaa=bbbaab.

Referenced by [14].

Overlap of [13] cbbbbdaa=bbbaab with [2] aaa=c:

Critical pair: cbbbbdc=bbbaaba.

Reduce LHS:

Defines rule #10.

Referenced by [15], [16].

Overlap of [5] ac=ca with [14] cbbbb=bbbaaba:

Critical pair: abbbaaba=cabbbb.

Flip LHS and RHS.

Referenced by [32].

Overlap of [14] cbbbb=bbbaaba with [3] bbbbaab=d:

Critical pair: cd=bbbaabaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [12] dbbbaab=bbbbdaa with [16] bbbaabcb=1:

Critical pair: dbbbaa=bbbbdaabbaabcb.

Flip LHS and RHS.

Referenced by [29].

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

Critical pair: bbbaabc=bbaabcb.

Flip LHS and RHS.

Referenced by [19], [27].

Overlap of [18] bbaabcb=bbbaabc with [18] bbaabcb=bbbaabc:

Critical pair: bbaabcbbbaabc=bbbaabcbaabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [20], [24].

Overlap of [2] aaa=c with [19] aabcb=baabc:

Critical pair: abaabc=cbcb.

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

Overlap of [3] bbbbaab=d with [20] abaabc=cbcb:

Critical pair: bbbbacbcb=daabc.

Reduce LHS:

Defines rule #19.

Overlap of [12] dbbbaab=bbbbdaa with [20] abaabc=cbcb:

Critical pair: dbbbacbcb=bbbbdaaaabc.

Reduce LHS:

Reduce RHS:

Defines rule #16.

Overlap of [20] abaabc=cbcb with [9] cd=1:

Critical pair: abaab=cbcbd.

Defines rule #6.

Referenced by [25], [28], [31], [35].

Overlap of [20] abaabc=cbcb with [19] aabcb=baabc:

Critical pair: abbaabc=cbcbb.

Referenced by [26], [27].

Overlap of [23] abaab=cbcbd with [23] abaab=cbcbd:

Critical pair: abacbcbd=cbcbdaab.

Reduce LHS:

Referenced by [38].

Overlap of [24] abbaabc=cbcbb with [9] cd=1:

Critical pair: abbaab=cbcbbd.

Defines rule #8.

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

Overlap of [24] abbaabc=cbcbb with [18] bbaabcb=bbbaabc:

Critical pair: abbbaabc=cbcbbb.

Referenced by [30].

Overlap of [26] abbaab=cbcbbd with [23] abaab=cbcbd:

Critical pair: abbacbcbd=cbcbbdaab.

Reduce LHS:

Referenced by [39].

Overlap of [17] bbbbdaabbaabcb=dbbbaa with [26] abbaab=cbcbbd:

Critical pair: bbbbdacbcbbdcb=dbbbaa.

Reduce LHS:

Defines rule #23.

Overlap of [27] abbbaabc=cbcbbb with [9] cd=1:

Critical pair: abbbaab=cbcbbbd.

Defines rule #13.

Referenced by [31], [32], [37].

Overlap of [30] abbbaab=cbcbbbd with [23] abaab=cbcbd:

Critical pair: abbbacbcbd=cbcbbbdaab.

Reduce LHS:

Referenced by [41].

Simplify [15] cabbbb=abbbaaba.

Reduce RHS:

Referenced by [33].

Overlap of [11] dc=1 with [32] cabbbb=cbcbbbda:

Critical pair: dcbcbbbda=abbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

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

Overlap of [12] dbbbaab=bbbbdaa with [33] abbbb=bcbbbda:

Critical pair: dbbbabcbbbda=bbbbdaabbb.

Referenced by [43].

Overlap of [23] abaab=cbcbd with [33] abbbb=bcbbbda:

Critical pair: ababcbbbda=cbcbdbbb.

Referenced by [40].

Overlap of [26] abbaab=cbcbbd with [33] abbbb=bcbbbda:

Critical pair: abbabcbbbda=cbcbbdbbb.

Referenced by [42].

Overlap of [30] abbbaab=cbcbbbd with [33] abbbb=bcbbbda:

Critical pair: abbbabcbbbda=cbcbbbdbbb.

Referenced by [44].

Overlap of [25] abcabcbd=cbcbdaab with [11] dc=1:

Critical pair: abcabcb=cbcbdaabc.

Defines rule #9.

Overlap of [28] abbcabcbd=cbcbbdaab with [11] dc=1:

Critical pair: abbcabcb=cbcbbdaabc.

Defines rule #14.

Overlap of [35] ababcbbbda=cbcbdbbb with [2] aaa=c:

Critical pair: ababcbbbdc=cbcbdbbbaa.

Reduce LHS:

Defines rule #18.

Overlap of [31] abbbcabcbd=cbcbbbdaab with [11] dc=1:

Critical pair: abbbcabcb=cbcbbbdaabc.

Defines rule #17.

Overlap of [36] abbabcbbbda=cbcbbdbbb with [2] aaa=c:

Critical pair: abbabcbbbdc=cbcbbdbbbaa.

Reduce LHS:

Defines rule #20.

Overlap of [34] dbbbabcbbbda=bbbbdaabbb with [2] aaa=c:

Critical pair: dbbbabcbbbdc=bbbbdaabbbaa.

Reduce LHS:

Defines rule #21.

Overlap of [37] abbbabcbbbda=cbcbbbdbbb with [2] aaa=c:

Critical pair: abbbabcbbbdc=cbcbbbdbbbaa.

Reduce LHS:

Defines rule #22.