\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\_\_accessors (TMJNsRBofdzqw4NpyV6GjheagG2YzZXZmv7)}
\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 : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero \in (2^{{ty\_2Ebinary\_\_ieee\_2Eflags}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfeejgghjgegfgcejhkffgchpg}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp} \in {({{2}^{{ty\_2Ebinary\_\_ieee\_2Eflags}}})}}\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfjeogghbgmgjgegpeah}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow} \in {({{2}^{{ty\_2Ebinary\_\_ieee\_2Eflags}}})}}\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfpeghfgchggmgpghh}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision} \in {({{2}^{{ty\_2Ebinary\_\_ieee\_2Eflags}}})}}\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfafchfgdgjgdhjgpgog}
\end{equation}
Let $ c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding \in (2^{{ty\_2Ebinary\_\_ieee\_2Eflags}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfcefgggpgchfgcfpgfhogegjgoghg}
\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 : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding \in (2^{{ty\_2Ebinary\_\_ieee\_2Eflags}})\end{array}
\label{hyp:ngfgngpfdgpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfbeggehfgchcfpgfhogegjgoghg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V0b))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfeejgghjgegfgcejhkffgchpg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V1b0))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfjeogghbgmgjgegpeah}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V2b1))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfpeghfgchggmgpghh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V3b2))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfafchfgdgjgdhjgpgog}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V4b3))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfcefgggpgchfgcfpgfhogegjgoghg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V5b4))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfffogegfgchggmgpghhpfpfbeggehfgchcfpgfhogegjgoghg}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfbgdgdgfgdhdhpgchdh}
$$\begin{array}{c}(({\unicdcdadad} V0b \in 2 .  ({\unicdcdadad} V1b0 \in 2 .  ({\unicdcdadad} V2b1 \in 2 .  ({\unicdcdadad} V3b2 \in \\
2 .  ({\unicdcdadad} V4b3 \in 2 .  ({\unicdcdadad} V5b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V0b)~V1b0)~V2b1)~V3b2)~V4b3)~V5b4))){\unicdbdjded}(p~V0b)))))))){\unicdcdcdhd}(({\unicdcdadad} V6b \in \\
2 .  ({\unicdcdadad} V7b0 \in 2 .  ({\unicdcdadad} V8b1 \in 2 .  ({\unicdcdadad} V9b2 \in 2 .  ({\unicdcdadad} V10b3 \in \\
2 .  ({\unicdcdadad} V11b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V6b)~V7b0)~V8b1)~V9b2)~V10b3)~V11b4))){\unicdbdjded}(p~V7b0)))))))){\unicdcdcdhd}(({\unicdcdadad} V12b \in \\
2 .  ({\unicdcdadad} V13b0 \in 2 .  ({\unicdcdadad} V14b1 \in 2 .  ({\unicdcdadad} V15b2 \in 2 .  (\\
{\unicdcdadad} V16b3 \in 2 .  ({\unicdcdadad} V17b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V12b)~V13b0)~V14b1)~V15b2)~V16b3)~V17b4))){\unicdbdjded}(p~V14b1)))))))){\unicdcdcdhd}(\\
({\unicdcdadad} V18b \in 2 .  ({\unicdcdadad} V19b0 \in 2 .  ({\unicdcdadad} V20b1 \in 2 .  ({\unicdcdadad} V21b2 \in \\
2 .  ({\unicdcdadad} V22b3 \in 2 .  ({\unicdcdadad} V23b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V18b)~V19b0)~V20b1)~V21b2)~V22b3)~V23b4))){\unicdbdjded}(p~V21b2)))))))){\unicdcdcdhd}(\\
({\unicdcdadad} V24b \in 2 .  ({\unicdcdadad} V25b0 \in 2 .  ({\unicdcdadad} V26b1 \in 2 .  ({\unicdcdadad} V27b2 \in \\
2 .  ({\unicdcdadad} V28b3 \in 2 .  ({\unicdcdadad} V29b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V24b)~V25b0)~V26b1)~V27b2)~V28b3)~V29b4))){\unicdbdjded}(p~V28b3)))))))){\unicdcdcdhd}(\\
{\unicdcdadad} V30b \in 2 .  ({\unicdcdadad} V31b0 \in 2 .  ({\unicdcdadad} V32b1 \in 2 .  ({\unicdcdadad} V33b2 \in \\
2 .  ({\unicdcdadad} V34b3 \in 2 .  ({\unicdcdadad} V35b4 \in 2 .  ((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~(ap~(ap~(ap~(ap~c\_2Ebinary\_\_ieee\_2Erecordtype\_2Eflags~\\
V30b)~V31b0)~V32b1)~V33b2)~V34b3)~V35b4))){\unicdbdjded}(p~V35b4)))))))))))))\end{array}$$
\end{theorem}
\end{document}
