Certificate for #564 ⟨a, b, c | ca=bc, cc=c⟩

Back:⟨a, b, c | ca=bc, cc=c⟩

Completion settings:

[1] ca=bc

Axiom: ca=bc.

Referenced by [5], [7].

[2] cc=c

Axiom: cc=c.

Defines rule #6.

Referenced by [4], [5].

[3] cb=d

Axiom: cb=d.

Defines rule #5.

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

[4] cd=d

Overlap of [2] cc=c with [3] cb=d:

c c cb

Critical pair: cd=cb.

Reduce RHS:

[3](cb)
⇒ d

Defines rule #4.

[5] bc=dc

Overlap of [2] cc=c with [1] ca=bc:

c c ca

Critical pair: cbc=ca.

Reduce LHS:

[3](cb)c
⇒ dc

Reduce RHS:

[1](ca)
⇒ bc

Flip LHS and RHS.

Defines rule #2.

Referenced by [6], [7].

[6] bd=dd

Overlap of [5] bc=dc with [3] cb=d:

b c cb

Critical pair: bd=dcb.

Reduce RHS:

[3]d(cb)
⇒ dd

Defines rule #1.

[7] ca=dc

Simplify [1] ca=bc.

Reduce RHS:

[5](bc)
⇒ dc

Defines rule #3.