Theorem cador
The adder carry in disjunctive normal form. (Contributed by Mario
Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)
Conclusion
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \)
Proof
xor2
rbaib _
l2
anbi1d _
\( \vdash \neg (\varphi \wedge \psi) \rightarrow ((\varphi \veebar \psi) \wedge \chi \leftrightarrow (\varphi \vee \psi) \wedge \chi) \)
l3
ancom
\( \vdash (\varphi \veebar \psi) \wedge \chi \leftrightarrow \chi \wedge (\varphi \veebar \psi) \)
andir
\( \vdash (\varphi \vee \psi) \wedge \chi \leftrightarrow \varphi \wedge \chi \vee \psi \wedge \chi \)
3bitr3g l2 l3 _
l6
pm5.74i _
\( \vdash \neg (\varphi \wedge \psi) \rightarrow \chi \wedge (\varphi \veebar \psi) \leftrightarrow \neg (\varphi \wedge \psi) \rightarrow \varphi \wedge \chi \vee \psi \wedge \chi \)
l7
df-or
\( \vdash \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \leftrightarrow \neg (\varphi \wedge \psi) \rightarrow \chi \wedge (\varphi \veebar \psi) \)
df-or
\( \vdash \varphi \wedge \psi \vee (\varphi \wedge \chi \vee \psi \wedge \chi) \leftrightarrow \neg (\varphi \wedge \psi) \rightarrow \varphi \wedge \chi \vee \psi \wedge \chi \)
l9
3bitr4i l6 l7 _
\( \vdash \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \leftrightarrow \varphi \wedge \psi \vee (\varphi \wedge \chi \vee \psi \wedge \chi) \)
l10
df-cad
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \chi \wedge (\varphi \veebar \psi) \)
3orass
\( \vdash \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \vee (\varphi \wedge \chi \vee \psi \wedge \chi) \)
3bitr4i l9 l10 _