Certificate for #3595 ⟨a, b, c | ba=ac, cb=ac⟩

Back:⟨a, b, c | ba=ac, cb=ac⟩

Completion settings:

[1] ba=ac

Axiom: ba=ac.

Referenced by [4].

[2] cb=ac

Axiom: cb=ac.

Referenced by [5].

[3] ac=d

Axiom: ac=d.

Defines rule #1.

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

[4] ba=d

Simplify [1] ba=ac.

Reduce RHS:

[3](ac)
⇒ d

Defines rule #2.

Referenced by [6], [7].

[5] cb=d

Simplify [2] cb=ac.

Reduce RHS:

[3](ac)
⇒ d

Defines rule #3.

Referenced by [7], [8].

[6] dc=bd

Overlap of [4] ba=d with [3] ac=d:

b a ac

Critical pair: bd=dc.

Flip LHS and RHS.

Defines rule #6.

[7] da=cd

Overlap of [5] cb=d with [4] ba=d:

c b ba

Critical pair: cd=da.

Flip LHS and RHS.

Defines rule #4.

[8] db=ad

Overlap of [3] ac=d with [5] cb=d:

a c cb

Critical pair: ad=db.

Flip LHS and RHS.

Defines rule #5.