Certificate for #3456 ⟨a, b, c | ba=ac, acc=b⟩

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

Completion settings:

[1] ba=ac

Axiom: ba=ac.

Defines rule #1.

Referenced by [3].

[2] acc=b

Axiom: acc=b.

Defines rule #3.

Referenced by [3].

[3] bc=bb

Overlap of [1] ba=ac with [2] acc=b:

b a acc

Critical pair: bb=accc.

Reduce RHS:

[2](acc)c
⇒ bc

Flip LHS and RHS.

Defines rule #2.