Certificate for #1891 ⟨a, b, c | aba=cc, acb=1⟩

Back:⟨a, b, c | aba=cc, acb=1⟩

Completion settings:

[1] aba=cc

Axiom: aba=cc.

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

[2] acb=1

Axiom: acb=1.

Defines rule #4.

Referenced by [4].

[3] ccba=abcc

Overlap of [1] aba=cc with [1] aba=cc:

ab a aba

Critical pair: abcc=ccba.

Flip LHS and RHS.

Referenced by [5], [6].

[4] ab=cccb

Overlap of [1] aba=cc with [2] acb=1:

ab a acb

Critical pair: ab=cccb.

Defines rule #3.

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

[5] ccccbcc=cc

Overlap of [1] aba=cc with [4] ab=cccb:

aba ab

Critical pair: cccba=cc.

Reduce LHS:

[3]c(ccba)
[4]⇒ c(ab)cc
⇒ ccccbcc

Defines rule #1.

[6] ccba=cccbcc

Simplify [3] ccba=abcc.

Reduce RHS:

[4](ab)cc
⇒ cccbcc

Defines rule #5.

Referenced by [7].

[7] ccbcccb=cccbccb

Overlap of [6] ccba=cccbcc with [4] ab=cccb:

ccb a ab

Critical pair: ccbcccb=cccbccb.

Defines rule #2.