Доказывая логическое выражение

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) ??

Как это могло быть возможно?
Я хочу знать подробную информацию о доказательстве этой формулы ...

Answer 1

Вы можете отобразить (промежуточные) битовые векторы в виде наборов символов по 8 бит каждый:

| 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  |

Шести битов будет достаточно, поскольку 62 можно выразить шестью битами.

Этап сложения не может создать биты переноса, поскольку каждая соответствующая пара битов имеет по одному нулевому биту каждая.Другие операции имеют только побитовый эффект.Следовательно, можно анализировать позицию бита эквивалентности по позиции бита.

Последние две строки таблицы показывают, что выражения на самом деле эквивалентны.