Certificate for #3161 ⟨a, b | aabbbbbaaba=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. bbbbbaab=d

Axiom: aabbbbbaaba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [27], [35], [38], [43], [47], [51], [57].

Axiom: bbbbbaab=d.

Referenced by [4], [11], [14].

Overlap of [1] aabbbbbaaba=1 with [3] bbbbbaab=d:

Critical pair: aada=1.

Referenced by [6], [7], [8], [9], [10], [12].

Overlap of [2] aaa=c with [2] aaa=c:

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [35], [36], [41], [55], [56], [57], [58].

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 [15], [18], [21], [37], [55], [57].

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], [28], [29], [40], [42], [45], [46], [48], [50], [52], [54].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [28], [34], [40], [45], [48], [49], [52], [53].

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

Critical pair: bbbbbaad=dbbbbaab.

Referenced by [12], [13].

Overlap of [11] bbbbbaad=dbbbbaab with [4] aada=1:

Critical pair: bbbbb=dbbbbaaba.

Flip LHS and RHS.

Referenced by [18].

Overlap of [11] bbbbbaad=dbbbbaab with [10] dc=1:

Critical pair: bbbbbaa=dbbbbaabc.

Referenced by [14], [29].

Overlap of [3] bbbbbaab=d with [13] bbbbbaa=dbbbbaabc:

Critical pair: dbbbbaabcb=d.

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

Overlap of [8] cd=1 with [14] dbbbbaabcb=d:

Critical pair: cd=bbbbaabcb.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [14] dbbbbaabcb=d with [15] bbbbaabcb=1:

Critical pair: dbbbbaabc=dbbbaabcb.

Referenced by [23], [29].

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

Critical pair: bbbbaabc=bbbaabcb.

Referenced by [19], [20], [21], [26].

Overlap of [8] cd=1 with [12] dbbbbaaba=bbbbb:

Critical pair: cbbbbb=bbbbaaba.

Flip LHS and RHS.

Defines rule #20.

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

Overlap of [15] bbbbaabcb=1 with [17] bbbbaabc=bbbaabcb:

Critical pair: bbbaabcbb=1.

Referenced by [20], [22].

Overlap of [15] bbbbaabcb=1 with [17] bbbbaabc=bbbaabcb:

Critical pair: bbbbaabcbbbaabcb=bbbaabc.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [17] bbbbaabc=bbbaabcb with [8] cd=1:

Critical pair: bbbbaab=bbbaabcbd.

Reduce RHS:

Flip LHS and RHS.

Referenced by [30].

Simplify [19] bbbaabcbb=1.

Reduce LHS:

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

Overlap of [14] dbbbbaabcb=d with [22] bbaabcbbb=1:

Critical pair: dbbbbaabc=dbaabcbbb.

Reduce LHS:

Referenced by [29].

Overlap of [22] bbaabcbbb=1 with [22] bbaabcbbb=1:

Critical pair: bbaabcb=aabcbbb.

Referenced by [25], [26], [30].

Overlap of [22] bbaabcbbb=1 with [24] bbaabcb=aabcbbb:

Critical pair: aabcbbbbb=1.

Referenced by [26], [27].

Overlap of [24] bbaabcb=aabcbbb with [17] bbbbaabc=bbbaabcb:

Critical pair: bbaabcbbbaabcb=aabcbbbbbbaabc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [29], [35], [36], [37], [39], [44].

Overlap of [2] aaa=c with [25] aabcbbbbb=1:

Critical pair: a=cbcbbbbb.

Flip LHS and RHS.

Referenced by [28].

Overlap of [10] dc=1 with [27] cbcbbbbb=a:

Critical pair: da=bcbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

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

Simplify [13] bbbbbaa=dbbbbaabc.

Reduce RHS:

Defines rule #21.

Referenced by [57].

Overlap of [21] bbaabcbbd=bbbbaab with [24] bbaabcb=aabcbbb:

Critical pair: aabcbbbbd=bbbbaab.

Referenced by [51].

Overlap of [28] bcbbbbb=ad with [18] bbbbaaba=cbbbbb:

Critical pair: bcbbcbbbbb=adbaaba.

Reduce LHS:

Defines rule #9.

Referenced by [42].

Overlap of [28] bcbbbbb=ad with [18] bbbbaaba=cbbbbb:

Critical pair: bcbbbcbbbbb=adbbaaba.

Reduce LHS:

Defines rule #13.

Referenced by [46].

Overlap of [28] bcbbbbb=ad with [18] bbbbaaba=cbbbbb:

Critical pair: bcbbbbcbbbbb=adbbbaaba.

Reduce LHS:

Defines rule #16.

Referenced by [50].

Overlap of [28] bcbbbbb=ad with [28] bcbbbbb=ad:

Critical pair: bcbbbbad=adcbbbbb.

Reduce RHS:

Referenced by [49].

Overlap of [18] bbbbaaba=cbbbbb with [26] baabc=aabcb:

Critical pair: bbbbaaaabcb=cbbbbbabc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [53], [54].

Overlap of [26] baabc=aabcb with [5] ca=ac:

Critical pair: baabac=aabcba.

Defines rule #8.

Referenced by [41].

Overlap of [26] baabc=aabcb with [8] cd=1:

Critical pair: baab=aabcbd.

Flip LHS and RHS.

Referenced by [38], [39].

Overlap of [2] aaa=c with [37] aabcbd=baab:

Critical pair: abaab=cbcbd.

Flip LHS and RHS.

Referenced by [40].

Overlap of [26] baabc=aabcb with [37] aabcbd=baab:

Critical pair: bbaab=aabcbbd.

Flip LHS and RHS.

Referenced by [43], [44].

Overlap of [10] dc=1 with [38] cbcbd=abaab:

Critical pair: dabaab=bcbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [36] baabac=aabcba with [5] ca=ac:

Critical pair: baabaac=aabcbaa.

Defines rule #10.

Overlap of [31] bcbad=adbaaba with [9] da=ad:

Critical pair: bcbaad=adbaabaa.

Defines rule #11.

Overlap of [2] aaa=c with [39] aabcbbd=bbaab:

Critical pair: abbaab=cbcbbd.

Flip LHS and RHS.

Referenced by [45].

Overlap of [26] baabc=aabcb with [39] aabcbbd=bbaab:

Critical pair: bbbaab=aabcbbbd.

Flip LHS and RHS.

Referenced by [47].

Overlap of [10] dc=1 with [43] cbcbbd=abbaab:

Critical pair: dabbaab=bcbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [32] bcbbad=adbbaaba with [9] da=ad:

Critical pair: bcbbaad=adbbaabaa.

Defines rule #14.

Overlap of [2] aaa=c with [44] aabcbbbd=bbbaab:

Critical pair: abbbaab=cbcbbbd.

Flip LHS and RHS.

Referenced by [48].

Overlap of [10] dc=1 with [47] cbcbbbd=abbbaab:

Critical pair: dabbbaab=bcbbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [34] bcbbbbad=abbbbb with [10] dc=1:

Critical pair: bcbbbba=abbbbbc.

Defines rule #19.

Overlap of [33] bcbbbad=adbbbaaba with [9] da=ad:

Critical pair: bcbbbaad=adbbbaabaa.

Defines rule #17.

Overlap of [2] aaa=c with [30] aabcbbbbd=bbbbaab:

Critical pair: abbbbaab=cbcbbbbd.

Flip LHS and RHS.

Referenced by [52].

Overlap of [10] dc=1 with [51] cbcbbbbd=abbbbaab:

Critical pair: dabbbbaab=bcbbbbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [10] dc=1 with [35] cbbbbbabc=bbbbacbcb:

Critical pair: dbbbbacbcb=bbbbbabc.

Flip LHS and RHS.

Defines rule #23.

Referenced by [56].

Overlap of [28] bcbbbbb=ad with [35] cbbbbbabc=bbbbacbcb:

Critical pair: bbbbbacbcb=adabc.

Reduce RHS:

Referenced by [55].

Overlap of [54] bbbbbacbcb=aadbc with [28] bcbbbbb=ad:

Critical pair: bbbbbacbcad=aadbccbbbbb.

Reduce LHS:

Defines rule #25.

Referenced by [57].

Overlap of [53] bbbbbabc=dbbbbacbcb with [5] ca=ac:

Critical pair: bbbbbabac=dbbbbacbcba.

Defines rule #26.

Referenced by [58].

Overlap of [55] bbbbbacba=aadbccbbbbb with [2] aaa=c:

Critical pair: bbbbbacbc=aadbccbbbbbaa.

Reduce RHS:

Defines rule #24.

Overlap of [56] bbbbbabac=dbbbbacbcba with [5] ca=ac:

Critical pair: bbbbbabaac=dbbbbacbcbaa.

Defines rule #27.