Certificate for #2959 ⟨a, b | aaabbaaabba=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(c) = 0; deg(d) = 1; deg(b) = 2; deg(a) = 3
• Auxiliary generators:
  1. aaaa=c
  2. bbaaabb=d

Axiom: aaabbaaabba=1.

Referenced by [4].

Axiom: aaaa=c.

Referenced by [5], [6], [7], [9], [11], [16], [17], [19], [22], [23], [24], [26], [29].

Axiom: bbaaabb=d.

Referenced by [4], [21], [23], [26], [34].

Overlap of [1] aaabbaaabba=1 with [3] bbaaabb=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10], [11], [12], [14], [16].

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

Critical pair: ac=ca.

Referenced by [12], [15], [30], [32].

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

Critical pair: a=cda.

Flip LHS and RHS.

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

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

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaad=aada.

Referenced by [10], [12], [16].

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [13].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13], [14], [15], [17].

Overlap of [7] cada=aa with [4] aaada=1:

Critical pair: cad=aaaada.

Reduce RHS:

Referenced by [12], [15], [20].

Overlap of [4] aaada=1 with [10] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [13].

Overlap of [6] cda=a with [10] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [10] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

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

Overlap of [10] aadaa=cd with [10] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

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

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

Critical pair: aadaa=1.

Reduce LHS:

Referenced by [17].

Overlap of [10] aadaa=cd with [14] aad=ada:

Critical pair: adaaa=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [19], [27], [38], [55], [56], [57], [58], [59].

Simplify [13] adaaa=cd.

Reduce RHS:

Referenced by [19].

Overlap of [18] adaaa=1 with [15] ada=cddaa:

Critical pair: cddaaaa=1.

Reduce LHS:

Defines rule #2.

Referenced by [20], [22], [23], [24], [29], [30], [31], [33], [37], [40], [41], [42], [43], [44], [45], [47], [49], [50], [51], [52], [53], [54], [60], [61].

Overlap of [19] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Referenced by [21], [22], [23], [25], [26], [28].

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

Critical pair: bbaaad=daaabb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [20] ad=da with [21] daaabb=bbdaaa:

Critical pair: abbdaaa=daaaabb.

Reduce RHS:

Referenced by [24], [25].

Overlap of [21] daaabb=bbdaaa with [3] bbaaabb=d:

Critical pair: daaad=bbdaaaaaabb.

Reduce LHS:

Reduce RHS:

Referenced by [25], [31].

Overlap of [22] abbdaaa=bb with [2] aaaa=c:

Critical pair: abbdc=bba.

Reduce LHS:

Referenced by [25], [26].

Overlap of [22] abbdaaa=bb with [20] ad=da:

Critical pair: abbdaada=bbd.

Reduce LHS:

Referenced by [35].

Overlap of [24] abb=bba with [3] bbaaabb=d:

Critical pair: ad=bbaaaabb.

Reduce LHS:

Reduce RHS:

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

Overlap of [17] cd=1 with [26] da=bbcbb:

Critical pair: cbbcbb=a.

Flip LHS and RHS.

Referenced by [28], [29], [30], [31], [32], [34], [35], [48].

Overlap of [20] ad=da with [26] da=bbcbb:

Critical pair: abbcbb=daa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [29].

Overlap of [26] da=bbcbb with [2] aaaa=c:

Critical pair: dc=bbcbbaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [26] da=bbcbb with [5] ac=ca:

Critical pair: dca=bbcbbc.

Reduce LHS:

Flip LHS and RHS.

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

Simplify [23] ddaaa=bbaabb.

Reduce LHS:

Reduce RHS:

Referenced by [32], [33], [34].

Overlap of [5] ac=ca with [31] cbbcbbbbcbbbbcbb=ccbbcbbbbcbbbbbb:

Critical pair: accbbcbbbbcbbbbbb=cabbcbbbbcbbbbcbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [19] dc=1 with [31] cbbcbbbbcbbbbcbb=ccbbcbbbbcbbbbbb:

Critical pair: dccbbcbbbbcbbbbbb=bbcbbbbcbbbbcbb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35], [36].

Overlap of [3] bbaaabb=d with [27] a=cbbcbb:

Critical pair: bbcbbcbbaabb=d.

Reduce LHS:

Referenced by [35].

Overlap of [25] bbbbbbaaa=bbd with [27] a=cbbcbb:

Critical pair: bbbbbbcbbcbbaa=bbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [29] cccbbcbbbbcbbbbcbbbbcbb=1 with [33] bbcbbbbcbbbbcbb=cbbcbbbbcbbbbbb:

Critical pair: ccccbbcbbbbcbbbbbbbbcbb=1.

Reduce LHS:

Referenced by [39].

Overlap of [35] bbd=dbb with [19] dc=1:

Critical pair: bb=dbbc.

Flip LHS and RHS.

Referenced by [38].

Overlap of [17] cd=1 with [37] dbbc=bb:

Critical pair: cbb=bbc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [39], [46], [48].

Simplify [36] cccccbbcbbbbcbbbbbbbbbb=1.

Reduce LHS:

Referenced by [40].

Overlap of [19] dc=1 with [39] cccccccbbbbbbbbbbbbbbbb=1:

Critical pair: d=ccccccbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [41].

Overlap of [19] dc=1 with [40] ccccccbbbbbbbbbbbbbbbb=d:

Critical pair: dd=cccccbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [42].

Overlap of [19] dc=1 with [41] cccccbbbbbbbbbbbbbbbb=dd:

Critical pair: ddd=ccccbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [43].

Overlap of [19] dc=1 with [42] ccccbbbbbbbbbbbbbbbb=ddd:

Critical pair: dddd=cccbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [44].

Overlap of [19] dc=1 with [43] cccbbbbbbbbbbbbbbbb=dddd:

Critical pair: ddddd=ccbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [45], [46].

Overlap of [19] dc=1 with [44] ccbbbbbbbbbbbbbbbb=ddddd:

Critical pair: dddddd=cbbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Referenced by [46], [61].

Overlap of [44] ccbbbbbbbbbbbbbbbb=ddddd with [38] bbc=cbb:

Critical pair: ccbbbbbbbbbbbbbbbcbb=dddddbc.

Reduce LHS:

Referenced by [47].

Overlap of [46] ccbdddddd=dddddbc with [19] dc=1:

Critical pair: ccbddddd=dddddbcc.

Referenced by [49].

Simplify [27] a=cbbcbb.

Reduce RHS:

Defines rule #7.

Overlap of [47] ccbddddd=dddddbcc with [19] dc=1:

Critical pair: ccbdddd=dddddbccc.

Referenced by [50].

Overlap of [49] ccbdddd=dddddbccc with [19] dc=1:

Critical pair: ccbddd=dddddbcccc.

Referenced by [51].

Overlap of [50] ccbddd=dddddbcccc with [19] dc=1:

Critical pair: ccbdd=dddddbccccc.

Referenced by [52].

Overlap of [51] ccbdd=dddddbccccc with [19] dc=1:

Critical pair: ccbd=dddddbcccccc.

Referenced by [53], [54].

Overlap of [19] dc=1 with [52] ccbd=dddddbcccccc:

Critical pair: ddddddbcccccc=cbd.

Flip LHS and RHS.

Referenced by [60].

Overlap of [52] ccbd=dddddbcccccc with [19] dc=1:

Critical pair: ccb=dddddbccccccc.

Flip LHS and RHS.

Referenced by [55].

Overlap of [17] cd=1 with [54] dddddbccccccc=ccb:

Critical pair: cccb=ddddbccccccc.

Flip LHS and RHS.

Referenced by [56].

Overlap of [17] cd=1 with [55] ddddbccccccc=cccb:

Critical pair: ccccb=dddbccccccc.

Flip LHS and RHS.

Referenced by [57].

Overlap of [17] cd=1 with [56] dddbccccccc=ccccb:

Critical pair: cccccb=ddbccccccc.

Flip LHS and RHS.

Referenced by [58].

Overlap of [17] cd=1 with [57] ddbccccccc=cccccb:

Critical pair: ccccccb=dbccccccc.

Flip LHS and RHS.

Referenced by [59].

Overlap of [17] cd=1 with [58] dbccccccc=ccccccb:

Critical pair: cccccccb=bccccccc.

Flip LHS and RHS.

Defines rule #3.

Overlap of [19] dc=1 with [53] cbd=ddddddbcccccc:

Critical pair: dddddddbcccccc=bd.

Flip LHS and RHS.

Defines rule #4.

Overlap of [19] dc=1 with [45] cbbbbbbbbbbbbbbbb=dddddd:

Critical pair: ddddddd=bbbbbbbbbbbbbbbb.

Flip LHS and RHS.

Defines rule #6.