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

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

[2] bcbbc=c

Axiom: bcbbc=c.

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

[3] cbbc=bcbc

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

bcb bc bcbbc

Critical pair: bcbc=cbbc.

Flip LHS and RHS.

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

[4] cbc=bcc

Overlap of [3] cbbc=bcbc with [2] bcbbc=c:

cb bc bcbbc

Critical pair: cbc=bcbcbbc.

Reduce RHS:

[2]bc(bcbbc)
⇒ bcc

Defines rule #2.

Referenced by [5], [6].

[5] bbbcc=c

Overlap of [2] bcbbc=c with [3] cbbc=bcbc:

b cbbc cbbc

Critical pair: bbcbc=c.

Reduce LHS:

[4]bb(cbc)
⇒ bbbcc

Defines rule #4.

[6] cbbc=bbcc

Simplify [3] cbbc=bcbc.

Reduce RHS:

[4]b(cbc)
⇒ bbcc

Defines rule #3.