Certificate for #5850 ⟨a, b, c | ab=a, bab=cc⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [2], [4].

[2] cc=ba

Axiom: bab=cc.

Reduce LHS:

[1]b(ab)
⇒ ba

Flip LHS and RHS.

Defines rule #4.

Referenced by [3].

[3] bac=cba

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

c c cc

Critical pair: cba=bac.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4].

[4] aac=acba

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

a b bac

Critical pair: acba=aac.

Flip LHS and RHS.

Defines rule #2.