I'm trying to prove/derive the equivalence of the following formula:
$$
x*y = (x \land y) * (x \lor y) + (x \land \neg y) * (\neg x \land y)
$$
whereas $(\land, \lor, \neg)$ correspond to bitwise operations over Boolean algebra ($B^n, \land , \lor, \neg)$ and arithmetic operations are in integer modular ring $Z/(2^n)$.
Rearranging by using DeMorgan rules gives me:
$x * (x \lor y) \land y * (x \lor y)$. However, I cannot simply factor out $(x \lor y)$ so I'm stuck at that point. The issue seems to be, that this whole thing is a non-linear expression.
I came across this identity in this paper and was wondering how one could derive/generate such identities.
Similar identities can be found in Hackers Delight chapter 2 (and are much simpler, i.e., linear combinations of the 16 boolean functions).
Is it because the last term always equals to zero? How would one prove that? The last term isn't always zero (e.g. $1*524288$).
Example in $Z/2^{32}$
$$
4 * 5 = (4 \land 5) * (4 \lor 5) + (4 \land \lnot 5) * (\lnot 4 \land 5)
\equiv (4) * (5) + (4 \land 4294967290) * (4294967291 \land 5)
\equiv (4) * (5) + (0) * (0)
\equiv 20
$$
Update:
Let's split the formula into the two parts for easier reference:
$$
t0 = (x \land y) * (x \lor y) \\
t1 = (x \land \neg y) * (\neg x \land y)
$$
I've used an SMT solver (z3) to prove that for all values of $x,y$ either $t0$ or $t1$ can be $\neq 0$, but not both at the same time.
Counter example: $x = 1431655427, y = 427$
Best Answer
Note we have $x \land \neg y = x - x \land y$. Using this fact
$$(x \land y) (x \lor y) + (x \land \neg y) (\neg x \land y) = x y$$
becomes
$$(x \land y) (x \lor y) + (x - x \land y) (y - x \land y) = x y$$
expanding,
$$(x \land y) (x \lor y) + x y - (x + y) (x \land y) + (x \land y)^2 = x y$$
$$(x \land y) (x \lor y) - (x + y) (x \land y) + (x \land y)^2 = 0$$
Divide by $x \land y$:
$$(x \lor y) - (x + y) + (x \land y) = 0$$
$$(x \lor y) + (x \land y) = x + y$$
To prove this equality, write down $x$ and $y$ in binary: $x = \sum_{i=0}^{n-1} x_i 2^i$ and $y = \sum_{i=0}^{n-1} y_i 2^i$, where $x_i, y_i \in \{0,1\}$. Note that $x \land y = \sum_{i=0}^{n-1} \min (x_i, y_i) 2^i$ and $x \lor y = \sum_{i=0}^{n-1} \max (x_i, y_i) 2^i$. We want to show
$$\sum_{i=0}^{n-1} 2^i \max (x_i, y_i) + \sum_{i=0}^{n-1} 2^i \min (x_i, y_i) = \sum_{i=0}^{n-1} 2^i x_i + \sum_{i=0}^{n-1} 2^i y_i$$
which is the same as
$$\sum_{i=0}^{n-1} 2^i (\max (x_i, y_i) + \min (x_i, y_i)) = \sum_{i=0}^{n-1} 2^i (x_i + y_i)$$
but for any numbers $x_i, y_i$ we have $\max (x_i, y_i) + \min(x_i, y_i) = x_i + y_i$.