Certificate for #1439 ⟨a, b, c | ab=1, aaa=cc⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

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

[2] aaa=cc

Axiom: aaa=cc.

Referenced by [3], [4].

[3] aa=ccb

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

aa a ab

Critical pair: aa=ccb.

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

[4] ccba=cc

Overlap of [2] aaa=cc with [3] aa=ccb:

aaa aa

Critical pair: ccba=cc.

Referenced by [6], [8].

[5] a=ccbb

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

a a ab

Critical pair: a=ccbb.

Defines rule #5.

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

[6] ccbbccb=cc

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

a a aa

Critical pair: accb=ccba.

Reduce LHS:

[5](a)ccb
⇒ ccbbccb

Reduce RHS:

[4](ccba)
⇒ cc

Defines rule #4.

Referenced by [9], [10].

[7] ccbbb=1

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

ab a

Critical pair: ccbbb=1.

Defines rule #1.

[8] ccbccbb=cc

Simplify [4] ccba=cc.

Reduce LHS:

[5]ccb(a)
⇒ ccbccbb

Referenced by [9], [10].

[9] ccccb=ccbcc

Overlap of [8] ccbccbb=cc with [6] ccbbccb=cc:

ccb ccbb ccbbccb

Critical pair: ccbcc=ccccb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [10].

[10] ccbccb=ccbbcc

Overlap of [6] ccbbccb=cc with [8] ccbccbb=cc:

ccbb ccb ccbccbb

Critical pair: ccbbcc=ccccbb.

Reduce RHS:

[9](ccccb)b
⇒ ccbccb

Flip LHS and RHS.

Defines rule #3.