Certificate for #1109 ⟨a, b, c | aa=1, bbccb=1⟩

Completion settings:

• Auxiliary generators:
  1. d = bbb
• Reduction order:
  • Left-to-right shortlex with a < b < c < d

Axiom: aa=1.

Defines rule #1.

Axiom: bbccb=1.

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

Axiom: bbb=d.

Defines rule #4.

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

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

Critical pair: bd=db.

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

Overlap of [2] bbccb=1 with [3] bbb=d:

Critical pair: bbccd=bb.

Referenced by [8].

Overlap of [3] bbb=d with [2] bbccb=1:

Critical pair: b=dccb.

Flip LHS and RHS.

Referenced by [7].

Overlap of [6] dccb=b with [2] bbccb=1:

Critical pair: dcc=bbccb.

Reduce RHS:

Referenced by [10].

Overlap of [2] bbccb=1 with [5] bbccd=bb:

Critical pair: bbccbb=bccd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [9].

Overlap of [2] bbccb=1 with [8] bccd=b:

Critical pair: bbccb=ccd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #6.

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

Overlap of [7] dcc=1 with [9] ccd=1:

Critical pair: dc=cd.

Defines rule #3.

Referenced by [12], [13].

Overlap of [9] ccd=1 with [4] db=bd:

Critical pair: ccbd=b.

Referenced by [12].

Overlap of [11] ccbd=b with [10] dc=cd:

Critical pair: ccbcd=bc.

Referenced by [13].

Overlap of [12] ccbcd=bc with [10] dc=cd:

Critical pair: ccbccd=bcc.

Reduce LHS:

Defines rule #5.