\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\_\_literal\_\_11 (TMPVCmx1APoCxpJAK3AUCmEigFQyMNn9kTL)}
\maketitle
Let $ c\_2Ebool\_2EARB : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A\_27a .  {{{nonempty}~{A\_27a}}{\unicdbdjdcd}{{{c\_2Ebool\_2EARB}~{A\_27a}} \in {A\_27a}}}}\label{hyp:ngfgngpfdgpfcdfecgpgpgmgpfcdfebecfce}
\end{equation}
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\_\_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}
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\_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\_\_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\_\_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\_\_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}
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\_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\_\_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\_\_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\_\_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}
\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}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfele}
We define $\mname{c\_2Ecombin\_2EK}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {({{\uniddcgcg} V0x \in {A\_27a} .  {({{\uniddcgcg} V1y \in {A\_27b} .  {V0x}})}})}}}$.
\end{definition}
Assume the following.
\begin{equation}
\begin{array}{c}(({\unicdcdadad} V0f0 \in (2^{{2}}) .  ({\unicdcdadad} V1f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
V0f0)~V1f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V1f))))){\unicdcdcdhd}(({\unicdcdadad} V2f0 \in (2^{{2}}) .  ({\unicdcdadad} V3f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
V2f0)~V3f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V3f))))){\unicdcdcdhd}(({\unicdcdadad} V4f0 \in (2^{{2}}) .  ({\unicdcdadad} V5f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
V4f0)~V5f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V5f))))){\unicdcdcdhd}(({\unicdcdadad} V6f0 \in (2^{{2}}) .  ({\unicdcdadad} V7f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V6f0)~V7f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V7f))))){\unicdcdcdhd}(({\unicdcdadad} V8f0 \in (2^{{2}}) .  ({\unicdcdadad} V9f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V8f0)~V9f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V9f))))){\unicdcdcdhd}(({\unicdcdadad} V10f0 \in (2^{{2}}) .  ({\unicdcdadad} V11f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~\\
V10f0)~V11f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V11f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V12f0 \in (2^{{2}}) .  ({\unicdcdadad} V13f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
V12f0)~V13f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V13f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V14f0 \in (2^{{2}}) .  ({\unicdcdadad} V15f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
V14f0)~V15f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V15f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V16f0 \in (2^{{2}}) .  ({\unicdcdadad} V17f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V16f0)~V17f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V17f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V18f0 \in (2^{{2}}) .  ({\unicdcdadad} V19f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V18f0)~V19f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V19f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V20f0 \in (2^{{2}}) .  ({\unicdcdadad} V21f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~\\
V20f0)~V21f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V21f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V22f0 \in (2^{{2}}) .  ({\unicdcdadad} V23f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
V22f0)~V23f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V23f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V24f0 \in (2^{{2}}) .  ({\unicdcdadad} V25f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
V24f0)~V25f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V25f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V26f0 \in (2^{{2}}) .  ({\unicdcdadad} V27f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V26f0)~V27f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V27f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V28f0 \in (2^{{2}}) .  ({\unicdcdadad} V29f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V28f0)~V29f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V29f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V30f0 \in (2^{{2}}) .  ({\unicdcdadad} V31f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~\\
V30f0)~V31f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V31f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V32f0 \in (2^{{2}}) .  ({\unicdcdadad} V33f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
V32f0)~V33f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V33f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V34f0 \in (2^{{2}}) .  ({\unicdcdadad} V35f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
V34f0)~V35f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V35f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V36f0 \in (2^{{2}}) .  ({\unicdcdadad} V37f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V36f0)~V37f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V37f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V38f0 \in (2^{{2}}) .  ({\unicdcdadad} V39f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V38f0)~V39f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V39f))))){\unicdcdcdhd}\\
(({\unicdcdadad} V40f0 \in (2^{{2}}) .  ({\unicdcdadad} V41f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~V40f0)~\\
V41f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V41f))))){\unicdcdcdhd}(({\unicdcdadad} V42f0 \in (2^{{2}}) .  ({\unicdcdadad} V43f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~V42f0)~V43f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V43f))))){\unicdcdcdhd}(({\unicdcdadad} V44f0 \in (2^{{2}}) .  ({\unicdcdadad} V45f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~V44f0)~V45f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V45f))))){\unicdcdcdhd}(({\unicdcdadad} V46f0 \in (2^{{2}}) .  ({\unicdcdadad} V47f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~V46f0)~V47f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V47f))))){\unicdcdcdhd}(({\unicdcdadad} V48f0 \in (2^{{2}}) .  ({\unicdcdadad} V49f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V48f0)~V49f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V49f))))){\unicdcdcdhd}(({\unicdcdadad} V50f0 \in (2^{{2}}) .  ({\unicdcdadad} V51f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~V50f0)~\\
V51f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V51f))))){\unicdcdcdhd}(({\unicdcdadad} V52f0 \in (2^{{2}}) .  ({\unicdcdadad} V53f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~V52f0)~V53f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V53f))))){\unicdcdcdhd}(({\unicdcdadad} V54f0 \in (2^{{2}}) .  ({\unicdcdadad} V55f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~V54f0)~V55f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V55f))))){\unicdcdcdhd}(({\unicdcdadad} V56f0 \in (2^{{2}}) .  ({\unicdcdadad} V57f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~V56f0)~V57f))){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V57f))))){\unicdcdcdhd}(({\unicdcdadad} V58f0 \in (2^{{2}}) .  ({\unicdcdadad} V59f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V58f0)~V59f))){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V59f))))){\unicdcdcdhd}(({\unicdcdadad} V60f0 \in (2^{{2}}) .  ({\unicdcdadad} V61f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~\\
V60f0)~V61f))){\unicdbdjded}(p~(ap~V60f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V61f)))))){\unicdcdcdhd}(({\unicdcdadad} V62f0 \in (2^{{2}}) .  ({\unicdcdadad} V63f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
V62f0)~V63f))){\unicdbdjded}(p~(ap~V62f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~\\
V63f)))))){\unicdcdcdhd}(({\unicdcdadad} V64f0 \in (2^{{2}}) .  ({\unicdcdadad} V65f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
V64f0)~V65f))){\unicdbdjded}(p~(ap~V64f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~\\
V65f)))))){\unicdcdcdhd}(({\unicdcdadad} V66f0 \in (2^{{2}}) .  ({\unicdcdadad} V67f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
V66f0)~V67f))){\unicdbdjded}(p~(ap~V66f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~\\
V67f)))))){\unicdcdcdhd}(({\unicdcdadad} V68f0 \in (2^{{2}}) .  ({\unicdcdadad} V69f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
V68f0)~V69f))){\unicdbdjded}(p~(ap~V68f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V69f)))))){\unicdcdcdhd}({\unicdcdadad} V70f0 \in (2^{{2}}) .  ({\unicdcdadad} V71f \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
V70f0)~V71f))){\unicdbdjded}(p~(ap~V70f0~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V71f)))))))))))))))))))))))))))))))))))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfbgdgdgggfhahegdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0f1 \in ty\_2Ebinary\_\_ieee\_2Eflags .  ({\unicdcdadad} V1f2 \in ty\_2Ebinary\_\_ieee\_2Eflags .  \\
((V0f1=V1f2){\unicdbdjded}(((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~\\
V0f1)){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero~V1f2))){\unicdcdcdhd}\\
(((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~V0f1)){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp~\\
V1f2))){\unicdcdcdhd}(((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V0f1)){\unicdbdjded}\\
(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow~V1f2))){\unicdcdcdhd}(((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~\\
V0f1)){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision~V1f2))){\unicdcdcdhd}\\
(((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V0f1)){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding~\\
V1f2))){\unicdcdcdhd}((p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V0f1)){\unicdbdjded}(p~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding~\\
V1f2)))))))))))\end{array}
\label{hyp:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfdgpgngahpgogfgogehpfpffgbhfhbgmgjgehjh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}(\\
{\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1y \in A\_27b .  ((ap~(ap~(\mname{c\_2Ecombin\_2EK}~\\
A\_27a~A\_27b)~V0x)~V1y)=V0x)))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfelepfpfefiene}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfecgjgogbgchjhpfpfjgfgfgfgpfcdfeggmgbghgdhpfpfmgjgehfgchbgmgpfpfbdbd}
$$\begin{array}{c}({\unicdcdadad} V0b41 \in 2 .  ({\unicdcdadad} V1b31 \in 2 .  ({\unicdcdadad} V2b21 \in 2 .  ({\unicdcdadad} V3b11 \in \\
2 .  ({\unicdcdadad} V4b01 \in 2 .  ({\unicdcdadad} V5b1 \in 2 .  ({\unicdcdadad} V6b42 \in 2 .  ({\unicdcdadad} V7b32 \in \\
2 .  ({\unicdcdadad} V8b22 \in 2 .  ({\unicdcdadad} V9b12 \in 2 .  ({\unicdcdadad} V10b02 \in 2 .  \\
({\unicdcdadad} V11b2 \in 2 .  (((ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V0b41))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V1b31))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V2b21))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V3b11))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V4b01))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V5b1))~(c\_2Ebool\_2EARB~ty\_2Ebinary\_\_ieee\_2Eflags)))))))=\\
(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_DivideByZero\_\_fupd~(ap~(\mname{c\_2Ecombin\_2EK}~\\
2~2)~V6b42))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_InvalidOp\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V7b32))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Overflow\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V8b22))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Precision\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V9b12))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_BeforeRounding\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V10b02))~(ap~(ap~c\_2Ebinary\_\_ieee\_2Eflags\_\_Underflow\_\_AfterRounding\_\_fupd~\\
(ap~(\mname{c\_2Ecombin\_2EK}~2~2)~V11b2))~(c\_2Ebool\_2EARB~ty\_2Ebinary\_\_ieee\_2Eflags)))))))){\unicdbdjded}\\
(((p~V0b41){\unicdbdjded}(p~V6b42)){\unicdcdcdhd}(((p~V1b31){\unicdbdjded}(p~V7b32)){\unicdcdcdhd}(((p~V2b21){\unicdbdjded}(p~\\
V8b22)){\unicdcdcdhd}(((p~V3b11){\unicdbdjded}(p~V9b12)){\unicdcdcdhd}(((p~V4b01){\unicdbdjded}(p~V10b02)){\unicdcdcdhd}((p~V5b1){\unicdbdjded}\\
(p~V11b2))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
