Certificate for #1315 ⟨a, b, c | ab=1, acac=a⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

[2] acac=a

Axiom: acac=a.

Defines rule #3.

Referenced by [3].

[3] aac=aca

Overlap of [2] acac=a with [2] acac=a:

ac ac acac

Critical pair: aca=aac.

Flip LHS and RHS.

Defines rule #2.