Operations on OBDD: negation through Shannon's expansion

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?

Maybe it is better to understand if you make a truth table for both functions. You can see that if $(\neg f|_{x_1=0} \wedge \neg f|_{x_1=1})$ is true then $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ is also true, because both $f$ terms are true and either $x_1$ is true or $\neg x_1$ is true. And if $(\neg f|_{x_1=0} \wedge \neg f|_{x_1=1})$ is false then you have to do a case study:

• If both $f$ terms are false then is $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ also false

• If exactly one $f$ term (w.l.o.g. $\neg f|_{x_1=0}$) is false then it is equivalent to $(x_1 \wedge \neg f|_{x_1=1})$

Therefore, both formulas $(\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})$ and $(\neg x_1 \wedge \neg f|_{x_1=0}) \vee (x_1 \wedge \neg f|_{x_1=1})$ are equivalent.

StackExchange Computer Science Q#2595, answer score: 4