Certificate for #3223 ⟨a, b | abaabbbabba=1⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(b) = 0; deg(d) = 1; deg(c) = 2; deg(a) = 3
• Auxiliary generators:
  1. baa=c
  2. abcc=d

Axiom: abaabbbabba=1.

Referenced by [4].

Axiom: baa=c.

Referenced by [4], [5], [6], [16], [18], [25].

Axiom: abcc=d.

Referenced by [5], [8], [11], [13], [19], [21].

Overlap of [1] abaabbbabba=1 with [2] baa=c:

Critical pair: acbbbabba=1.

Referenced by [6], [7], [12].

Overlap of [2] baa=c with [3] abcc=d:

Critical pair: bad=cbcc.

Referenced by [17], [18], [26].

Overlap of [4] acbbbabba=1 with [2] baa=c:

Critical pair: acbbbabc=a.

Referenced by [7], [9].

Overlap of [4] acbbbabba=1 with [6] acbbbabc=a:

Critical pair: acbbbabba=cbbbabc.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [3] abcc=d with [7] cbbbabc=1:

Critical pair: abc=dbbbabc.

Flip LHS and RHS.

Referenced by [11].

Overlap of [6] acbbbabc=a with [7] cbbbabc=1:

Critical pair: acbbbab=abbbabc.

Referenced by [12].

Overlap of [7] cbbbabc=1 with [7] cbbbabc=1:

Critical pair: cbbbab=bbbabc.

Referenced by [11], [13], [23], [27].

Overlap of [8] dbbbabc=abc with [7] cbbbabc=1:

Critical pair: dbbbab=abcbbbabc.

Reduce RHS:

Referenced by [14].

Overlap of [4] acbbbabba=1 with [9] acbbbab=abbbabc:

Critical pair: abbbabcba=1.

Referenced by [23].

Overlap of [7] cbbbabc=1 with [10] cbbbab=bbbabc:

Critical pair: bbbabcc=1.

Reduce LHS:

Referenced by [14], [15], [20], [23], [34], [36], [39], [41], [44], [46].

Simplify [11] dbbbab=abbbbd.

Reduce RHS:

Referenced by [15].

Overlap of [14] dbbbab=ab with [13] bbbd=1:

Critical pair: dbbba=abbbd.

Reduce RHS:

Referenced by [16], [17].

Overlap of [15] dbbba=a with [2] baa=c:

Critical pair: dbbc=aa.

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] dbbba=a with [5] bad=cbcc:

Critical pair: dbbcbcc=ad.

Flip LHS and RHS.

Referenced by [22].

Overlap of [2] baa=c with [16] aa=dbbc:

Critical pair: badbbc=ca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [19], [25].

Overlap of [3] abcc=d with [18] ca=cbccbbc:

Critical pair: abccbccbbc=da.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [13] bbbd=1 with [19] da=dbccbbc:

Critical pair: bbbdbccbbc=a.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

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

Overlap of [3] abcc=d with [20] a=bccbbc:

Critical pair: bccbbcbcc=d.

Referenced by [23], [25], [30], [32], [35].

Overlap of [17] ad=dbbcbcc with [20] a=bccbbc:

Critical pair: bccbbcd=dbbcbcc.

Flip LHS and RHS.

Defines rule #5.

Referenced by [33].

Simplify [12] abbbabcba=1.

Reduce LHS:

Referenced by [24], [29].

Overlap of [23] bccbbbbccbbc=1 with [23] bccbbbbccbbc=1:

Critical pair: bccbbbbccb=cbbbbccbbc.

Referenced by [29], [40], [50].

Overlap of [2] baa=c with [20] a=bccbbc:

Critical pair: bbccbbca=c.

Reduce LHS:

Referenced by [30], [31], [33], [37], [38].

Overlap of [5] bad=cbcc with [20] a=bccbbc:

Critical pair: bbccbbcd=cbcc.

Referenced by [31], [43], [45].

Simplify [10] cbbbab=bbbabc.

Reduce RHS:

Referenced by [28].

Overlap of [27] cbbbab=bbbbccbbcbc with [20] a=bccbbc:

Critical pair: cbbbbccbbcb=bbbbccbbcbc.

Flip LHS and RHS.

Referenced by [29], [40], [51].

Overlap of [23] bccbbbbccbbc=1 with [24] bccbbbbccb=cbbbbccbbc:

Critical pair: cbbbbccbbcbc=1.

Reduce LHS:

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

Overlap of [25] bdbbc=c with [21] bccbbcbcc=d:

Critical pair: bdbd=ccbbcbcc.

Flip LHS and RHS.

Referenced by [32], [33], [46], [48], [49], [53].

Overlap of [25] bdbbc=c with [26] bbccbbcd=cbcc:

Critical pair: bdcbcc=ccbbcd.

Referenced by [33].

Overlap of [21] bccbbcbcc=d with [30] ccbbcbcc=bdbd:

Critical pair: bccbbcbcbdbd=dcbbcbcc.

Flip LHS and RHS.

Referenced by [54].

Overlap of [31] bdcbcc=ccbbcd with [30] ccbbcbcc=bdbd:

Critical pair: bdcbbdbd=ccbbcdbbcbcc.

Reduce RHS:

Referenced by [34].

Overlap of [13] bbbd=1 with [33] bdcbbdbd=bdcd:

Critical pair: bbbdcd=cbbdbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [21] bccbbcbcc=d with [34] cbbdbd=cd:

Critical pair: bccbbcbccd=dbbdbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [13] bbbd=1 with [35] dbbdbd=dd:

Critical pair: bbbdd=bbdbd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [37].

Overlap of [36] bbdbd=d with [25] bdbbc=c:

Critical pair: bbdc=dbbc.

Referenced by [40].

Overlap of [25] bdbbc=c with [29] ccbbbbccbbcb=1:

Critical pair: bdbb=ccbbbbccbbcb.

Reduce RHS:

Referenced by [40], [41], [42].

Overlap of [29] ccbbbbccbbcb=1 with [13] bbbd=1:

Critical pair: ccbbbbccbbc=bbd.

Referenced by [40].

Overlap of [37] bbdc=dbbc with [29] ccbbbbccbbcb=1:

Critical pair: bbd=dbbccbbbbccbbcb.

Reduce RHS:

Referenced by [41].

Overlap of [38] bdbb=1 with [13] bbbd=1:

Critical pair: bdb=bbd.

Reduce RHS:

Referenced by [42].

Overlap of [38] bdbb=1 with [41] bdb=dbb:

Critical pair: dbbb=1.

Defines rule #1.

Referenced by [43], [44], [45], [48], [55], [57], [59], [60], [61], [63], [64], [66].

Overlap of [26] bbccbbcd=cbcc with [42] dbbb=1:

Critical pair: bbccbbc=cbccbbb.

Defines rule #3.

Referenced by [46], [47], [50], [51], [52], [58].

Overlap of [42] dbbb=1 with [13] bbbd=1:

Critical pair: db=bd.

Flip LHS and RHS.

Defines rule #2.

Referenced by [46], [48], [49], [53], [54], [55], [63], [64], [65].

Overlap of [42] dbbb=1 with [26] bbccbbcd=cbcc:

Critical pair: dbcbcc=ccbbcd.

Defines rule #4.

Overlap of [43] bbccbbc=cbccbbb with [30] ccbbcbcc=bdbd:

Critical pair: bbbdbd=cbccbbbbcc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [48], [49].

Overlap of [43] bbccbbc=cbccbbb with [43] bbccbbc=cbccbbb:

Critical pair: bbcccbccbbb=cbccbbbcbbc.

Referenced by [63].

Overlap of [30] ccbbcbcc=bdbd with [46] cbccbbbbcc=db:

Critical pair: ccbbcbcdb=bdbdbccbbbbcc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [59].

Overlap of [46] cbccbbbbcc=db with [30] ccbbcbcc=bdbd:

Critical pair: cbccbbbbcbdbd=dbcbbcbcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Simplify [24] bccbbbbccb=cbbbbccbbc.

Reduce RHS:

Referenced by [55], [56].

Simplify [28] bbbbccbbcbc=cbbbbccbbcb.

Reduce RHS:

Referenced by [52].

Overlap of [51] bbbbccbbcbc=cbbcbccbbbb with [43] bbccbbc=cbccbbb:

Critical pair: bbcbccbbbbc=cbbcbccbbbb.

Referenced by [61], [62].

Simplify [30] ccbbcbcc=bdbd.

Reduce RHS:

Defines rule #12.

Simplify [32] dcbbcbcc=bccbbcbcbdbd.

Reduce RHS:

Defines rule #9.

Overlap of [50] bccbbbbccb=cbbcbccbbb with [44] bd=db:

Critical pair: bccbbbbccdb=cbbcbccbbbd.

Reduce RHS:

Referenced by [56], [57], [58], [59], [60].

Overlap of [50] bccbbbbccb=cbbcbccbbb with [55] bccbbbbccdb=cbbcbcc:

Critical pair: bccbbbcbbcbcc=cbbcbccbbbbbbccdb.

Defines rule #14.

Overlap of [42] dbbb=1 with [55] bccbbbbccdb=cbbcbcc:

Critical pair: dbbcbbcbcc=ccbbbbccdb.

Defines rule #11.

Referenced by [61].

Overlap of [43] bbccbbc=cbccbbb with [55] bccbbbbccdb=cbbcbcc:

Critical pair: bbccbcbbcbcc=cbccbbbcbbbbccdb.

Defines rule #15.

Overlap of [48] dccbbbbcc=ccbbcbcdb with [55] bccbbbbccdb=cbbcbcc:

Critical pair: dccbbbcbbcbcc=ccbbcbcdbbbbbccdb.

Reduce RHS:

Defines rule #16.

Overlap of [55] bccbbbbccdb=cbbcbcc with [42] dbbb=1:

Critical pair: bccbbbbcc=cbbcbccbb.

Defines rule #6.

Overlap of [42] dbbb=1 with [52] bbcbccbbbbc=cbbcbccbbbb:

Critical pair: dbbcbbcbccbbbb=bcbccbbbbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [62].

Overlap of [61] bcbccbbbbc=ccbbbbccbb with [52] bbcbccbbbbc=cbbcbccbbbb:

Critical pair: bcbccbbcbbcbccbbbb=ccbbbbccbbbccbbbbc.

Referenced by [64].

Overlap of [47] bbcccbccbbb=cbccbbbcbbc with [44] bd=db:

Critical pair: bbcccbccbbdb=cbccbbbcbbcd.

Reduce LHS:

Defines rule #13.

Overlap of [62] bcbccbbcbbcbccbbbb=ccbbbbccbbbccbbbbc with [44] bd=db:

Critical pair: bcbccbbcbbcbccbbbdb=ccbbbbccbbbccbbbbcd.

Reduce LHS:

Referenced by [65].

Overlap of [64] bcbccbbcbbcbccb=ccbbbbccbbbccbbbbcd with [44] bd=db:

Critical pair: bcbccbbcbbcbccdb=ccbbbbccbbbccbbbbcdd.

Referenced by [66].

Overlap of [65] bcbccbbcbbcbccdb=ccbbbbccbbbccbbbbcdd with [42] dbbb=1:

Critical pair: bcbccbbcbbcbcc=ccbbbbccbbbccbbbbcddbb.

Defines rule #17.