Certificate for #4898 ⟨a, b, c | ab=a, bccbc=1⟩

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

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [7].

[2] bccbc=1

Axiom: bccbc=1.

Referenced by [3], [4].

[3] cbc=bcc

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

bcc bc bccbc

Critical pair: bcc=cbc.

Flip LHS and RHS.

Referenced by [4], [5].

[4] cbbcc=1

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

cb c cbc

Critical pair: cbbcc=bccbc.

Reduce RHS:

[2](bccbc)
⇒ 1

Referenced by [5], [6].

[5] cb=bc

Overlap of [3] cbc=bcc with [4] cbbcc=1:

cb c cbbcc

Critical pair: cb=bccbbcc.

Reduce RHS:

[4]bc(cbbcc)
⇒ bc

Defines rule #2.

Referenced by [6].

[6] bbccc=1

Overlap of [4] cbbcc=1 with [5] cb=bc:

cbbcc cb

Critical pair: bcbcc=1.

Reduce LHS:

[5]b(cb)cc
⇒ bbccc

Defines rule #4.

Referenced by [7].

[7] accc=a

Overlap of [1] ab=a with [6] bbccc=1:

a b bbccc

Critical pair: a=abccc.

Reduce RHS:

[1](ab)ccc
⇒ accc

Flip LHS and RHS.

Defines rule #3.