Certificate for #478 ⟨a, b, c | ba=ac, bcb=1⟩

Back:⟨a, b, c | ba=ac, bcb=1⟩

Completion settings:

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[2] bcb=1

Axiom: bcb=1.

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

[3] bc=cb

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

bc b bcb

Critical pair: bc=cb.

Defines rule #1.

Referenced by [4], [6].

[4] cbb=1

Overlap of [2] bcb=1 with [3] bc=cb:

bcb bc

Critical pair: cbb=1.

Defines rule #3.

Referenced by [5].

[5] babb=a

Overlap of [1] ac=ba with [4] cbb=1:

a c cbb

Critical pair: a=babb.

Flip LHS and RHS.

Referenced by [6].

[6] abb=cba

Overlap of [2] bcb=1 with [5] babb=a:

bc b babb

Critical pair: bca=abb.

Reduce LHS:

[3](bc)a
⇒ cba

Flip LHS and RHS.

Defines rule #4.