Certificate for #5659 ⟨a, b, c | aa=a, bcb=bc⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

[2] bcb=bc

Axiom: bcb=bc.

Referenced by [4].

[3] bc=d

Axiom: bc=d.

Defines rule #4.

Referenced by [4], [5], [6].

[4] bcb=d

Simplify [2] bcb=bc.

Reduce RHS:

[3](bc)
⇒ d

Referenced by [5].

[5] db=d

Overlap of [4] bcb=d with [3] bc=d:

bcb bc

Critical pair: db=d.

Defines rule #3.

Referenced by [6].

[6] dc=dd

Overlap of [5] db=d with [3] bc=d:

d b bc

Critical pair: dd=dc.

Flip LHS and RHS.

Defines rule #2.