Certificate for #3002 ⟨a, b, c | aab=c, cbc=a⟩

Back:⟨a, b, c | aab=c, cbc=a⟩

Completion settings:

[1] aab=c

Axiom: aab=c.

Referenced by [3].

[2] a=cbc

Axiom: cbc=a.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[3] cbccbcb=c

Overlap of [1] aab=c with [2] a=cbc:

aab a

Critical pair: cbcab=c.

Reduce LHS:

[2]cbc(a)b
⇒ cbccbcb

Defines rule #2.

Referenced by [4].

[4] cccbcb=cbccbc

Overlap of [3] cbccbcb=c with [3] cbccbcb=c:

cbccb cb cbccbcb

Critical pair: cbccbc=cccbcb.

Flip LHS and RHS.

Defines rule #1.