Proving boolean expression

Question

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

x^18 is equivalent to ((x|(~44))&(x^62))+(x&44) ??

How could this be possible?
I want to know detailed information about proving this formula...

Answer 1

You could display the (intermediate) bit vectors as symbolic sets of 8 bits each:

| X                       |   x7 |   x6 |   x5 |   x4 |   x3 |   x2 |   x1 |   x0  |
| 44                      |    0 |    0 |    1 |    0 |    1 |    1 |    0 |    0  |
| ~44                     |    1 |    1 |    0 |    1 |    0 |    0 |    1 |    1  |
| X|(~44)                 |    1 |    1 |   x5 |    1 |   x3 |   x2 |    1 |    1  |
| 62                      |    0 |    0 |    1 |    1 |    1 |    1 |    1 |    0  |
| X^62                    |   x7 |   x6 |  !x5 |  !x4 |  !x3 |  !x2 |  !x1 |   x0  |
| (X|(~44))&(X^62)        |   x7 |   x6 |    0 |  !x4 |    0 |    0 |  !x1 |   x0  |
| X&44                    |    0 |    0 |   x5 |    0 |   x3 |   x2 |    0 |    0  |
| (X|(~44))&(X^62)+(X&44) |   x7 |   x6 |   x5 |  !x4 |   x3 |   x2 |  !x1 |   x0  |
| X^18                    |   x7 |   x6 |   x5 |  !x4 |   x3 |   x2 |  !x1 |   x0  |

Six bits would suffice, as 62 can be expressed with six bits.

The addition step cannot produce carry bits, as all corresponding bit pairs have one zero bit each. The other operations only have a bitwise effect. Therefore, one could analyze the equivalence bit position by bit position.

The final two table rows show that the expressions are in fact equivalent.