Certificate for #3587 ⟨a, b, c | ba=ab, cc=ab⟩

Back:⟨a, b, c | ba=ab, cc=ab⟩

Completion settings:

[1] ba=ab

Axiom: ba=ab.

Referenced by [3].

[2] ab=cc

Axiom: cc=ab.

Flip LHS and RHS.

Defines rule #1.

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

[3] ba=cc

Simplify [1] ba=ab.

Reduce RHS:

[2](ab)
⇒ cc

Defines rule #2.

Referenced by [4], [5].

[4] bcc=ccb

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

b a ab

Critical pair: bcc=ccb.

Defines rule #4.

[5] acc=cca

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

a b ba

Critical pair: acc=cca.

Defines rule #3.