Theorem had0
If the first input is false, then the adder sum is equivalent to the
exclusive disjunction of the other two inputs, and conversely.
(Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf
Lammen, 12-Jul-2020.) Strengthen to a biconditional. (Revised by BJ,
10-Aug-2026.)
Conclusion
\( \vdash \neg \varphi \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \psi \veebar \chi) \)
Proof
l0
hadrot
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ hadd } ( \psi , \chi , \varphi ) \)
l1
df-had
\( \vdash \text{ hadd } ( \psi , \chi , \varphi ) \leftrightarrow (\psi \veebar \chi) \veebar \varphi \)
l2
df-xor
\( \vdash (\psi \veebar \chi) \veebar \varphi \leftrightarrow \neg (\psi \veebar \chi \leftrightarrow \varphi) \)
xor3
\( \vdash \neg (\psi \veebar \chi \leftrightarrow \varphi) \leftrightarrow (\psi \veebar \chi \leftrightarrow \neg \varphi) \)
bitri l2 _
\( \vdash (\psi \veebar \chi) \veebar \varphi \leftrightarrow (\psi \veebar \chi \leftrightarrow \neg \varphi) \)
bitri l1 _
\( \vdash \text{ hadd } ( \psi , \chi , \varphi ) \leftrightarrow (\psi \veebar \chi \leftrightarrow \neg \varphi) \)
l6
bitri l0 _
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \veebar \chi \leftrightarrow \neg \varphi) \)
biass
\( \vdash \text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow \psi \veebar \chi \leftrightarrow \neg \varphi \leftrightarrow (\text{ hadd } ( \varphi , \psi , \chi ) \leftrightarrow (\psi \veebar \chi \leftrightarrow \neg \varphi)) \)
mpbir l6 _
bicomi _