Certificate for #252 ⟨a, b, c | ab=1, bca=c⟩

Back:⟨a, b, c | ab=1, bca=c⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #3.

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

[2] bca=c

Axiom: bca=c.

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

[3] ac=d

Axiom: ac=d.

Defines rule #5.

Referenced by [4], [6], [8].

[4] ca=d

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

a b bca

Critical pair: ac=ca.

Reduce LHS:

[3](ac)
⇒ d

Flip LHS and RHS.

Defines rule #8.

Referenced by [6], [7], [8], [9].

[5] cb=bc

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

bc a ab

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #6.

[6] ad=da

Overlap of [3] ac=d with [4] ca=d:

a c ca

Critical pair: ad=da.

Defines rule #4.

[7] db=c

Overlap of [4] ca=d with [1] ab=1:

c a ab

Critical pair: c=db.

Flip LHS and RHS.

Defines rule #2.

[8] cd=dc

Overlap of [4] ca=d with [3] ac=d:

c a ac

Critical pair: cd=dc.

Defines rule #7.

[9] bd=c

Overlap of [2] bca=c with [4] ca=d:

b ca ca

Critical pair: bd=c.

Defines rule #1.