I'm studying formal verification, and I am faced with the problem:
Let $f$, $g$ be Boolean functions. Proof or disproof that
$$\neg(f_v) = (\neg f)_v$$ $$(f ⊕ g)_v = (f_v ⊕ g_v)$$ where $f_v$ denote the positive cofactor with respect to variable $v$.
Note: The positive cofactor of $f$ with respect to variable $x_i$ is defined as
$$f_{x_i}:= f(x_1, x_2, ..., x_i=1, ...x_n)$$
I search on the Internet but can't see a proof. Can anybody tell me how to proof it?
Hint: $f = (x_i\wedge f_{x_i=1}) \vee (\bar x_i \wedge f_{x_i=0})$, where $f_{x_i=1} =f_{x_i}$ is the cofactor of $f$ w.r.t. $x_i$.
$f\vee g = (x_i\wedge [f_{x_i=1}\wedge g_{x_i=1}]) \vee (\bar x_i\wedge [f_{x_i=0}\wedge g_{x_i=0}]) $. This gives the 2nd result.
$\neg f = \neg[(x_i\wedge f_{x_i=1}) \vee (\bar x_i \wedge f_{x_i=0})] = (\bar x_i\vee\neg f_{x_i=1}) \wedge (x_i \vee f_{x_i=0}) = (x_i\wedge \bar x_i) \vee (x_i\wedge \neg f_{x_i=1}) \vee (\bar x_i\wedge\neg f_{x_i=0}) \vee (\neg f_{x_i=1}\wedge \neg f_{x_i=0}).$
But $x_i\wedge \bar x_i=0$ and $\neg f_{x_i=1}\wedge \neg f_{x_i=0} = \neg [f_{x_i=1}\vee \neg f_{x_i=0}] = \neg 1 = 0$. Thus $\neg f = (x_i\wedge \neg f_{x_i=1}) \vee (\bar x_i\wedge\neg f_{x_i=0})$ and hence $(\neg f)_{x_i=1} =\neg (f_{x_i=1})$.