Theorem cadbi123d
Equality theorem for the adder carry. (Contributed by Mario Carneiro,
4-Sep-2016.)
Hypotheses
cadbid.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
cadbid.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
cadbid.3
\( \vdash \varphi \rightarrow (\eta \leftrightarrow \zeta) \)
Conclusion
\( \vdash \varphi \rightarrow (\text{ cadd } ( \psi , \theta , \eta ) \leftrightarrow \text{ cadd } ( \chi , \tau , \zeta )) \)
Proof
l0
cadbid.1
cadbid.2
l2
anbi12d l0 _
l3
cadbid.3
l4
cadbid.1
cadbid.2
xorbi12d l4 _
anbi12d l3 _
l8
orbi12d l2 _
\( \vdash \varphi \rightarrow (\psi \wedge \theta \vee \eta \wedge (\psi \veebar \theta) \leftrightarrow \chi \wedge \tau \vee \zeta \wedge (\chi \veebar \tau)) \)
l9
df-cad
\( \vdash \text{ cadd } ( \psi , \theta , \eta ) \leftrightarrow \psi \wedge \theta \vee \eta \wedge (\psi \veebar \theta) \)
df-cad
\( \vdash \text{ cadd } ( \chi , \tau , \zeta ) \leftrightarrow \chi \wedge \tau \vee \zeta \wedge (\chi \veebar \tau) \)
3bitr4g l8 l9 _