Certificate for #5748 ⟨a, b, c | aa=b, bcb=cc⟩

Back:⟨a, b, c | aa=b, bcb=cc⟩

Completion settings:

[1] b=aa

Axiom: aa=b.

Flip LHS and RHS.

Defines rule #4.

Referenced by [2].

[2] aacaa=cc

Axiom: bcb=cc.

Reduce LHS:

[1](b)cb
[1]⇒ aac(b)
⇒ aacaa

Defines rule #1.

Referenced by [3], [4].

[3] cccaa=aaccc

Overlap of [2] aacaa=cc with [2] aacaa=cc:

aac aa aacaa

Critical pair: aaccc=cccaa.

Flip LHS and RHS.

Defines rule #2.

[4] ccacaa=aacacc

Overlap of [2] aacaa=cc with [2] aacaa=cc:

aaca a aacaa

Critical pair: aacacc=ccacaa.

Flip LHS and RHS.

Defines rule #3.