Certificate for #3428 ⟨a, b, c | ba=ab, acc=b⟩

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

Completion settings:

[1] ab=ba

Axiom: ba=ab.

Flip LHS and RHS.

Referenced by [3].

[2] b=acc

Axiom: acc=b.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] ab=acca

Simplify [1] ab=ba.

Reduce RHS:

[2](b)a
⇒ acca

Referenced by [4].

[4] aacc=acca

Overlap of [3] ab=acca with [2] b=acc:

a b b

Critical pair: aacc=acca.

Defines rule #1.