Certificate for #3539 ⟨a, b, c | bb=ac, cba=a⟩

Completion settings:

[1] ac=bb

Axiom: bb=ac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4], [5].

[2] cba=a

Axiom: cba=a.

Defines rule #4.

Referenced by [3], [4].

[3] aa=bbba

Overlap of [1] ac=bb with [2] cba=a:

a c cba

Critical pair: aa=bbba.

Defines rule #5.

[4] cbbb=bb

Overlap of [2] cba=a with [1] ac=bb:

cb a ac

Critical pair: cbbb=ac.

Reduce RHS:

[1](ac)
⇒ bb

Defines rule #1.

Referenced by [5].

[5] abb=bbbbb

Overlap of [1] ac=bb with [4] cbbb=bb:

a c cbbb

Critical pair: abb=bbbbb.

Defines rule #3.