Certificate for #3452 ⟨a, b, c | ba=ac, acb=a⟩

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

Completion settings:

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Defines rule #1.

Referenced by [2].

[2] bab=a

Axiom: acb=a.

Reduce LHS:

[1](ac)b
⇒ bab

Defines rule #2.

Referenced by [3].

[3] aab=baa

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

ba b bab

Critical pair: baa=aab.

Flip LHS and RHS.

Defines rule #3.