Certificate for #1086 ⟨a, b, c | aa=1, abccb=1⟩

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

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

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

[2] abccb=1

Axiom: abccb=1.

Referenced by [3], [9].

[3] bccb=a

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

a a abccb

Critical pair: a=bccb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [4], [7].

[4] bcca=accb

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

bcc b bccb

Critical pair: bcca=accb.

Defines rule #4.

Referenced by [5].

[5] accba=bcc

Overlap of [4] bcca=accb with [1] aa=1:

bcc a aa

Critical pair: bcc=accba.

Flip LHS and RHS.

Referenced by [6].

[6] ccba=abcc

Overlap of [1] aa=1 with [5] accba=bcc:

a a accba

Critical pair: abcc=ccba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [8].

[7] babcc=1

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

b ccb ccba

Critical pair: babcc=aa.

Reduce RHS:

[1](aa)
⇒ 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.