Certificate for #3423 ⟨a, b, c | ba=ab, aca=b⟩

Back:⟨a, b, c | ba=ab, aca=b⟩

Completion settings:

[1] ab=ba

Axiom: ba=ab.

Flip LHS and RHS.

Referenced by [3].

[2] b=aca

Axiom: aca=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] ab=acaa

Simplify [1] ab=ba.

Reduce RHS:

[2](b)a
⇒ acaa

Referenced by [4].

[4] acaa=aaca

Overlap of [3] ab=acaa with [2] b=aca:

a b b

Critical pair: aaca=acaa.

Flip LHS and RHS.

Defines rule #1.