Theorem cadcomb
Commutative law for the adder carry. (Contributed by Mario Carneiro,
4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)
Conclusion
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow \text{ cadd } ( \varphi , \chi , \psi ) \)
Proof
l0
cadan
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \)
l1
3ancoma
\( \vdash (\varphi \vee \psi) \wedge (\varphi \vee \chi) \wedge (\psi \vee \chi) \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \psi) \wedge (\psi \vee \chi) \)
orcom
3anbi3i _
\( \vdash (\varphi \vee \chi) \wedge (\varphi \vee \psi) \wedge (\psi \vee \chi) \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \psi) \wedge (\chi \vee \psi) \)
l4
3bitri l0 l1 _
\( \vdash \text{ cadd } ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \psi) \wedge (\chi \vee \psi) \)
cadan
\( \vdash \text{ cadd } ( \varphi , \chi , \psi ) \leftrightarrow (\varphi \vee \chi) \wedge (\varphi \vee \psi) \wedge (\chi \vee \psi) \)
bitr4i l4 _