Certificate for #5954 ⟨a, b, c | ab=a, cbc=ba⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [4].

[2] cbc=ba

Axiom: cbc=ba.

Defines rule #4.

Referenced by [3].

[3] bac=cbba

Overlap of [2] cbc=ba with [2] cbc=ba:

cb c cbc

Critical pair: cbba=babc.

Reduce RHS:

[1]b(ab)c
⇒ bac

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] aac=acbba

Overlap of [1] ab=a with [3] bac=cbba:

a b bac

Critical pair: acbba=aac.

Flip LHS and RHS.

Defines rule #2.