Certificate for #2884 ⟨a, b, c | aab=a, bcb=a⟩

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

Completion settings:

[1] aab=a

Axiom: aab=a.

Referenced by [3].

[2] a=bcb

Axiom: bcb=a.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3], [4].

[3] aab=bcb

Simplify [1] aab=a.

Reduce RHS:

[2](a)
⇒ bcb

Referenced by [4].

[4] bcbbcbb=bcb

Overlap of [3] aab=bcb with [2] a=bcb:

aab a

Critical pair: bcbab=bcb.

Reduce LHS:

[2]bcb(a)b
⇒ bcbbcbb

Defines rule #2.

Referenced by [5].

[5] bcbcbb=bcbbcb

Overlap of [4] bcbbcbb=bcb with [4] bcbbcbb=bcb:

bcb bcbb bcbbcbb

Critical pair: bcbbcb=bcbcbb.

Flip LHS and RHS.

Defines rule #1.