Certificate for #4889 ⟨a, b, c | ab=a, bcbbc=1⟩

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

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [6].

[2] bcbbc=1

Axiom: bcbbc=1.

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

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

Referenced by [5], [6].

[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 [7].

[6] acc=a

Overlap of [1] ab=a with [4] bbbcc=1:

a b bbbcc

Critical pair: a=abbcc.

Reduce RHS:

[1](ab)bcc
[1]⇒ (ab)cc
⇒ acc

Flip LHS and RHS.

Defines rule #3.

[7] 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.