Certificate for #7860 ⟨a, b, c | ab=1, ccc=aaa⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

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

[2] aaa=ccc

Axiom: ccc=aaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] aa=cccb

Overlap of [2] aaa=ccc with [1] ab=1:

aa a ab

Critical pair: aa=cccb.

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

[4] cccba=ccc

Overlap of [2] aaa=ccc with [3] aa=cccb:

aaa aa

Critical pair: cccba=ccc.

Referenced by [6], [8].

[5] a=cccbb

Overlap of [3] aa=cccb with [1] ab=1:

a a ab

Critical pair: a=cccbb.

Defines rule #5.

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

[6] cccbbcccb=ccc

Overlap of [3] aa=cccb with [3] aa=cccb:

a a aa

Critical pair: acccb=cccba.

Reduce LHS:

[5](a)cccb
⇒ cccbbcccb

Reduce RHS:

[4](cccba)
⇒ ccc

Defines rule #4.

Referenced by [9], [10].

[7] cccbbb=1

Overlap of [1] ab=1 with [5] a=cccbb:

ab a

Critical pair: cccbbb=1.

Defines rule #1.

[8] cccbcccbb=ccc

Simplify [4] cccba=ccc.

Reduce LHS:

[5]cccb(a)
⇒ cccbcccbb

Referenced by [9], [10].

[9] ccccccb=cccbccc

Overlap of [8] cccbcccbb=ccc with [6] cccbbcccb=ccc:

cccb cccbb cccbbcccb

Critical pair: cccbccc=ccccccb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [10].

[10] cccbcccb=cccbbccc

Overlap of [6] cccbbcccb=ccc with [8] cccbcccbb=ccc:

cccbb cccb cccbcccbb

Critical pair: cccbbccc=ccccccbb.

Reduce RHS:

[9](ccccccb)b
⇒ cccbcccb

Flip LHS and RHS.

Defines rule #3.