Certificate for #3168 ⟨a, b, c | ac=ab, bbcb=1⟩

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

Completion settings:

[1] ac=ab

Axiom: ac=ab.

Defines rule #3.

Referenced by [7].

[2] bbcb=1

Axiom: bbcb=1.

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

[3] bbc=bcb

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

bbc b bbcb

Critical pair: bbc=bcb.

Referenced by [4], [5].

[4] bcbb=1

Overlap of [2] bbcb=1 with [3] bbc=bcb:

bbcb bbc

Critical pair: bcbb=1.

Referenced by [5], [6].

[5] bc=cb

Overlap of [2] bbcb=1 with [3] bbc=bcb:

bbc b bbc

Critical pair: bbcbcb=bc.

Reduce LHS:

[3](bbc)bcb
[4]⇒ (bcbb)cb
⇒ cb

Flip LHS and RHS.

Defines rule #4.

Referenced by [6].

[6] cbbb=1

Simplify [4] bcbb=1.

Reduce LHS:

[5](bc)bb
⇒ cbbb

Defines rule #2.

Referenced by [7].

[7] abbbb=a

Overlap of [1] ac=ab with [6] cbbb=1:

a c cbbb

Critical pair: a=abbbb.

Flip LHS and RHS.

Defines rule #1.