Certificate for #7855 ⟨a, b, c | ab=1, cbc=bcc⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #3.

Referenced by [6].

[2] bcc=cbc

Axiom: cbc=bcc.

Flip LHS and RHS.

Referenced by [4].

[3] cbc=d

Axiom: cbc=d.

Defines rule #5.

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

[4] bcc=d

Simplify [2] bcc=cbc.

Reduce RHS:

[3](cbc)
⇒ d

Defines rule #8.

Referenced by [6], [7], [8].

[5] cbd=dbc

Overlap of [3] cbc=d with [3] cbc=d:

cb c cbc

Critical pair: cbd=dbc.

Defines rule #4.

[6] ad=cc

Overlap of [1] ab=1 with [4] bcc=d:

a b bcc

Critical pair: ad=cc.

Defines rule #2.

[7] bcd=dbc

Overlap of [4] bcc=d with [3] cbc=d:

bc c cbc

Critical pair: bcd=dbc.

Referenced by [9].

[8] cd=dc

Overlap of [3] cbc=d with [4] bcc=d:

c bc bcc

Critical pair: cd=dc.

Defines rule #1.

Referenced by [9].

[9] bdc=dbc

Simplify [7] bcd=dbc.

Reduce LHS:

[8]b(cd)
⇒ bdc

Defines rule #7.

Referenced by [10].

[10] bdd=dbd

Overlap of [9] bdc=dbc with [3] cbc=d:

bd c cbc

Critical pair: bdd=dbcbc.

Reduce RHS:

[3]db(cbc)
⇒ dbd

Defines rule #6.