Certificate for #22860 ⟨a, b | aaa=1, bbbbb=aba⟩

Completion settings:

• Auxiliary generators:
  1. c = aa
  2. d = cbbbbcbbbbcb
• Reduction order:
  • Left-to-right recursive path with deg(d) = deg(b) = 0, d < b; deg(c) = 1; deg(a) = 2

Axiom: aaa=1.

Referenced by [5].

Axiom: bbbbb=aba.

Flip LHS and RHS.

Referenced by [9].

Axiom: aa=c.

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

Axiom: cbbbbcbbbbcb=d.

Referenced by [18], [19], [20], [21], [22], [23], [27], [37].

Overlap of [1] aaa=1 with [3] aa=c:

Critical pair: ca=1.

Referenced by [6], [7].

Overlap of [3] aa=c with [3] aa=c:

Critical pair: ac=ca.

Reduce RHS:

Referenced by [8].

Overlap of [5] ca=1 with [3] aa=c:

Critical pair: cc=a.

Flip LHS and RHS.

Defines rule #20.

Referenced by [8], [9].

Simplify [6] ac=1.

Reduce LHS:

Defines rule #18.

Referenced by [10], [11], [12], [20].

Simplify [2] aba=bbbbb.

Reduce LHS:

Referenced by [10], [11].

Overlap of [9] ccbcc=bbbbb with [8] ccc=1:

Critical pair: ccb=bbbbbc.

Referenced by [12], [13], [21], [28], [45], [48].

Overlap of [8] ccc=1 with [9] ccbcc=bbbbb:

Critical pair: cbbbbb=bcc.

Flip LHS and RHS.

Defines rule #15.

Referenced by [15], [16], [18], [22], [31], [32].

Overlap of [8] ccc=1 with [10] ccb=bbbbbc:

Critical pair: cbbbbbc=b.

Referenced by [13], [14], [15], [19], [23], [29], [34].

Overlap of [10] ccb=bbbbbc with [12] cbbbbbc=b:

Critical pair: cb=bbbbbcbbbbc.

Flip LHS and RHS.

Referenced by [17], [23], [24].

Overlap of [12] cbbbbbc=b with [12] cbbbbbc=b:

Critical pair: cbbbbbb=bbbbbbc.

Flip LHS and RHS.

Referenced by [16], [22].

Overlap of [12] cbbbbbc=b with [11] bcc=cbbbbb:

Critical pair: cbbbbcbbbbb=bc.

Referenced by [16], [17], [19], [22], [35], [38].

Overlap of [11] bcc=cbbbbb with [15] cbbbbcbbbbb=bc:

Critical pair: bcbc=cbbbbbbbbbcbbbbb.

Reduce RHS:

Referenced by [56].

Overlap of [15] cbbbbcbbbbb=bc with [13] bbbbbcbbbbc=cb:

Critical pair: cbbbbcbbbcb=bcbbbcbbbbc.

Flip LHS and RHS.

Referenced by [21].

Overlap of [4] cbbbbcbbbbcb=d with [11] bcc=cbbbbb:

Critical pair: cbbbbcbbbbccbbbbb=dcc.

Reduce LHS:

Referenced by [39].

Overlap of [4] cbbbbcbbbbcb=d with [15] cbbbbcbbbbb=bc:

Critical pair: cbbbbbc=dbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [24], [25], [26], [29], [30], [45].

Overlap of [8] ccc=1 with [4] cbbbbcbbbbcb=d:

Critical pair: ccd=bbbbcbbbbcb.

Flip LHS and RHS.

Referenced by [21], [40].

Overlap of [10] ccb=bbbbbc with [4] cbbbbcbbbbcb=d:

Critical pair: cd=bbbbbcbbbcbbbbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [11] bcc=cbbbbb with [4] cbbbbcbbbbcb=d:

Critical pair: bcd=cbbbbbbbbbcbbbbcb.

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [13] bbbbbcbbbbc=cb with [4] cbbbbcbbbbcb=d:

Critical pair: bbbbbd=cbbbbbcb.

Reduce RHS:

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

Overlap of [19] dbbbb=b with [13] bbbbbcbbbbc=cb:

Critical pair: dcb=bbcbbbbc.

Flip LHS and RHS.

Referenced by [33], [40].

Overlap of [19] dbbbb=b with [23] bbbbbd=bb:

Critical pair: dbb=bbd.

Flip LHS and RHS.

Referenced by [26], [29], [36], [40].

Overlap of [19] dbbbb=b with [25] bbd=dbb:

Critical pair: dbbdbb=bd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [27], [28], [29], [42], [43], [44], [46], [51], [54], [55], [57].

Overlap of [4] cbbbbcbbbbcb=d with [26] bd=db:

Critical pair: cbbbbcbbbbcdb=dd.

Reduce LHS:

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

Overlap of [10] ccb=bbbbbc with [26] bd=db:

Critical pair: ccdb=bbbbbcd.

Referenced by [32], [33].

Overlap of [12] cbbbbbc=b with [27] bcdbbcdb=dd:

Critical pair: cbbbbdd=bdbbcdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [31], [32].

Overlap of [27] bcdbbcdb=dd with [19] dbbbb=b:

Critical pair: bcdbbcb=ddbbb.

Referenced by [37].

Overlap of [27] bcdbbcdb=dd with [29] dbbbcdb=cdb:

Critical pair: bcdbbccdb=ddbbcdb.

Reduce LHS:

Referenced by [39].

Overlap of [29] dbbbcdb=cdb with [29] dbbbcdb=cdb:

Critical pair: dbbbccdb=cdbbbcdb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [33].

Simplify [21] ccdbbcbb=cd.

Reduce LHS:

Referenced by [34], [35], [36].

Overlap of [33] ddcbbb=cd with [12] cbbbbbc=b:

Critical pair: ddb=cdbbc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [42].

Overlap of [33] ddcbbb=cd with [15] cbbbbcbbbbb=bc:

Critical pair: ddbc=cdbcbbbbb.

Flip LHS and RHS.

Referenced by [49].

Overlap of [25] bbd=dbb with [33] ddcbbb=cd:

Critical pair: bbcd=dbbdcbbb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [4] cbbbbcbbbbcb=d with [22] cbbbbcbb=bcd:

Critical pair: bcdbbcb=d.

Reduce LHS:

Defines rule #2.

Referenced by [41], [42], [46], [47], [52], [54], [59], [60].

Overlap of [15] cbbbbcbbbbb=bc with [22] cbbbbcbb=bcd:

Critical pair: bcdbbb=bc.

Defines rule #5.

Referenced by [39], [41], [50], [51], [53], [57].

Overlap of [18] cbbbbcbbbcbbbbbbbbbb=dcc with [22] cbbbbcbb=bcd:

Critical pair: bcdbcbbbbbbbbbb=dcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [54].

Overlap of [20] bbbbcbbbbcb=ccd with [24] bbcbbbbc=dcb:

Critical pair: bbdcbb=ccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [45].

Overlap of [37] ddbbb=d with [38] bcdbbb=bc:

Critical pair: ddbbbc=dcdbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [57], [60].

Overlap of [34] cdbbc=ddb with [34] cdbbc=ddb:

Critical pair: cdbbddb=ddbdbbc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [43], [52], [55], [58].

Overlap of [26] bd=db with [42] ddc=cdd:

Critical pair: bcdd=dbdc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [44], [49], [52], [55], [58].

Overlap of [26] bd=db with [43] ddbc=bcdd:

Critical pair: bbcdd=dbdbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [46], [55], [58].

Overlap of [40] ccd=dbbcbb with [19] dbbbb=b:

Critical pair: ccb=dbbcbbbbbb.

Reduce LHS:

Referenced by [48].

Overlap of [26] bd=db with [44] ddbbc=bbcdd:

Critical pair: bbbcdd=dbdbbc.

Reduce RHS:

Referenced by [47].

Overlap of [46] bbbcdd=dc with [37] ddbbb=d:

Critical pair: bbbcd=dcbbb.

Referenced by [50], [57].

Simplify [10] ccb=bbbbbc.

Reduce RHS:

Defines rule #11.

Simplify [35] cdbcbbbbb=ddbc.

Reduce RHS:

Referenced by [51], [52].

Overlap of [47] bbbcd=dcbbb with [38] bcdbbb=bc:

Critical pair: bbbc=dcbbbbbb.

Defines rule #8.

Referenced by [56], [57].

Overlap of [49] cdbcbbbbb=bcdd with [26] bd=db:

Critical pair: cdbcbbbbdb=bcddd.

Reduce LHS:

Referenced by [55].

Overlap of [42] ddc=cdd with [49] cdbcbbbbb=bcdd:

Critical pair: ddbcdd=cdddbcbbbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [53].

Overlap of [52] cdbcdbb=bcdddd with [38] bcdbbb=bc:

Critical pair: cdbc=bcddddb.

Defines rule #12.

Referenced by [54], [55].

Overlap of [39] dcc=bbcdbb with [53] cdbc=bcddddb:

Critical pair: dcbcddddb=bbcdbbdbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [55].

Overlap of [51] cdbcbb=bcddd with [54] bbcdc=dcbcddddb:

Critical pair: cdbcdcbcddddb=bcdddcdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [57].

Simplify [16] bcbc=cbbbcbbbbbbbbbbb.

Reduce RHS:

Defines rule #16.

Overlap of [47] bbbcd=dcbbb with [55] bcdcdcdd=bbcbbcddddddddddddb:

Critical pair: bbbbcbbcddddddddddddb=dcbbbcdcdd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [58].

Overlap of [42] ddc=cdd with [57] dcdcdc=dbcbbcddddddddddb:

Critical pair: ddbcbbcddddddddddb=cdddcdc.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [59].

Overlap of [58] cdcdcdd=bcbbcddddddddddddb with [37] ddbbb=d:

Critical pair: cdcdcd=bcbbcddddddddddddbbbb.

Reduce RHS:

Referenced by [60].

Overlap of [59] cdcdcd=bcbbcdddddddddddb with [41] dcdbbb=dc:

Critical pair: cdcdc=bcbbcdddddddddddbbbb.

Reduce RHS:

Defines rule #19.