Certificate for #1112 ⟨a, b, c | aa=1, bcbbc=1⟩

Back:⟨a, b, c | aa=1, bcbbc=1⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

[2] bcbbc=1

Axiom: bcbbc=1.

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

[3] bcb=bbc

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

bcb bc bcbbc

Critical pair: bcb=bbc.

Referenced by [4], [5].

[4] bbbcc=1

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

bcbbc bcb

Critical pair: bbcbc=1.

Reduce LHS:

[3]b(bcb)c
⇒ bbbcc

Defines rule #3.

Referenced by [5].

[5] bbccb=1

Overlap of [3] bcb=bbc with [3] bcb=bbc:

bc b bcb

Critical pair: bcbbc=bbccb.

Reduce LHS:

[3](bcb)bc
[3]⇒ b(bcb)c
[4]⇒ (bbbcc)
⇒ 1

Flip LHS and RHS.

Referenced by [6].

[6] cb=bc

Overlap of [2] bcbbc=1 with [5] bbccb=1:

bc bbc bbccb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #2.