Certificate for #5438 ⟨a, b, c | ab=a, cbac=b⟩

Back:⟨a, b, c | ab=a, cbac=b⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [4].

[2] cbac=b

Axiom: cbac=b.

Defines rule #4.

Referenced by [3].

[3] bbac=cba

Overlap of [2] cbac=b with [2] cbac=b:

cba c cbac

Critical pair: cbab=bbac.

Reduce LHS:

[1]cb(ab)
⇒ cba

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] aac=acba

Overlap of [1] ab=a with [3] bbac=cba:

a b bbac

Critical pair: acba=abac.

Reduce RHS:

[1](ab)ac
⇒ aac

Flip LHS and RHS.

Defines rule #2.