Certificate for #6095 ⟨a, b, c | ab=c, bcc=ca⟩

Completion settings:

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

Axiom: ab=c.

Defines rule #2.

Referenced by [6], [8].

Axiom: bcc=ca.

Flip LHS and RHS.

Referenced by [4].

Axiom: cc=d.

Defines rule #6.

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

Simplify [2] ca=bcc.

Reduce RHS:

Defines rule #7.

Referenced by [6], [7].

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

Critical pair: cd=dc.

Defines rule #4.

Referenced by [8].

Overlap of [4] ca=bd with [1] ab=c:

Critical pair: cc=bdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [8], [9].

Overlap of [3] cc=d with [4] ca=bd:

Critical pair: cbd=da.

Defines rule #5.

Overlap of [1] ab=c with [6] bdb=d:

Critical pair: ad=cdb.

Reduce RHS:

Defines rule #8.

Overlap of [6] bdb=d with [6] bdb=d:

Critical pair: bdd=ddb.

Defines rule #3.