Theorem cadnot
The adder carry distributes over negation. (Contributed by Mario
Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)
Conclusion
\( \vdash \neg \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ cadd } ( \neg \varphi , \neg \psi , \neg \chi ) \)
Proof
l0
ianor
l1
ianor
ianor
l3
3anbi123i l0 l1 _
\( \vdash \neg (\varphi \wedge \psi) \wedge \neg (\varphi \wedge \chi) \wedge \neg (\psi \wedge \chi) \leftrightarrow (\neg \varphi \vee \neg \psi) \wedge (\neg \varphi \vee \neg \chi) \wedge (\neg \psi \vee \neg \chi) \)
l4
3ioran
\( \vdash \neg (\varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi) \leftrightarrow \neg (\varphi \wedge \psi) \wedge \neg (\varphi \wedge \chi) \wedge \neg (\psi \wedge \chi) \)
cador
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \)
l6
xchnxbir l4 _
\( \vdash \neg \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \neg (\varphi \wedge \psi) \wedge \neg (\varphi \wedge \chi) \wedge \neg (\psi \wedge \chi) \)
cadan
\( \vdash \text{ cadd } ( \neg \varphi , \neg \psi , \neg \chi ) \leftrightarrow (\neg \varphi \vee \neg \psi) \wedge (\neg \varphi \vee \neg \chi) \wedge (\neg \psi \vee \neg \chi) \)
3bitr4i l3 l6 _