Certificate for #3047 ⟨a, b | aabaabbbaab=1⟩

Completion settings:

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

Axiom: aabaabbbaab=1.

Referenced by [4].

Axiom: aa=c.

Defines rule #6.

Referenced by [4], [5].

Axiom: cbcbc=d.

Defines rule #7.

Referenced by [6], [7], [8], [9], [12], [13], [14], [17], [18], [21].

Overlap of [1] aabaabbbaab=1 with [2] aa=c:

Critical pair: cbaabbbaab=1.

Reduce LHS:

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

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

Critical pair: ac=ca.

Defines rule #5.

Referenced by [7].

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

Critical pair: cbd=dbc.

Flip LHS and RHS.

Referenced by [18], [25].

Overlap of [5] ac=ca with [3] cbcbc=d:

Critical pair: ad=cabcbc.

Flip LHS and RHS.

Referenced by [12].

Overlap of [3] cbcbc=d with [4] cbcbbbcb=1:

Critical pair: cb=dbbbcb.

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] cbcbbbcb=1 with [3] cbcbc=d:

Critical pair: cbcbbbd=cbc.

Referenced by [14], [19].

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

Critical pair: cbcbbb=cbbbcb.

Flip LHS and RHS.

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

Overlap of [8] dbbbcb=cb with [4] cbcbbbcb=1:

Critical pair: dbbb=cbcbbbcb.

Reduce RHS:

Referenced by [13], [14], [15], [17], [18], [20], [23].

Overlap of [3] cbcbc=d with [7] cabcbc=ad:

Critical pair: cbcbad=dabcbc.

Flip LHS and RHS.

Referenced by [29].

Overlap of [10] cbbbcb=cbcbbb with [3] cbcbc=d:

Critical pair: cbbbd=cbcbbbcbc.

Reduce RHS:

Referenced by [16].

Overlap of [10] cbbbcb=cbcbbb with [9] cbcbbbd=cbc:

Critical pair: cbbbcbc=cbcbbbcbbbd.

Reduce LHS:

Reduce RHS:

Referenced by [15].

Overlap of [10] cbbbcb=cbcbbb with [10] cbbbcb=cbcbbb:

Critical pair: cbbbcbcbbb=cbcbbbbbcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [18], [19], [21], [24].

Overlap of [10] cbbbcb=cbcbbb with [13] cbbbd=c:

Critical pair: cbbbc=cbcbbbbbd.

Referenced by [18], [21].

Overlap of [3] cbcbc=d with [15] cbcbbbbbcb=bb:

Critical pair: cbbb=dbbbbbcb.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [6] dbc=cbd with [15] cbcbbbbbcb=bb:

Critical pair: dbbb=cbdbcbbbbbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20], [21], [22], [23], [24].

Overlap of [15] cbcbbbbbcb=bb with [9] cbcbbbd=cbc:

Critical pair: cbcbbbbbcbc=bbcbbbd.

Reduce LHS:

Reduce RHS:

Referenced by [21], [26].

Overlap of [11] dbbb=1 with [18] bbdb=1:

Critical pair: dbb=bdb.

Referenced by [21], [23].

Overlap of [15] cbcbbbbbcb=bb with [18] bbdb=1:

Critical pair: cbcbbbbbc=bbbdb.

Reduce LHS:

Reduce RHS:

Referenced by [26].

Overlap of [18] bbdb=1 with [18] bbdb=1:

Critical pair: bbd=bdb.

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [11] dbbb=1 with [22] bdb=bbd:

Critical pair: dbbbbd=db.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [25], [27], [28].

Overlap of [15] cbcbbbbbcb=bb with [22] bdb=bbd:

Critical pair: cbcbbbbbcbbd=bbdb.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [28], [29].

Overlap of [6] dbc=cbd with [23] db=bd:

Critical pair: bdc=cbd.

Referenced by [27].

Simplify [19] bbc=cbbbbbd.

Reduce RHS:

Defines rule #4.

Referenced by [27], [29].

Overlap of [23] db=bd with [26] bbc=cbb:

Critical pair: dcbb=bdbc.

Reduce RHS:

Referenced by [28].

Overlap of [27] dcbb=bcbd with [24] bbbd=1:

Critical pair: dc=bcbdbd.

Reduce RHS:

Defines rule #3.

Overlap of [24] bbbd=1 with [12] dabcbc=cbcbad:

Critical pair: bbbcbcbad=abcbc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.