Theorem hadnot
The adder sum distributes over negation. (Contributed by Mario Carneiro,
4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)
Conclusion
\( \vdash \neg \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \neg \varphi , \neg \psi , \neg \chi ) \)
Proof
notbi
l1
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg \chi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi \leftrightarrow \neg \chi) \)
l2
xor3
\( \vdash \neg (\varphi \leftrightarrow \psi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \neg \chi) \)
hadbi
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \chi) \)
l4
xchnxbir l2 _
\( \vdash \neg \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \leftrightarrow \psi \leftrightarrow \neg \chi) \)
hadbi
\( \vdash \text{ hadd } ( \neg \varphi , \neg \psi , \neg \chi ) \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi \leftrightarrow \neg \chi) \)
3bitr4i l1 l4 _