Theorem cadan
The adder carry in conjunctive normal form. (Contributed by Mario
Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 25-Sep-2018.)
Conclusion
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
Proof
l0
df-3or
\( \vdash \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \)
l1
cador
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \)
andi
orbi1i _
\( \vdash \varphi \wedge (\psi \vee \chi) \vee \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \vee \varphi \wedge \chi \vee \psi \wedge \chi \)
l4
3bitr4i l0 l1 _
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge (\psi \vee \chi) \vee \psi \wedge \chi \)
l5
ordir
\( \vdash \varphi \wedge (\psi \vee \chi) \vee \psi \wedge \chi \leftrightarrow (\varphi \vee \psi \wedge \chi) \wedge (\psi \vee \chi \vee \psi \wedge \chi) \)
l6
ordi
l7
orcom
\( \vdash \psi \vee \chi \vee \psi \wedge \chi \leftrightarrow \psi \wedge \chi \vee (\psi \vee \chi) \)
l8
animorl
\( \vdash \psi \wedge \chi \rightarrow \psi \vee \chi \)
pm4.72
\( \vdash \psi \wedge \chi \rightarrow \psi \vee \chi \leftrightarrow (\psi \vee \chi \leftrightarrow \psi \wedge \chi \vee (\psi \vee \chi)) \)
mpbi l8 _
\( \vdash \psi \vee \chi \leftrightarrow \psi \wedge \chi \vee (\psi \vee \chi) \)
bitr4i l7 _
anbi12i l6 _
\( \vdash (\varphi \vee \psi \wedge \chi) \wedge (\psi \vee \chi \vee \psi \wedge \chi) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
l13
3bitri l4 l5 _
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
df-3an
\( \vdash (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
bitr4i l13 _