I have a problem with the application of the Shannon expansion for to obtain the negation of a formula boolean, than will need for implement the negation operator on OBDD (Order Binary Decision Diagram) that is, show that:
$\qquad \displaystyle \neg f(x_1,\ldots,x_n) = (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$
where $f|_{x_i=b}$ is the function boolean in which replaces $x_i$ with b, that is:
$\qquad \displaystyle f|_{x_i=b}(x_1,\ldots,x_n)=f(x_1,\ldots,x_{i-1},b,x_{i+1},\ldots,x_n)$.
The proof says:
$\qquad \displaystyle\neg f(x_1,\ldots,x_n) = \neg((\neg x_1 \wedge f|_{x_1=0}) \vee (x_1 \wedge f|_{x_1=1}))$.
Applying the negation (skip the intermediate steps), we get:
$\qquad \displaystyle (x_1 \wedge \neg x_1) \vee (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1}) \vee (\neg f|_{x_1=0} \wedge \neg f|_{x_1=1}) $.
Now $(x_1 \wedge \neg x_1)= \mathrm{false}$ can be dropped, which leads to
$\qquad \displaystyle (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1}) \vee (\neg f|_{x_1=0} \wedge \neg f|_{x_1=1}) $
which in turn is, finally, equal to
$\qquad \displaystyle (\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$.
Why does this hold?