Certificate for #3124 ⟨a, b | aabbababbba=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. bbababbb=d

Axiom: aabbababbba=1.

Referenced by [4].

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [15], [16], [18], [20], [21], [23], [32], [34], [37], [40], [43], [46].

Axiom: bbababbb=d.

Defines rule #18.

Referenced by [4], [11], [12], [16], [20], [27], [31], [35].

Overlap of [1] aabbababbba=1 with [3] bbababbb=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 [17], [36], [45].

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], [28], [30], [32], [36].

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], [13], [20], [24], [33], [35], [42], [44], [47].

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

Critical pair: dc=adaa.

Reduce RHS:

Defines rule #1.

Referenced by [14], [16], [20], [25], [34], [42], [44], [47].

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

Critical pair: bbababd=dababbb.

Reduce RHS:

Defines rule #7.

Referenced by [13], [14].

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

Critical pair: bbababbd=dbababbb.

Defines rule #15.

Referenced by [33].

Overlap of [11] bbababd=adbabbb with [9] da=ad:

Critical pair: bbababad=adbabbba.

Defines rule #11.

Referenced by [24].

Overlap of [11] bbababd=adbabbb with [10] dc=1:

Critical pair: bbabab=adbabbbc.

Flip LHS and RHS.

Referenced by [15].

Overlap of [2] aaa=c with [14] adbabbbc=bbabab:

Critical pair: aabbabab=cdbabbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [16], [17], [18], [34], [38].

Overlap of [3] bbababbb=d with [15] babbbc=aabbabab:

Critical pair: bbaaabbabab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [18], [19], [22], [26].

Overlap of [15] babbbc=aabbabab with [5] ca=ac:

Critical pair: babbbac=aabbababa.

Defines rule #10.

Referenced by [20].

Overlap of [16] bbcbbabab=1 with [15] babbbc=aabbabab:

Critical pair: bbcbbabaaabbabab=abbbc.

Reduce LHS:

Referenced by [29].

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

Critical pair: bbcbbaba=bcbbabab.

Referenced by [20].

Overlap of [3] bbababbb=d with [17] babbbac=aabbababa:

Critical pair: bbaaabbababa=dac.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [20] bcbbababba=a with [2] aaa=c:

Critical pair: bcbbababbc=aaa.

Reduce RHS:

Referenced by [22].

Overlap of [21] bcbbababbc=c with [16] bbcbbabab=1:

Critical pair: bcbbaba=cbbabab.

Defines rule #9.

Referenced by [23], [29], [34], [35].

Overlap of [22] bcbbaba=cbbabab with [2] aaa=c:

Critical pair: bcbbabc=cbbababaa.

Flip LHS and RHS.

Referenced by [25], [26].

Overlap of [13] bbababad=adbabbba with [9] da=ad:

Critical pair: bbababaad=adbabbbaa.

Referenced by [30].

Overlap of [10] dc=1 with [23] cbbababaa=bcbbabc:

Critical pair: dbcbbabc=bbababaa.

Flip LHS and RHS.

Defines rule #14.

Referenced by [30].

Overlap of [16] bbcbbabab=1 with [23] cbbababaa=bcbbabc:

Critical pair: bbbcbbabc=aa.

Referenced by [27], [28].

Overlap of [3] bbababbb=d with [26] bbbcbbabc=aa:

Critical pair: bbababbaa=dbbcbbabc.

Referenced by [35], [41].

Overlap of [26] bbbcbbabc=aa with [8] cd=1:

Critical pair: bbbcbbab=aad.

Referenced by [31].

Overlap of [18] bbcbbabcbbabab=abbbc with [22] bcbbaba=cbbabab:

Critical pair: bbcbbacbbababb=abbbc.

Referenced by [35].

Overlap of [24] bbababaad=adbabbbaa with [25] bbababaa=dbcbbabc:

Critical pair: dbcbbabcd=adbabbbaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32].

Overlap of [28] bbbcbbab=aad with [3] bbababbb=d:

Critical pair: bbbcbbad=aadbababbb.

Referenced by [34].

Overlap of [2] aaa=c with [30] adbabbbaa=dbcbbab:

Critical pair: aadbcbbab=cdbabbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [39].

Overlap of [12] bbababbd=dbababbb with [9] da=ad:

Critical pair: bbababbad=dbababbba.

Defines rule #16.

Overlap of [31] bbbcbbad=aadbababbb with [10] dc=1:

Critical pair: bbbcbba=aadbababbbc.

Reduce RHS:

Referenced by [35].

Overlap of [3] bbababbb=d with [34] bbbcbba=aabbababb:

Critical pair: bbababbaabbababb=dbbcbba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36], [41].

Overlap of [8] cd=1 with [35] dbbcbba=adbbbcb:

Critical pair: cadbbbcb=bbcbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [37], [38], [39].

Overlap of [36] bbcbba=abbbcb with [2] aaa=c:

Critical pair: bbcbbc=abbbcbaa.

Flip LHS and RHS.

Referenced by [40].

Overlap of [36] bbcbba=abbbcb with [15] babbbc=aabbabab:

Critical pair: bbcbaabbabab=abbbcbbbbc.

Flip LHS and RHS.

Referenced by [43].

Overlap of [36] bbcbba=abbbcb with [32] babbbaa=aadbcbbab:

Critical pair: bbcbaadbcbbab=abbbcbbbbaa.

Flip LHS and RHS.

Referenced by [46].

Overlap of [2] aaa=c with [37] abbbcbaa=bbcbbc:

Critical pair: aabbcbbc=cbbbcbaa.

Flip LHS and RHS.

Referenced by [42].

Simplify [27] bbababbaa=dbbcbbabc.

Reduce RHS:

Defines rule #17.

Overlap of [10] dc=1 with [40] cbbbcbaa=aabbcbbc:

Critical pair: daabbcbbc=bbbcbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [2] aaa=c with [38] abbbcbbbbc=bbcbaabbabab:

Critical pair: aabbcbaabbabab=cbbbcbbbbc.

Flip LHS and RHS.

Referenced by [44].

Overlap of [10] dc=1 with [43] cbbbcbbbbc=aabbcbaabbabab:

Critical pair: daabbcbaabbabab=bbbcbbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [45].

Overlap of [44] bbbcbbbbc=aadbbcbaabbabab with [5] ca=ac:

Critical pair: bbbcbbbbac=aadbbcbaabbababa.

Defines rule #20.

Overlap of [2] aaa=c with [39] abbbcbbbbaa=bbcbaadbcbbab:

Critical pair: aabbcbaadbcbbab=cbbbcbbbbaa.

Flip LHS and RHS.

Referenced by [47].

Overlap of [10] dc=1 with [46] cbbbcbbbbaa=aabbcbaadbcbbab:

Critical pair: daabbcbaadbcbbab=bbbcbbbbaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.