Certificate for #5370 ⟨a, b, c | ab=a, bbca=c⟩

Back:⟨a, b, c | ab=a, bbca=c⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [4].

[2] bbca=c

Axiom: bbca=c.

Defines rule #5.

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

[3] aca=ac

Overlap of [1] ab=a with [2] bbca=c:

a b bbca

Critical pair: ac=abca.

Reduce RHS:

[1](ab)ca
⇒ aca

Flip LHS and RHS.

Defines rule #3.

[4] cb=c

Overlap of [2] bbca=c with [1] ab=a:

bbc a ab

Critical pair: bbca=cb.

Reduce LHS:

[2](bbca)
⇒ c

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] cca=cc

Overlap of [4] cb=c with [2] bbca=c:

c b bbca

Critical pair: cc=cbca.

Reduce RHS:

[4](cb)ca
⇒ cca

Flip LHS and RHS.

Defines rule #4.