Certificate for #3578 ⟨a, b, c | ac=ab, ca=bb⟩

Back:⟨a, b, c | ac=ab, ca=bb⟩

Completion settings:

[1] ac=ab

Axiom: ac=ab.

Defines rule #1.

Referenced by [3], [4].

[2] ca=bb

Axiom: ca=bb.

Defines rule #2.

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

[3] aba=abb

Overlap of [1] ac=ab with [2] ca=bb:

a c ca

Critical pair: abb=aba.

Flip LHS and RHS.

Defines rule #4.

[4] bbc=bbb

Overlap of [2] ca=bb with [1] ac=ab:

c a ac

Critical pair: cab=bbc.

Reduce LHS:

[2](ca)b
⇒ bbb

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] bbba=bbbb

Overlap of [4] bbc=bbb with [2] ca=bb:

bb c ca

Critical pair: bbbb=bbba.

Flip LHS and RHS.

Defines rule #5.