Certificate for #2962 ⟨a, b | aaabbaababa=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. aaaa=c
  2. bbaabab=d

Axiom: aaabbaababa=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [11], [21], [24], [27], [29], [30], [31], [34], [40], [44], [52], [55], [57], [59], [62].

Axiom: bbaabab=d.

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

Overlap of [1] aaabbaababa=1 with [3] bbaabab=d:

Critical pair: aaada=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [19], [31], [36], [37], [41], [42], [49], [54], [58], [61].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

Overlap of [4] aaada=1 with [4] aaada=1:

Critical pair: aaad=aada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [15], [20], [40], [43], [44], [49], [52], [55], [57].

Overlap of [4] aaada=1 with [7] aada=aaad:

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] aada=aaad with [7] aada=aaad:

Critical pair: aadaaad=aaadada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [16], [22], [32], [35], [38], [39], [50], [51], [60], [63].

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

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #1.

Referenced by [13], [22], [32], [33], [38], [60], [63].

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

Critical pair: bbaabad=dbaabab.

Referenced by [13].

Overlap of [12] bbaabad=dbaabab with [11] dc=1:

Critical pair: bbaaba=dbaababc.

Referenced by [14], [28].

Overlap of [3] bbaabab=d with [13] bbaaba=dbaababc:

Critical pair: dbaababcb=d.

Referenced by [15], [16].

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

Critical pair: cd=baababcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16], [17], [18], [23].

Overlap of [14] dbaababcb=d with [15] baababcb=1:

Critical pair: dbaababc=daababcb.

Reduce RHS:

Referenced by [28].

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

Critical pair: baababc=aababcb.

Defines rule #6.

Referenced by [18], [19], [20], [24], [25], [30], [36].

Overlap of [15] baababcb=1 with [17] baababc=aababcb:

Critical pair: aababcbb=1.

Referenced by [21].

Overlap of [17] baababc=aababcb with [5] ca=ac:

Critical pair: baababac=aababcba.

Defines rule #10.

Referenced by [41].

Overlap of [17] baababc=aababcb with [8] cd=1:

Critical pair: baabab=aababcbd.

Flip LHS and RHS.

Referenced by [27].

Overlap of [2] aaaa=c with [18] aababcbb=1:

Critical pair: aa=cbabcbb.

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [11] dc=1 with [21] cbabcbb=aa:

Critical pair: daa=babcbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [33], [45], [49].

Overlap of [15] baababcb=1 with [21] cbabcbb=aa:

Critical pair: baababaa=abcbb.

Defines rule #13.

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

Overlap of [23] baababaa=abcbb with [2] aaaa=c:

Critical pair: baababc=abcbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [23] baababaa=abcbb with [17] baababc=aababcb:

Critical pair: baabaaababcb=abcbbbabc.

Flip LHS and RHS.

Referenced by [51].

Overlap of [23] baababaa=abcbb with [23] baababaa=abcbb:

Critical pair: baabaabcbb=abcbbbabaa.

Flip LHS and RHS.

Referenced by [50].

Overlap of [2] aaaa=c with [20] aababcbd=baabab:

Critical pair: aabaabab=cbabcbd.

Flip LHS and RHS.

Referenced by [38].

Simplify [13] bbaaba=dbaababc.

Reduce RHS:

Defines rule #9.

Referenced by [29], [30].

Overlap of [28] bbaaba=aadbabcb with [2] aaaa=c:

Critical pair: bbaabc=aadbabcbaaa.

Flip LHS and RHS.

Referenced by [42].

Overlap of [28] bbaaba=aadbabcb with [17] baababc=aababcb:

Critical pair: bbaaaababcb=aadbabcbababc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [52].

Overlap of [2] aaaa=c with [24] abcbbaa=aababcb:

Critical pair: aaaaababcb=cbcbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [11] dc=1 with [31] cbcbbaa=acbabcb:

Critical pair: dacbabcb=bcbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33], [34].

Overlap of [22] babcbb=aad with [32] bcbbaa=ababcb:

Critical pair: babcbababcb=aadcbbaa.

Reduce RHS:

Referenced by [49].

Overlap of [32] bcbbaa=ababcb with [2] aaaa=c:

Critical pair: bcbbc=ababcbaa.

Flip LHS and RHS.

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

Overlap of [10] da=ad with [34] ababcbaa=bcbbc:

Critical pair: dbcbbc=adbabcbaa.

Flip LHS and RHS.

Referenced by [40], [42].

Overlap of [34] ababcbaa=bcbbc with [17] baababc=aababcb:

Critical pair: ababcaababcb=bcbbcbabc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [34] ababcbaa=bcbbc with [23] baababaa=abcbb:

Critical pair: ababcabcbb=bcbbcbabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Overlap of [11] dc=1 with [27] cbabcbd=aabaabab:

Critical pair: daabaabab=babcbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [39], [46].

Overlap of [38] babcbd=aadbaabab with [10] da=ad:

Critical pair: babcbad=aadbaababa.

Defines rule #11.

Referenced by [47].

Overlap of [2] aaaa=c with [35] adbabcbaa=dbcbbc:

Critical pair: aaadbcbbc=cdbabcbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [48].

Overlap of [34] ababcbaa=bcbbc with [19] baababac=aababcba:

Critical pair: ababcaababcba=bcbbcbabac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Simplify [29] aadbabcbaaa=bbaabc.

Reduce LHS:

Referenced by [43].

Overlap of [42] adbcbbac=bbaabc with [8] cd=1:

Critical pair: adbcbba=bbaabcd.

Reduce RHS:

Referenced by [44], [45], [46], [47], [48].

Overlap of [2] aaaa=c with [43] adbcbba=bbaab:

Critical pair: aaabbaab=cdbcbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [53], [56].

Overlap of [43] adbcbba=bbaab with [22] babcbb=aad:

Critical pair: adbcbaad=bbaabbcbb.

Flip LHS and RHS.

Defines rule #27.

Overlap of [43] adbcbba=bbaab with [38] babcbd=aadbaabab:

Critical pair: adbcbaadbaabab=bbaabbcbd.

Flip LHS and RHS.

Defines rule #18.

Overlap of [43] adbcbba=bbaab with [39] babcbad=aadbaababa:

Critical pair: adbcbaadbaababa=bbaabbcbad.

Flip LHS and RHS.

Defines rule #22.

Overlap of [43] adbcbba=bbaab with [40] babcbaa=aaadbcbbc:

Critical pair: adbcbaaadbcbbc=bbaabbcbaa.

Flip LHS and RHS.

Defines rule #23.

Overlap of [33] babcbababcb=aabbaa with [22] babcbb=aad:

Critical pair: babcbababcaad=aabbaaabcbb.

Reduce LHS:

Defines rule #26.

Referenced by [56].

Overlap of [10] da=ad with [26] abcbbbabaa=baabaabcbb:

Critical pair: dbaabaabcbb=adbcbbbabaa.

Flip LHS and RHS.

Referenced by [55].

Overlap of [10] da=ad with [25] abcbbbabc=baabaaababcb:

Critical pair: dbaabaaababcb=adbcbbbabc.

Flip LHS and RHS.

Referenced by [57].

Overlap of [2] aaaa=c with [30] aadbabcbababc=bbcbabcb:

Critical pair: aabbcbabcb=cdbabcbababc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [53], [54].

Overlap of [44] bcbba=aaabbaab with [52] babcbababc=aabbcbabcb:

Critical pair: bcbaabbcbabcb=aaabbaabbcbababc.

Flip LHS and RHS.

Referenced by [59].

Overlap of [52] babcbababc=aabbcbabcb with [5] ca=ac:

Critical pair: babcbababac=aabbcbabcba.

Defines rule #21.

Overlap of [2] aaaa=c with [50] adbcbbbabaa=dbaabaabcbb:

Critical pair: aaadbaabaabcbb=cdbcbbbabaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [44] bcbba=aaabbaab with [49] babcbababaa=aabbaaabcbb:

Critical pair: bcbaabbaaabcbb=aaabbaabbcbababaa.

Flip LHS and RHS.

Referenced by [62].

Overlap of [2] aaaa=c with [51] adbcbbbabc=dbaabaaababcb:

Critical pair: aaadbaabaaababcb=cdbcbbbabc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [58].

Overlap of [57] bcbbbabc=aaadbaabaaababcb with [5] ca=ac:

Critical pair: bcbbbabac=aaadbaabaaababcba.

Defines rule #19.

Overlap of [2] aaaa=c with [53] aaabbaabbcbababc=bcbaabbcbabcb:

Critical pair: abcbaabbcbabcb=cbbaabbcbababc.

Flip LHS and RHS.

Referenced by [60].

Overlap of [11] dc=1 with [59] cbbaabbcbababc=abcbaabbcbabcb:

Critical pair: dabcbaabbcbabcb=bbaabbcbababc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #28.

Referenced by [61].

Overlap of [60] bbaabbcbababc=adbcbaabbcbabcb with [5] ca=ac:

Critical pair: bbaabbcbababac=adbcbaabbcbabcba.

Defines rule #29.

Overlap of [2] aaaa=c with [56] aaabbaabbcbababaa=bcbaabbaaabcbb:

Critical pair: abcbaabbaaabcbb=cbbaabbcbababaa.

Flip LHS and RHS.

Referenced by [63].

Overlap of [11] dc=1 with [62] cbbaabbcbababaa=abcbaabbaaabcbb:

Critical pair: dabcbaabbaaabcbb=bbaabbcbababaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #30.