bit-manipulation - ブール式の証明

Question

>>> import z3  
>>> X = z3.BitVec('X', 32)  
>>> z3.prove( X^18 == ((X|(~44)) & (X^62)) + (X&44) )  
proved  

x^18は((x|(~44))&(x^62))+(x&44) ?? と同等です。

これはどのように可能でしょうか？
この公式の証明について詳しく知りたいのですが...