Certificate for #2309 ⟨a, b, c | aaa=a, bbcb=1⟩

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

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #2.

[2] bbcb=1

Axiom: bbcb=1.

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

[3] bcb=bbc

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

bbc b bbcb

Critical pair: bbc=bcb.

Flip LHS and RHS.

Referenced by [4], [5].

[4] cb=bc

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

bbc b bcb

Critical pair: bbcbbc=cb.

Reduce LHS:

[2](bbcb)bc
⇒ bc

Flip LHS and RHS.

Defines rule #1.

[5] bbbc=1

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

b bcb bcb

Critical pair: bbbc=1.

Defines rule #3.