Certificate for #2966 ⟨a, b | aaabbaabbba=1⟩

Completion settings:

• Reduction order:
  • Right-to-left recursive path with deg(c) = deg(d) = deg(b) = 0, c < d < b; deg(a) = 1
• Auxiliary generators:
  1. bbb=c
  2. aaaabbaa=d

Axiom: aaabbaabbba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [29], [33], [45], [46], [52], [53], [54], [56], [58], [60], [66].

Axiom: aaaabbaa=d.

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

Overlap of [1] aaabbaabbba=1 with [2] bbb=c:

Critical pair: aaabbaaca=1.

Referenced by [7], [8], [9], [10], [11], [13], [15], [17], [18].

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

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [16], [26], [27], [44], [50], [52], [53], [64], [66].

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

Critical pair: aaaabbd=daabbaa.

Referenced by [19].

Overlap of [3] aaaabbaa=d with [4] aaabbaaca=1:

Critical pair: a=dca.

Flip LHS and RHS.

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

Overlap of [3] aaaabbaa=d with [4] aaabbaaca=1:

Critical pair: aaaabb=dabbaaca.

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

Overlap of [4] aaabbaaca=1 with [3] aaaabbaa=d:

Critical pair: aaabbaacd=aaabbaa.

Referenced by [21].

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

Critical pair: aaabbaac=aabbaaca.

Referenced by [11], [17], [18], [21].

Overlap of [7] dca=a with [4] aaabbaaca=1:

Critical pair: dc=aaabbaaca.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [3] aaaabbaa=d with [11] aabbaacaa=dc:

Critical pair: aaaabbdc=dbbaacaa.

Reduce LHS:

Referenced by [22].

Overlap of [4] aaabbaaca=1 with [11] aabbaacaa=dc:

Critical pair: adc=a.

Referenced by [16], [17].

Overlap of [11] aabbaacaa=dc with [3] aaaabbaa=d:

Critical pair: aabbaacd=dcaabbaa.

Reduce RHS:

Referenced by [23].

Overlap of [11] aabbaacaa=dc with [4] aaabbaaca=1:

Critical pair: aabbaac=dcabbaaca.

Reduce RHS:

Referenced by [16], [17], [18], [21], [22], [23], [24].

Overlap of [11] aabbaacaa=dc with [11] aabbaacaa=dc:

Critical pair: aabbaacdc=dcbbaacaa.

Reduce LHS:

Reduce RHS:

Referenced by [17], [18], [19], [20], [21], [22], [23], [24], [40].

Overlap of [4] aaabbaaca=1 with [13] adc=a:

Critical pair: aaabbaaca=dc.

Reduce LHS:

Referenced by [18], [25].

Overlap of [4] aaabbaaca=1 with [10] aaabbaac=aabbaaca:

Critical pair: aabbaacaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [25], [26], [30], [37], [39], [40], [41], [42], [43], [47], [57], [59], [61], [62], [65].

Overlap of [6] aaaabbd=daabbaa with [8] aaaabb=dabbaaca:

Critical pair: dabbaacad=daabbaa.

Reduce LHS:

Referenced by [22].

Simplify [8] aaaabb=dabbaaca.

Reduce RHS:

Referenced by [38].

Overlap of [9] aaabbaacd=aaabbaa with [10] aaabbaac=aabbaaca:

Critical pair: aabbaacad=aaabbaa.

Reduce LHS:

Referenced by [41].

Overlap of [12] dabbaacadc=dbbaacaa with [16] abbaaca=dbbcaacaa:

Critical pair: ddbbcaacaadc=dbbaacaa.

Reduce LHS:

Referenced by [38].

Overlap of [14] aabbaacd=aabbaa with [15] aabbaac=abbaaca:

Critical pair: abbaacad=aabbaa.

Reduce LHS:

Referenced by [42].

Simplify [15] aabbaac=abbaaca.

Reduce RHS:

Referenced by [39].

Simplify [17] dbbcaacaaaa=dc.

Reduce RHS:

Referenced by [28].

Overlap of [18] dc=1 with [5] cb=bc:

Critical pair: dbc=b.

Referenced by [27], [31], [35].

Overlap of [26] dbc=b with [5] cb=bc:

Critical pair: dbbc=bb.

Referenced by [28], [32].

Simplify [25] dbbcaacaaaa=1.

Reduce LHS:

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

Overlap of [2] bbb=c with [28] bbaacaaaa=1:

Critical pair: b=caacaaaa.

Flip LHS and RHS.

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

Overlap of [18] dc=1 with [29] caacaaaa=b:

Critical pair: db=aacaaaa.

Flip LHS and RHS.

Referenced by [31], [36].

Overlap of [26] dbc=b with [29] caacaaaa=b:

Critical pair: dbb=baacaaaa.

Reduce RHS:

Referenced by [32].

Overlap of [27] dbbc=bb with [29] caacaaaa=b:

Critical pair: dbbb=bbaacaaaa.

Reduce LHS:

Reduce RHS:

Referenced by [33].

Overlap of [2] bbb=c with [32] bbdb=1:

Critical pair: b=cdb.

Flip LHS and RHS.

Referenced by [34].

Overlap of [33] cdb=b with [28] bbaacaaaa=1:

Critical pair: cd=bbaacaaaa.

Reduce RHS:

Defines rule #2.

Referenced by [35], [44], [46], [52], [54], [55], [64], [66].

Overlap of [26] dbc=b with [34] cd=1:

Critical pair: db=bd.

Defines rule #4.

Referenced by [36], [38], [39], [40], [41], [42], [51], [57], [59], [61], [63].

Simplify [30] aacaaaa=db.

Reduce RHS:

Defines rule #18.

Referenced by [37], [44], [48], [52], [63], [64].

Overlap of [36] aacaaaa=bd with [36] aacaaaa=bd:

Critical pair: aacaabd=bdcaaaa.

Reduce RHS:

Referenced by [43].

Simplify [20] aaaabb=ddbbcaacaa.

Reduce RHS:

Defines rule #15.

Referenced by [66].

Simplify [24] aabbaac=dbbcaacaa.

Reduce RHS:

Referenced by [52], [53].

Simplify [16] abbaaca=dbbcaacaa.

Reduce RHS:

Referenced by [44], [45], [46], [52].

Overlap of [21] dbbcaacaaad=aaabbaa with [35] db=bd:

Critical pair: bdbcaacaaad=aaabbaa.

Reduce LHS:

Referenced by [58].

Overlap of [23] dbbcaacaad=aabbaa with [35] db=bd:

Critical pair: bdbcaacaad=aabbaa.

Reduce LHS:

Referenced by [56].

Overlap of [37] aacaabd=baaaa with [18] dc=1:

Critical pair: aacaab=baaaac.

Defines rule #13.

Referenced by [45], [46].

Overlap of [40] abbaaca=bbaacaa with [36] aacaaaa=bd:

Critical pair: abbaacbd=bbaacaaacaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [46], [47].

Overlap of [40] abbaaca=bbaacaa with [43] aacaab=baaaac:

Critical pair: abbbaaaac=bbaacaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [60].

Overlap of [40] abbaaca=bbaacaa with [44] bbaacabd=abbaab:

Critical pair: aabbaab=bbaacaabd.

Reduce RHS:

Defines rule #14.

Referenced by [48], [49], [53].

Overlap of [44] bbaacabd=abbaab with [18] dc=1:

Critical pair: bbaacab=abbaabc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [50].

Overlap of [36] aacaaaa=bd with [46] aabbaab=caaaa:

Critical pair: aacaaacaaaa=bdabbaab.

Reduce LHS:

Defines rule #9.

Referenced by [51].

Overlap of [46] aabbaab=caaaa with [46] aabbaab=caaaa:

Critical pair: aabbcaaaa=caaaabaab.

Flip LHS and RHS.

Referenced by [65].

Overlap of [47] abbaabc=bbaacab with [5] cb=bc:

Critical pair: abbaabbc=bbaacabb.

Defines rule #10.

Overlap of [48] aacabd=bdabbaab with [35] db=bd:

Critical pair: aacabbd=bdabbaabb.

Defines rule #11.

Overlap of [36] aacaaaa=bd with [39] aabbaac=bbaacaa:

Critical pair: aacaaabbaacaa=bdabbaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [54], [55].

Overlap of [46] aabbaab=caaaa with [39] aabbaac=bbaacaa:

Critical pair: aabbbbaacaa=caaaabaac.

Reduce LHS:

Flip LHS and RHS.

Referenced by [62], [63].

Overlap of [2] bbb=c with [52] bdabbaac=aaca:

Critical pair: bbaaca=cdabbaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [52] bdabbaac=aaca with [34] cd=1:

Critical pair: bdabbaa=aacad.

Flip LHS and RHS.

Defines rule #7.

Overlap of [2] bbb=c with [42] bbaacaad=aabbaa:

Critical pair: baabbaa=caacaad.

Flip LHS and RHS.

Referenced by [57].

Overlap of [18] dc=1 with [56] caacaad=baabbaa:

Critical pair: dbaabbaa=aacaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Overlap of [2] bbb=c with [41] bbaacaaad=aaabbaa:

Critical pair: baaabbaa=caacaaad.

Flip LHS and RHS.

Referenced by [59].

Overlap of [18] dc=1 with [58] caacaaad=baaabbaa:

Critical pair: dbaaabbaa=aacaaad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [2] bbb=c with [45] bbaacaaab=acaaaac:

Critical pair: bacaaaac=caacaaab.

Flip LHS and RHS.

Referenced by [61].

Overlap of [18] dc=1 with [60] caacaaab=bacaaaac:

Critical pair: dbacaaaac=aacaaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [18] dc=1 with [53] caaaabaac=aabcaacaa:

Critical pair: daabcaacaa=aaaabaac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [36] aacaaaa=bd with [53] caaaabaac=aabcaacaa:

Critical pair: aaaabcaacaa=bdbaac.

Reduce RHS:

Referenced by [64].

Overlap of [63] aaaabcaacaa=bbdaac with [36] aacaaaa=bd:

Critical pair: aaaabcaacbd=bbdaaccaaaa.

Reduce LHS:

Defines rule #22.

Referenced by [66].

Overlap of [18] dc=1 with [49] caaaabaab=aabbcaaaa:

Critical pair: daabbcaaaa=aaaabaab.

Flip LHS and RHS.

Defines rule #21.

Overlap of [64] aaaabcaab=bbdaaccaaaa with [2] bbb=c:

Critical pair: aaaabcaac=bbdaaccaaaabb.

Reduce RHS:

Defines rule #20.