Certificate for #3624 ⟨a, b, c | aaa=1, abccb=1⟩

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

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

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

[2] abccb=1

Axiom: abccb=1.

Referenced by [3], [9].

[3] bccb=aa

Overlap of [1] aaa=1 with [2] abccb=1:

aa a abccb

Critical pair: aa=bccb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [7].

[4] bccaa=aaccb

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

bcc b bccb

Critical pair: bccaa=aaccb.

Defines rule #5.

Referenced by [5].

[5] aaccba=bcc

Overlap of [4] bccaa=aaccb with [1] aaa=1:

bcc aa aaa

Critical pair: bcc=aaccba.

Flip LHS and RHS.

Referenced by [6].

[6] ccba=abcc

Overlap of [1] aaa=1 with [5] aaccba=bcc:

a aa aaccba

Critical pair: abcc=ccba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [8].

[7] babcc=1

Overlap of [3] bccb=aa with [6] ccba=abcc:

b ccb ccba

Critical pair: babcc=aaa.

Reduce RHS:

[1](aaa)
⇒ 1

Referenced by [8].

[8] babcabcc=cba

Overlap of [7] babcc=1 with [6] ccba=abcc:

babc c ccba

Critical pair: babcabcc=cba.

Referenced by [9].

[9] babc=cbab

Overlap of [8] babcabcc=cba with [2] abccb=1:

babc abcc abccb

Critical pair: babc=cbab.

Defines rule #3.