Certificate for #3231 ⟨a, b, c | ba=ac, bbcb=1⟩

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

Completion settings:

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[2] bbcb=1

Axiom: bbcb=1.

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

[3] bbc=bcb

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

bbc b bbcb

Critical pair: bbc=bcb.

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

[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 #1.

Referenced by [6], [8].

[6] cbbb=1

Simplify [4] bcbb=1.

Reduce LHS:

[5](bc)bb
⇒ cbbb

Defines rule #3.

Referenced by [7].

[7] babbb=a

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

a c cbbb

Critical pair: a=babbb.

Flip LHS and RHS.

Referenced by [8].

[8] abbb=cbba

Overlap of [2] bbcb=1 with [7] babbb=a:

bbc b babbb

Critical pair: bbca=abbb.

Reduce LHS:

[3](bbc)a
[5]⇒ (bc)ba
⇒ cbba

Flip LHS and RHS.

Defines rule #4.