Certificate for #3181 ⟨a, b | abaaaabbaab=1⟩

Completion settings:

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

Axiom: abaaaabbaab=1.

Referenced by [4].

Axiom: abaaaa=c.

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

Axiom: cbba=d.

Referenced by [4], [6], [8], [10], [13].

Overlap of [1] abaaaabbaab=1 with [2] abaaaa=c:

Critical pair: cbbaab=1.

Reduce LHS:

Referenced by [5], [9], [20].

Overlap of [4] dab=1 with [2] abaaaa=c:

Critical pair: dc=aaaa.

Flip LHS and RHS.

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

Overlap of [3] cbba=d with [5] aaaa=dc:

Critical pair: cbbdc=daaa.

Flip LHS and RHS.

Referenced by [12], [15].

Overlap of [2] abaaaa=c with [5] aaaa=dc:

Critical pair: abdc=c.

Referenced by [8].

Overlap of [7] abdc=c with [3] cbba=d:

Critical pair: abdd=cbba.

Reduce RHS:

Referenced by [9].

Overlap of [8] abdd=d with [4] dab=1:

Critical pair: abd=dab.

Reduce RHS:

Referenced by [10], [11], [12], [14], [17].

Overlap of [3] cbba=d with [9] abd=1:

Critical pair: cbb=dbd.

Referenced by [12], [13], [15], [18], [19].

Overlap of [5] aaaa=dc with [9] abd=1:

Critical pair: aaa=dcbd.

Referenced by [12].

Overlap of [9] abd=1 with [6] daaa=cbbdc:

Critical pair: abcbbdc=aaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [3] cbba=d with [10] cbb=dbd:

Critical pair: dbda=d.

Referenced by [14].

Overlap of [9] abd=1 with [13] dbda=d:

Critical pair: abd=bda.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [14] bda=1 with [6] daaa=cbbdc:

Critical pair: bcbbdc=aa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [16].

Overlap of [14] bda=1 with [15] aa=bdbddc:

Critical pair: bdbdbddc=a.

Flip LHS and RHS.

Defines rule #8.

Referenced by [17].

Overlap of [9] abd=1 with [16] a=bdbdbddc:

Critical pair: bdbdbddcbd=1.

Reduce LHS:

Defines rule #5.

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

Overlap of [10] cbb=dbd with [17] bdbdbdbddc=1:

Critical pair: cb=dbddbdbdbddc.

Defines rule #6.

Referenced by [24].

Overlap of [17] bdbdbdbddc=1 with [10] cbb=dbd:

Critical pair: bdbdbdbdddbd=bb.

Referenced by [20].

Overlap of [4] dab=1 with [19] bdbdbdbdddbd=bb:

Critical pair: dabb=dbdbdbdddbd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [20] dbdbdbdddbd=b with [17] bdbdbdbddc=1:

Critical pair: dbdbdbddd=bbdbdbddc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [20] dbdbdbdddbd=b with [20] dbdbdbdddbd=b:

Critical pair: dbdbdbddb=bbdbdddbd.

Flip LHS and RHS.

Defines rule #1.

Referenced by [24].

Overlap of [20] dbdbdbdddbd=b with [20] dbdbdbdddbd=b:

Critical pair: dbdbdbdddbb=bbdbdbdddbd.

Flip LHS and RHS.

Defines rule #2.

Overlap of [18] cb=dbddbdbdbddc with [22] bbdbdddbd=dbdbdbddb:

Critical pair: cdbdbdbddb=dbddbdbdbddcbdbdddbd.

Reduce RHS:

Referenced by [25].

Overlap of [24] cdbdbdbddb=dbddbdddbd with [20] dbdbdbdddbd=b:

Critical pair: cdbdbdbdb=dbddbdddbddbdbdddbd.

Referenced by [26].

Overlap of [25] cdbdbdbdb=dbddbdddbddbdbdddbd with [17] bdbdbdbddc=1:

Critical pair: cd=dbddbdddbddbdbdddbdddc.

Defines rule #7.