\documentclass{article}
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{conjecture}{Conjecture}
\newcommand\unicdcdgdad{\not=}
\newcommand\unicdcdcdbg{\cup}
\newcommand\unicdcdbdgd{\setminus}
\newcommand\unicdcdcdjd{\cap}
\newcommand\unicdcdadad{\forall}
\newcommand\unicdbdjdcd{\Rightarrow}
\newcommand\unicdcdadjd{\notin}
\newcommand\unicdbdjded{\Leftrightarrow}
\newcommand\unicdcdcdid{\lor}
\newcommand\unicdcdcdhd{\land}
\newcommand\uniddcgcg{\lambda}
\newcommand\unicdcdaddd{\exists}
\newcommand\unicdcdidid{\not\subseteq}
\newcommand\preoh[1]{\lnot #1}
\newcommand\mname[1]{{\mathsf{#1}}}
\begin{document}
\title{thm\_2Ebinary\_\_ieee\_2Eflags\_\_fn\_\_updates (TMWko6qzwcrcyiG1MFUwGTnYKfwL74MTy2Z)}
\maketitle
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfddeepfddeepfddfe}
We define $\mname{c\_2Emin\_2E\_3D\_3D\_3E}$ to be ${{\uniddcgcg} P \in {2} .  {{\uniddcgcg} Q \in {2} .  {{inj\_\_o}~{({{{p}~{P}}{\unicdbdjdcd}{{p}~{Q}}})}}}}$ of type ${\iota}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfddee}
We define $\mname{c\_2Emin\_2E\_3D}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} x \in {A} .  {{\uniddcgcg} y \in {A} .  {{inj\_\_o}~{({{x}={y}})}}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfeef}
We define $\mname{c\_2Ebool\_2ET}$ to be ${({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{2}}})}})}}~{({{\uniddcgcg} V0x \in {2} .  {V0x}})}})}}~{({{\uniddcgcg} V1x \in {2} .  {V1x}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdbd}
We define $\mname{c\_2Ebool\_2E\_21}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{A\_27a}}})}})}}~{V0P}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {\mname{c\_2Ebool\_2ET}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdgepffdde}
We define $\mname{c\_2Ebool\_2E\_2F\_5C}$ to be ${({{\uniddcgcg} V0t1 \in {2} .  {({{\uniddcgcg} V1t2 \in {2} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V2t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t1}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V1t2}})}}~{V2t}})}})}})}}~{V2t}})}})}})}})}})}$.
\end{definition}
Let $ ty\_2Ebinary\_\_ieee\_2Eflags : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Ebinary\_\_ieee\_2Eflags}}\label{hyp:ogfgpfehjhpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdh}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd \in ((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfeejgghjgegfgcejhkffgchpgpfpfggfhaheg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd \in ((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfjeogghbgmgjgegpeahpfpfggfhaheg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd \in ((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfpeghfgchggmgpghhpfpfggfhaheg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd \in ((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfafchfgdgjgdhjgpgogpfpfggfhaheg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd \in \\
((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfcefgggpgchfgcfpgfhogegjgoghgpfpfggfhaheg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags \in ((((((ty\_2Ebinary\_\_ieee\_2Eflags^{{2}})^{{2}})^{{2}})^{{2}})^{{2}})^{{2}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfechfgdgpgchegehjhahfgpfcdfeggmgbghgdh}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd \in \\
((ty\_2Ebinary\_\_ieee\_2Eflags^{{ty\_2Ebinary\_\_ieee\_2Eflags}})^{{({{2}^{{2}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfbeggehfgchcfpgfhogegjgoghgpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~V0f)~(ap~(\\
ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V1b)~\\
V2b0)~V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
(ap~V0f~V1b))~V2b0)~V3b1)~V4b2)~V5b3)~V6b4)))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfeejgghjgegfgcejhkffgchpgpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~V0f)~(ap~(ap~(\\
ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V1b)~V2b0)~\\
V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~(ap~V0f~V2b0))~V3b1)~V4b2)~V5b3)~V6b4)))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfjeogghbgmgjgegpeahpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~V0f)~(ap~(ap~(ap~\\
(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V1b)~V2b0)~\\
V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~(ap~V0f~V3b1))~V4b2)~V5b3)~V6b4)))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfpeghfgchggmgpghhpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~V0f)~(ap~(ap~(\\
ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V1b)~V2b0)~\\
V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~V3b1)~(ap~V0f~V4b2))~V5b3)~V6b4)))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfafchfgdgjgdhjgpgogpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V0f)~(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~V3b1)~V4b2)~(ap~V0f~V5b3))~V6b4)))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfcefgggpgchfgcfpgfhogegjgoghgpfpfggfhaheg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V0f)~(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V1b)~V2b0)~V3b1)~V4b2)~V5b3)~(ap~V0f~V6b4))))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfbeggehfgchcfpgfhogegjgoghgpfpfggfhaheg}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfggogpfpffhahegbgehfgdh}
$$\begin{array}{c}(({\unicdcdadad} V0f \in (2^{{2}}) .  ({\unicdcdadad} V1b \in 2 .  ({\unicdcdadad} V2b0 \in 2 .  ({\unicdcdadad} V3b1 \in \\
2 .  ({\unicdcdadad} V4b2 \in 2 .  ({\unicdcdadad} V5b3 \in 2 .  ({\unicdcdadad} V6b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~V0f)~(ap~(\\
ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V1b)~\\
V2b0)~V3b1)~V4b2)~V5b3)~V6b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
(ap~V0f~V1b))~V2b0)~V3b1)~V4b2)~V5b3)~V6b4))))))))){\unicdcdcdhd}(({\unicdcdadad} V7f \in \\
(2^{{2}}) .  ({\unicdcdadad} V8b \in 2 .  ({\unicdcdadad} V9b0 \in 2 .  ({\unicdcdadad} V10b1 \in 2 .  (\\
{\unicdcdadad} V11b2 \in 2 .  ({\unicdcdadad} V12b3 \in 2 .  ({\unicdcdadad} V13b4 \in 2 .  ((ap~(\\
ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~V7f)~(ap~(ap~(ap~\\
(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V8b)~V9b0)~\\
V10b1)~V11b2)~V12b3)~V13b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V8b)~(ap~V7f~V9b0))~V10b1)~V11b2)~V12b3)~V13b4))))))))){\unicdcdcdhd}(({\unicdcdadad} V14f \in \\
(2^{{2}}) .  ({\unicdcdadad} V15b \in 2 .  ({\unicdcdadad} V16b0 \in 2 .  ({\unicdcdadad} V17b1 \in 2 .  \\
({\unicdcdadad} V18b2 \in 2 .  ({\unicdcdadad} V19b3 \in 2 .  ({\unicdcdadad} V20b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~V14f)~(ap~(ap~(\\
ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V15b)~V16b0)~\\
V17b1)~V18b2)~V19b3)~V20b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V15b)~V16b0)~(ap~V14f~V17b1))~V18b2)~V19b3)~V20b4))))))))){\unicdcdcdhd}(({\unicdcdadad} V21f \in \\
(2^{{2}}) .  ({\unicdcdadad} V22b \in 2 .  ({\unicdcdadad} V23b0 \in 2 .  ({\unicdcdadad} V24b1 \in 2 .  \\
({\unicdcdadad} V25b2 \in 2 .  ({\unicdcdadad} V26b3 \in 2 .  ({\unicdcdadad} V27b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~V21f)~(ap~(ap~\\
(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V22b)~V23b0)~\\
V24b1)~V25b2)~V26b3)~V27b4))=(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V22b)~V23b0)~V24b1)~(ap~V21f~V25b2))~V26b3)~V27b4))))))))){\unicdcdcdhd}(({\unicdcdadad} V28f \in \\
(2^{{2}}) .  ({\unicdcdadad} V29b \in 2 .  ({\unicdcdadad} V30b0 \in 2 .  ({\unicdcdadad} V31b1 \in 2 .  \\
({\unicdcdadad} V32b2 \in 2 .  ({\unicdcdadad} V33b3 \in 2 .  ({\unicdcdadad} V34b4 \in 2 .  ((ap~\\
(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V28f)~(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V29b)~V30b0)~V31b1)~V32b2)~V33b3)~V34b4))=(ap~(ap~(ap~(ap~(ap~(ap~\\
c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V29b)~V30b0)~V31b1)~V32b2)~\\
(ap~V28f~V33b3))~V34b4))))))))){\unicdcdcdhd}({\unicdcdadad} V35f \in (2^{{2}}) .  ({\unicdcdadad} V36b \in \\
2 .  ({\unicdcdadad} V37b0 \in 2 .  ({\unicdcdadad} V38b1 \in 2 .  ({\unicdcdadad} V39b2 \in 2 .  (\\
{\unicdcdadad} V40b3 \in 2 .  ({\unicdcdadad} V41b4 \in 2 .  ((ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V35f)~(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V36b)~V37b0)~V38b1)~V39b2)~V40b3)~V41b4))=(ap~(ap~(ap~(ap~(ap~(ap~\\
c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~V36b)~V37b0)~V38b1)~V39b2)~\\
V40b3)~(ap~V35f~V41b4)))))))))))))))\end{array}$$
\end{theorem}
\end{document}
