Certificate for #6590 ⟨a, b, c | ab=1, cacbcc=1⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

[2] cacbcc=1

Axiom: cacbcc=1.

Referenced by [3], [4].

[3] cacbc=acbcc

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

cacbc c cacbcc

Critical pair: cacbc=acbcc.

Referenced by [4], [5].

[4] acbccc=1

Overlap of [2] cacbcc=1 with [3] cacbc=acbcc:

cacbcc cacbc

Critical pair: acbccc=1.

Defines rule #3.

Referenced by [5], [6].

[5] cacbacbcc=acb

Overlap of [3] cacbc=acbcc with [3] cacbc=acbcc:

cacb c cacbc

Critical pair: cacbacbcc=acbccacbc.

Reduce RHS:

[3]acbc(cacbc)
[3]⇒ acb(cacbc)c
[4]⇒ acb(acbccc)
⇒ acb

Referenced by [6].

[6] cacb=acbc

Overlap of [5] cacbacbcc=acb with [4] acbccc=1:

cacb acbcc acbccc

Critical pair: cacb=acbc.

Defines rule #2.