Certificate for #6874 ⟨a, b, c | ab=1, abbcb=c⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #2.

Referenced by [2], [3].

[2] bcb=c

Axiom: abbcb=c.

Reduce LHS:

[1](ab)bcb
⇒ bcb

Defines rule #4.

Referenced by [3], [4].

[3] ac=cb

Overlap of [1] ab=1 with [2] bcb=c:

a b bcb

Critical pair: ac=cb.

Defines rule #1.

[4] bcc=ccb

Overlap of [2] bcb=c with [2] bcb=c:

bc b bcb

Critical pair: bcc=ccb.

Defines rule #3.