Certificate for #5929 ⟨a, b, c | ab=a, cac=bc⟩

Back:⟨a, b, c | ab=a, cac=bc⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3].

[2] cac=bc

Axiom: cac=bc.

Defines rule #3.

Referenced by [3].

[3] bbc=bc

Overlap of [2] cac=bc with [2] cac=bc:

ca c cac

Critical pair: cabc=bcac.

Reduce LHS:

[1]c(ab)c
[2]⇒ (cac)
⇒ bc

Reduce RHS:

[2]b(cac)
⇒ bbc

Flip LHS and RHS.

Defines rule #2.