\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\_2Ealignment\_2Ealigned\_\_numeric (TMPmkjUdXZkxkR6sFBuTDnP2s73cCmUjMtN)}
\maketitle
Let $ c\_2Enum\_2EZERO\_\_REP : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2EZERO\_\_REP} \in {omega}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfekffecfpepfpfcffeaf}
\end{equation}
Let $ ty\_2Enum\_2Enum : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Enum\_2Enum}}\label{hyp:ogfgpfehjhpfcdfeogfhngpfcdfeogfhng}
\end{equation}
Let $ c\_2Enum\_2EABS\_\_num : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2EABS\_\_num} \in {({{ty\_2Enum\_2Enum}^{{omega}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfebecedfpfpfogfhng}
\end{equation}
\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:dgpfcdfeogfhngpfcdfead}
We define $\mname{c\_2Enum\_2E0}$ to be ${({{{ap}~{c\_2Enum\_2EABS\_\_num}}~{c\_2Enum\_2EZERO\_\_REP}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfekffecfpe}
We define $\mname{c\_2Earithmetic\_2EZERO}$ to be ${\mname{c\_2Enum\_2E0}}$.
\end{definition}
Let $ c\_2Enum\_2EREP\_\_num : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2EREP\_\_num} \in {({{omega}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfecffeafpfpfogfhng}
\end{equation}
Let $ c\_2Enum\_2ESUC\_\_REP : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2ESUC\_\_REP} \in {({{omega}^{{omega}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfedfffdepfpfcffeaf}
\end{equation}
\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:dgpfcdfeogfhngpfcdfedfffde}
We define $\mname{c\_2Enum\_2ESUC}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {({{{ap}~{c\_2Enum\_2EABS\_\_num}}~{({{{ap}~{c\_2Enum\_2ESUC\_\_REP}}~{({{{ap}~{c\_2Enum\_2EREP\_\_num}}~{V0m}})}})}})}}$.
\end{definition}
Let $ c\_2Earithmetic\_2E\_2B : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2E\_2B \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepfcdce}
\end{equation}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfecejeefbd}
We define $\mname{c\_2Earithmetic\_2EBIT1}$ to be ${{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{\mname{c\_2Enum\_2E0}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfeoeffnefecfbeme}
We define $\mname{c\_2Earithmetic\_2ENUMERAL}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {V0x}}$.
\end{definition}
Let $ ty\_2Ebool\_2Eitself : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Ebool\_2Eitself}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfecgpgpgmgpfcdfejgehdhfgmggg}
\end{equation}
Let $ c\_2Ebool\_2Ethe\_\_value : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ebool\_2Ethe\_\_value~A\_27a \in (\\
ty\_2Ebool\_2Eitself~A\_27a)\end{array}
\label{hyp:ngfgngpfdgpfcdfecgpgpgmgpfcdfeehigfgpfpfghbgmgfhfg}
\end{equation}
Let $ c\_2Efcp\_2Edimindex : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Efcp\_2Edimindex~A\_27a \in (ty\_2Enum\_2Enum^{{({{ty\_2Ebool\_2Eitself}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeggdgahpfcdfeegjgngjgogegfgih}
\end{equation}
Let $ c\_2Earithmetic\_2E\_2D : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2E\_2D \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepfcdee}
\end{equation}
Let $ ty\_2Efcp\_2Efinite\_\_image : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Efcp\_2Efinite\_\_image}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfeggdgahpfcdfeggjgogjgehfgpfpfjgngbghgfg}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfege}
We define $\mname{c\_2Ebool\_2EF}$ to be ${({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V0t \in {2} .  {V0t}})}})}$.
\end{definition}
\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:dgpfcdfecgpgpgmgpfcdfepfhdfe}
We define $\mname{c\_2Ebool\_2E\_7E}$ to be ${({{\uniddcgcg} V0t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t}})}}~{\mname{c\_2Ebool\_2EF}}})}})}$.
\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:dgpfcdfengjgogpfcdfepfedad}
We define $\mname{c\_2Emin\_2E\_40}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} P \in {{2}^{{A}}} .  {{\mathbf{if}}~{({{\unicdcdaddd} x \in {A} .  {{p}~{({{{ap}~{P}}~{x}})}}})}~{\mathbf{then}}~{({{the}~{({{\uniddcgcg} x .  {{{x} \in {A}}{\unicdcdcdhd}{{p}~{({{{ap}~{P}}~{x}})}}}})}})}~{\mathbf{else}}~{({{the}~{({{\uniddcgcg} x .  {{x} \in {A}}})}})}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfddge}
We define $\mname{c\_2Ebool\_2E\_3F}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{V0P}}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{A\_27a}})}}~{V0P}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeahchjgngpfpfchfgdgpfcdfepfddde}
We define $\mname{c\_2Eprim\_\_rec\_2E\_3C}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_3F}}~{({{2}^{{ty\_2Enum\_2Enum}}})}})}}~{({{\uniddcgcg} V2P \in {({{2}^{{ty\_2Enum\_2Enum}}})} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{ty\_2Enum\_2Enum}})}}~{({{\uniddcgcg} V3n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{V2P}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{V3n}})}})}})}}~{({{{ap}~{V2P}}~{V3n}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{V2P}}~{V0m}})}})}}~{({{{ap}~{\mname{c\_2Ebool\_2E\_7E}}}~{({{{ap}~{V2P}}~{V1n}})}})}})}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfddgepfcdbd}
We define $\mname{c\_2Ebool\_2E\_3F\_21}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_3F}}~{A\_27a}})}}~{V0P}})}})}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V2y \in {A\_27a} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{V0P}}~{V1x}})}})}}~{({{{ap}~{V0P}}~{V2y}})}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V1x}})}}~{V2y}})}})}})}})}})}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeggdgahpfcdfeggjgogjgehfgpfpfjgogegfgih}
We define $\mname{c\_2Efcp\_2Efinite\_\_index}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{({{A\_27a}^{{ty\_2Enum\_2Enum}}})}})}}~{({{\uniddcgcg} V0f \in {({{A\_27a}^{{ty\_2Enum\_2Enum}}})} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_3F\_21}}~{ty\_2Enum\_2Enum}})}}~{({{\uniddcgcg} V2n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V2n}})}}~{({{{ap}~{({{c\_2Efcp\_2Edimindex}~{A\_27a}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27a}})}})}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{V0f}}~{V2n}})}})}}~{V1x}})}})}})}})}})}})}})}})}}$.
\end{definition}
Let $ ty\_2Efcp\_2Ecart : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A0 .  nonempty~A0{\unicdbdjdcd}{\unicdcdadad} A1 .  nonempty~A1{\unicdbdjdcd}nonempty~(ty\_2Efcp\_2Ecart~\\
A0~A1)\end{array}
\label{hyp:ogfgpfehjhpfcdfeggdgahpfcdfedgbgcheh}
\end{equation}
Let $ c\_2Efcp\_2Edest\_\_cart : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}c\_2Efcp\_2Edest\_\_cart~\\
A\_27a~A\_27b \in ((A\_27a^{{({{ty\_2Efcp\_2Efinite\_\_image}~{A\_27b}})}})^{{({{{ty\_2Efcp\_2Ecart}~{A\_27a}}~{A\_27b}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeggdgahpfcdfeegfgdhehpfpfdgbgcheh}
\end{equation}
\begin{definition}\label{def:dgpfcdfeggdgahpfcdfeggdgahpfpfjgogegfgih}
We define $\mname{c\_2Efcp\_2Efcp\_\_index}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} V0x \in {({{{ty\_2Efcp\_2Ecart}~{A\_27a}}~{A\_27b}})} .  {{\uniddcgcg} V1i \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{{c\_2Efcp\_2Edest\_\_cart}~{A\_27a}}~{A\_27b}})}}~{V0x}})}}~{({{{ap}~{({{\mname{c\_2Efcp\_2Efinite\_\_index}}~{({{ty\_2Efcp\_2Efinite\_\_image}~{A\_27b}})}})}}~{V1i}})}})}}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfedepeoeee}
We define $\mname{c\_2Ebool\_2ECOND}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0t \in {2} .  {({{\uniddcgcg} V1t1 \in {A\_27a} .  {({{\uniddcgcg} V2t2 \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{A\_27a}})}}~{({{\uniddcgcg} V3x \in {A\_27a} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{2}})}}~{V0t}})}}~{\mname{c\_2Ebool\_2ET}}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V3x}})}}~{V1t1}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{2}})}}~{V0t}})}}~{\mname{c\_2Ebool\_2EF}}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V3x}})}}~{V2t2}})}})}})}})}})}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfenejeoe}
We define $\mname{c\_2Earithmetic\_2EMIN}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V0m}})}}~{V1n}})}})}}~{V0m}})}}~{V1n}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepffddepfcdge}
We define $\mname{c\_2Ebool\_2E\_5C\_2F}$ 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}})}}~{V2t}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V1t2}})}}~{V2t}})}})}}~{V2t}})}})}})}})}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfepfdddepfddee}
We define $\mname{c\_2Earithmetic\_2E\_3C\_3D}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_5C\_2F}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V0m}})}}~{V1n}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{V0m}})}}~{V1n}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeggdgahpfcdfegedeaf}
We define $\mname{c\_2Efcp\_2EFCP}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {({{\uniddcgcg} V0g \in {({{A\_27a}^{{ty\_2Enum\_2Enum}}})} .  {({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{({{{ty\_2Efcp\_2Ecart}~{A\_27a}}~{A\_27b}})}})}}~{({{\uniddcgcg} V1f \in {({{{ty\_2Efcp\_2Ecart}~{A\_27a}}~{A\_27b}})} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{ty\_2Enum\_2Enum}})}}~{({{\uniddcgcg} V2i \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V2i}})}}~{({{{ap}~{({{c\_2Efcp\_2Edimindex}~{A\_27b}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27b}})}})}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{\mname{c\_2Efcp\_2Efcp\_\_index}}~{A\_27a}}~{A\_27b}})}}~{V1f}})}}~{V2i}})}})}}~{({{{ap}~{V0g}}~{V2i}})}})}})}})}})}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhpgchegpfpfdhmgjgdgfg}
We define $\mname{c\_2Ewords\_2Eword\_\_slice}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0h \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1l \in {ty\_2Enum\_2Enum} .  {({{\uniddcgcg} V2w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{{\mname{c\_2Efcp\_2EFCP}}~{2}}~{A\_27a}})}}~{({{\uniddcgcg} V3i \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Earithmetic\_2E\_3C\_3D}}}~{V1l}})}}~{V3i}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Earithmetic\_2E\_3C\_3D}}}~{V3i}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Earithmetic\_2EMIN}}}~{V0h}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2D}}~{({{{ap}~{({{c\_2Efcp\_2Edimindex}~{A\_27a}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27a}})}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{({{{\mname{c\_2Efcp\_2Efcp\_\_index}}~{2}}~{A\_27a}})}}~{V2w}})}}~{V3i}})}})}})}})}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgmgjghgogngfgogehpfcdfebgmgjghgog}
We define $\mname{c\_2Ealignment\_2Ealign}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0p \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ewords\_2Eword\_\_slice}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2D}}~{({{{ap}~{({{c\_2Efcp\_2Edimindex}~{A\_27a}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27a}})}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}})}}~{V0p}})}}~{V1w}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgmgjghgogngfgogehpfcdfebgmgjghgogfgeg}
We define $\mname{c\_2Ealignment\_2Ealigned}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0p \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ealignment\_2Ealign}}~{A\_27a}})}}~{V0p}})}}~{V1w}})}})}}~{V1w}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfepfddfe}
We define $\mname{c\_2Earithmetic\_2E\_3E}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V1n}})}}~{V0m}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfepfddfepfddee}
We define $\mname{c\_2Earithmetic\_2E\_3E\_3D}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_5C\_2F}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Earithmetic\_2E\_3E}}}~{V0m}})}}~{V1n}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{V0m}})}}~{V1n}})}})}}}$.
\end{definition}
Let $ c\_2Earithmetic\_2EEXP : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2EEXP \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfefeifaf}
\end{equation}
\begin{definition}\label{def:dgpfcdfeogfhngfgchbgmgpfcdfejgjgdfffde}
We define $\mname{c\_2Enumeral\_2EiiSUC}$ to be ${{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{V0n}})}})}}$.
\end{definition}
Let $ c\_2Earithmetic\_2EEVEN : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Earithmetic\_2EEVEN} \in {({{2}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfefegffeoe}
\end{equation}
Let $ c\_2Enumeral\_2Eonecount : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Enumeral\_2Eonecount \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeogfhngfgchbgmgpfcdfepgogfgdgpgfhogeh}
\end{equation}
Let $ c\_2Enumeral\_2Eexactlog : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enumeral\_2Eexactlog} \in {({{ty\_2Enum\_2Enum}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngfgchbgmgpfcdfefgihbgdgehmgpghg}
\end{equation}
\begin{definition}\label{def:dgpfcdfeahchjgngpfpfchfgdgpfcdfeafcffe}
We define $\mname{c\_2Eprim\_\_rec\_2EPRE}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{V0m}})}}~{\mname{c\_2Enum\_2E0}}})}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{ty\_2Enum\_2Enum}})}}~{({{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{V0m}})}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{V1n}})}})}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfecejeefcd}
We define $\mname{c\_2Earithmetic\_2EBIT2}$ to be ${{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{\mname{c\_2Enum\_2E0}}})}})}})}})}}$.
\end{definition}
Let $ c\_2Earithmetic\_2EDIV : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2EDIV \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfeeejegf}
\end{equation}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfeeejegfcd}
We define $\mname{c\_2Earithmetic\_2EDIV2}$ to be ${{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EDIV}}~{V0n}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT2}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}$.
\end{definition}
Let $ c\_2Enumeral\_2Etexp\_\_help : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Enumeral\_2Etexp\_\_help \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeogfhngfgchbgmgpfcdfeehfgihahpfpfigfgmgah}
\end{equation}
Let $ c\_2Earithmetic\_2EODD : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Earithmetic\_2EODD} \in {({{2}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepeeeee}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfemefeef}
We define $\mname{c\_2Ebool\_2ELET}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {({{\uniddcgcg} V0f \in {({{A\_27b}^{{A\_27a}}})} .  {({{\uniddcgcg} V1x \in {A\_27a} .  {({{{ap}~{V0f}}~{V1x}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngfgchbgmgpfcdfejgeeffce}
We define $\mname{c\_2Enumeral\_2EiDUB}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0x}})}}~{V0x}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngfgchbgmgpfcdfejgkf}
We define $\mname{c\_2Enumeral\_2EiZ}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {V0x}}$.
\end{definition}
Let $ c\_2Earithmetic\_2E\_2A : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2E\_2A \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepfcdbe}
\end{equation}
\begin{definition}\label{def:dgpfcdfeogfhngfgchbgmgpfcdfejgogehfgchogbgmgpfpfngfhmgeh}
We define $\mname{c\_2Enumeral\_2Einternal\_\_mult}$ to be ${c\_2Earithmetic\_2E\_2A}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgjgehpfcdfedfcejeef}
We define $\mname{c\_2Ebit\_2ESBIT}$ to be ${{\uniddcgcg} V0b \in {2} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{ty\_2Enum\_2Enum}})}}~{V0b}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EEXP}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT2}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{V1n}})}})}}~{\mname{c\_2Enum\_2E0}}})}}}$.
\end{definition}
Let $ c\_2Esum\_\_num\_2ESUM : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Esum\_\_num\_2ESUM \in ((ty\_2Enum\_2Enum^{{({{ty\_2Enum\_2Enum}^{{ty\_2Enum\_2Enum}}})}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfhngpfpfogfhngpfcdfedfffne}
\end{equation}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhcdog}
We define $\mname{c\_2Ewords\_2Ew2n}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{c\_2Esum\_\_num\_2ESUM}}~{({{{ap}~{({{c\_2Efcp\_2Edimindex}~{A\_27a}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27a}})}})}})}}~{({{\uniddcgcg} V1i \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebit\_2ESBIT}}}~{({{{ap}~{({{{ap}~{({{{\mname{c\_2Efcp\_2Efcp\_\_index}}~{2}}~{A\_27a}})}}~{V0w}})}}~{V1i}})}})}}~{V1i}})}})}})}}}$.
\end{definition}
Let $ c\_2Ewords\_2Edimword : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ewords\_2Edimword~A\_27a \in (ty\_2Enum\_2Enum^{{({{ty\_2Ebool\_2Eitself}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfehhpgchegdhpfcdfeegjgnghhpgcheg}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgjgehpfcdfeeejegfpfpfcdfeifaf}
We define $\mname{c\_2Ebit\_2EDIV\_\_2EXP}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EDIV}}~{V1n}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EEXP}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT2}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{V0x}})}})}}}$.
\end{definition}
Let $ c\_2Earithmetic\_2EMOD : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2EMOD \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfenepeee}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgjgehpfcdfenepeeepfpfcdfeifaf}
We define $\mname{c\_2Ebit\_2EMOD\_\_2EXP}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EMOD}}~{V1n}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2EEXP}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT2}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{V0x}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgjgehpfcdfecejeefdf}
We define $\mname{c\_2Ebit\_2EBITS}$ to be ${{\uniddcgcg} V0h \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1l \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V2n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebit\_2EMOD\_\_2EXP}}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2D}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{V0h}})}})}}~{V1l}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebit\_2EDIV\_\_2EXP}}}~{V1l}})}}~{V2n}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgjgehpfcdfecejeef}
We define $\mname{c\_2Ebit\_2EBIT}$ to be ${{\uniddcgcg} V0b \in {ty\_2Enum\_2Enum} .  {{\uniddcgcg} V1n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebit\_2EBITS}}}~{V0b}})}}~{V0b}})}}~{V1n}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfeogcdhh}
We define $\mname{c\_2Ewords\_2En2w}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{\mname{c\_2Efcp\_2EFCP}}~{2}}~{A\_27a}})}}~{({{\uniddcgcg} V1i \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebit\_2EBIT}}}~{V1i}})}}~{V0n}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhpgchegpfpfcddgpgngah}
We define $\mname{c\_2Ewords\_2Eword\_\_2comp}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{\mname{c\_2Ewords\_2En2w}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2D}}~{({{{ap}~{({{c\_2Ewords\_2Edimword}~{A\_27a}})}}~{({{c\_2Ebool\_2Ethe\_\_value}~{A\_27a}})}})}})}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Ew2n}}~{A\_27a}})}}~{V0w}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhpgchegpfpfbgegeg}
We define $\mname{c\_2Ewords\_2Eword\_\_add}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0v \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {{\uniddcgcg} V1w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{\mname{c\_2Ewords\_2En2w}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Ew2n}}~{A\_27a}})}}~{V0v}})}})}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Ew2n}}~{A\_27a}})}}~{V1w}})}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhpgchegpfpfdhfhcg}
We define $\mname{c\_2Ewords\_2Eword\_\_sub}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0v \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {{\uniddcgcg} V1w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Ewords\_2Eword\_\_add}}~{A\_27a}})}}~{V0v}})}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Eword\_\_2comp}}~{A\_27a}})}}~{V1w}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfehhpgchegdhpfcdfehhpgchegpfpfngfhmg}
We define $\mname{c\_2Ewords\_2Eword\_\_mul}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0v \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {{\uniddcgcg} V1w \in {({{{ty\_2Efcp\_2Ecart}~{2}}~{A\_27a}})} .  {({{{ap}~{({{\mname{c\_2Ewords\_2En2w}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2A}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Ew2n}}~{A\_27a}})}}~{V0v}})}})}}~{({{{ap}~{({{\mname{c\_2Ewords\_2Ew2n}}~{A\_27a}})}}~{V1w}})}})}})}}}}$.
\end{definition}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0w \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ({\unicdcdadad} V1x \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  (((p~(ap~(ap~\\
(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V0w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))~V1x)))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V0w))){\unicdcdcdhd}\\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a)~V0w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))~V1x)))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V0w)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V2x \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))~V2x))){\unicdcdcdhd}(p~\\
(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27a)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))))~V2x))))){\unicdcdcdhd}\\
(({\unicdcdadad} V3w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ({\unicdcdadad} V4x \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  (((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V3w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))~\\
V4x)))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~V3w))){\unicdcdcdhd}\\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a)~V3w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))~\\
V4x)))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~V3w)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V5x \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))~\\
V5x))){\unicdcdcdhd}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27a)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))~\\
V5x))))){\unicdcdcdhd}(({\unicdcdadad} V6w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ({\unicdcdadad} V7x \in \\
(ty\_2Efcp\_2Ecart~2~A\_27a) .  (((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V6w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))~V7x)))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V6w))){\unicdcdcdhd}\\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a)~V6w)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))~V7x)))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V6w)))))){\unicdcdcdhd}\\
({\unicdcdadad} V8x \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))~V8x))){\unicdcdcdhd}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))))))~V8x))))))))))\end{array}
\label{hyp:ehigngpfcdfebgmgjghgogngfgogehpfcdfebgmgjghgogfgegpfpfbgegegpfpfdhfhcgpfpfbdcddd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}((ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))=\\
(ap~\mname{c\_2Enum\_2ESUC}~\mname{c\_2Enum\_2E0}))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfepeoefe}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}((ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))=\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfeefhfpe}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~V1n)=(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V1n)~V0m))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfebeeeeepfpfdfjfne}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V2p \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V1n)~V2p))=(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~V1n))~V2p)))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfebeeeeepfpfbedfdfpede}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
((ap~(ap~c\_2Earithmetic\_2E\_2A~\mname{c\_2Enum\_2E0})~V0m)=\mname{c\_2Enum\_2E0}){\unicdcdcdhd}\\
(((ap~(ap~c\_2Earithmetic\_2E\_2A~V0m)~\mname{c\_2Enum\_2E0})=\mname{c\_2Enum\_2E0}){\unicdcdcdhd}\\
(((ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V0m)=V0m){\unicdcdcdhd}\\
(((ap~(ap~c\_2Earithmetic\_2E\_2A~V0m)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))=V0m){\unicdcdcdhd}(\\
((ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~\mname{c\_2Enum\_2ESUC}~V0m))~V1n)=(ap~\\
(ap~c\_2Earithmetic\_2E\_2B~(ap~(ap~c\_2Earithmetic\_2E\_2A~V0m)~V1n))~\\
V1n)){\unicdcdcdhd}((ap~(ap~c\_2Earithmetic\_2E\_2A~V0m)~(ap~\mname{c\_2Enum\_2ESUC}~V1n))=\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~(ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V0m)~V1n))))))))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfeneffmeefpfpfdemebeffdffedf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V2p \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~\\
(ap~c\_2Earithmetic\_2E\_2B~V0m)~V1n))~V2p)=(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~(ap~c\_2Earithmetic\_2E\_2A~V0m)~V2p))~(ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V1n)~V2p))))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfecfjeheieefpfpfbeeeeepfpfeejedfefcfjece}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V2p \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2A~V2p)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~V1n))=(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~(ap~c\_2Earithmetic\_2E\_2A~V2p)~V0m))~(ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V2p)~V1n))))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfemefegeefpfpfbeeeeepfpfeejedfefcfjece}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2A~(\\
ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
V0n)=(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V0n)))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfeefjenefedfcd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V2p \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0m)~V1n))~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0m)~V2p))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~V1n)~V2p))))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfebeeeeepfpfnepeoepepfpfmefedfdfpfpffebf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  (\\
(\preoh (V0m=V1n)){\unicdbdjded}((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Enum\_2ESUC}~\\
V0m))~V1n)){\unicdcdcdid}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Enum\_2ESUC}~\\
V1n))~V0m))))))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfeoepeefpfpfoeffnepfpffebf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2Enum\_2ESUC}~V0n)=(ap~(ap~\\
c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~V0n)))\end{array}
\label{hyp:ehigngpfcdfebgchjgehigngfgehjgdgpfcdfedfffdepfpfpeoefepfpfbeeeee}
\end{equation}
Assume the following.
\begin{equation}
{True}\label{hyp:ehigngpfcdfecgpgpgmgpfcdfeefcfffefie}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0t1 \in 2 .  ({\unicdcdadad} V1t2 \in 2 .  (((p~V0t1){\unicdbdjdcd}(p~V1t2)){\unicdbdjdcd}(((p~\\
V1t2){\unicdbdjdcd}(p~V0t1)){\unicdbdjdcd}((p~V0t1){\unicdbdjded}(p~V1t2))))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfejeneafpfpfbeoeefjedfjfnepfpfbeif}
\end{equation}
Assume the following.
\begin{equation}
{({{\unicdcdadad} V0t \in {2} .  {({{False}{\unicdbdjdcd}{({{p}~{V0t}})}})}})}\label{hyp:ehigngpfcdfecgpgpgmgpfcdfegebemedfjeefjf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0t \in 2 .  (({\unicdcdadad} V1x \in \\
A\_27a .  (p~V0t)){\unicdbdjded}(p~V0t)))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfegepecfbememepfpfdfjeneaf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0t \in 2 .  (((True{\unicdcdcdid}(p~V0t)){\unicdbdjded}True){\unicdcdcdhd}((((p~V0t){\unicdcdcdid}True){\unicdbdjded}True){\unicdcdcdhd}\\
(((False{\unicdcdcdid}(p~V0t)){\unicdbdjded}(p~V0t)){\unicdcdcdhd}((((p~V0t){\unicdcdcdid}False){\unicdbdjded}(p~V0t)){\unicdcdcdhd}(((p~V0t){\unicdcdcdid}\\
(p~V0t)){\unicdbdjded}(p~V0t)))))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfepecfpfpfdemebeffdffedf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(({\unicdcdadad} V0t \in 2 .  ((\preoh (\preoh (p~V0t))){\unicdbdjded}(p~V0t))){\unicdcdcdhd}(((\preoh True){\unicdbdjded}False){\unicdcdcdhd}\\
((\preoh False){\unicdbdjded}True)))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfeoepeefpfpfdemebeffdffedf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ((V0x=V0x){\unicdbdjded}\\
True))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfecffegemepfpfdemebeffdffe}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1y \in \\
A\_27a .  ((V0x=V1y){\unicdbdjded}(V1y=V0x))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfefebfpfpfdfjfnepfpffebf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0t \in 2 .  (((True{\unicdbdjded}(p~V0t)){\unicdbdjded}(p~V0t)){\unicdcdcdhd}((((p~V0t){\unicdbdjded}True){\unicdbdjded}\\
(p~V0t)){\unicdcdcdhd}(((False{\unicdbdjded}(p~V0t)){\unicdbdjded}(\preoh (p~V0t))){\unicdcdcdhd}(((p~V0t){\unicdbdjded}False){\unicdbdjded}(\preoh (\\
p~V0t)))))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfefebfpfpfdemebeffdffedf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0t1 \in A\_27a .  ({\unicdcdadad} V1t2 \in \\
A\_27a .  (((ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~A\_27a)~\mname{c\_2Ebool\_2ET})~V0t1)~\\
V1t2)=V0t1){\unicdcdcdhd}((ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~A\_27a)~\mname{c\_2Ebool\_2EF})~\\
V0t1)~V1t2)=V1t2))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfedepeoeeepfpfdemebeffdffedf}
\end{equation}
Assume the following.
\begin{equation}
{({{\unicdcdadad} V0t \in {2} .  {({{({{({{p}~{V0t}})}{\unicdbdjdcd}{False}})}{\unicdbdjded}{({{({{p}~{V0t}})}{\unicdbdjded}{False}})}})}})}\label{hyp:ehigngpfcdfecgpgpgmgpfcdfejeneafpfpfgepfpffebfpfpfge}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(((ap~\mname{c\_2Enum\_2ESUC}~\mname{c\_2Earithmetic\_2EZERO})=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})){\unicdcdcdhd}(({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~\\
\mname{c\_2Enum\_2ESUC}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))){\unicdcdcdhd}({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2Enum\_2ESUC}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1n))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Enum\_2ESUC}~V1n))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfdhfhdg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2B~\\
\mname{c\_2Enum\_2E0})~V0n)=V0n)){\unicdcdcdhd}(({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  ((ap~\\
(ap~c\_2Earithmetic\_2E\_2B~V1n)~\mname{c\_2Enum\_2E0})=V1n)){\unicdcdcdhd}(({\unicdcdadad} V2n \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V3m \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V2n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V3m))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Enumeral\_2EiZ}~(ap~\\
(ap~c\_2Earithmetic\_2E\_2B~V2n)~V3m)))))){\unicdcdcdhd}(({\unicdcdadad} V4n \in ty\_2Enum\_2Enum .  \\
((ap~(ap~c\_2Earithmetic\_2E\_2A~\mname{c\_2Enum\_2E0})~V4n)=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}\\
(({\unicdcdadad} V5n \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V5n)~\mname{c\_2Enum\_2E0})=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}(({\unicdcdadad} V6n \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V7m \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2A~(\\
ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V6n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V7m))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V6n)~V7m))))){\unicdcdcdhd}(({\unicdcdadad} V8n \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2D~\\
\mname{c\_2Enum\_2E0})~V8n)=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}(({\unicdcdadad} V9n \in ty\_2Enum\_2Enum .  \\
((ap~(ap~c\_2Earithmetic\_2E\_2D~V9n)~\mname{c\_2Enum\_2E0})=V9n)){\unicdcdcdhd}(({\unicdcdadad} V10n \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V11m \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2E\_2D~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V10n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V11m))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~(ap~c\_2Earithmetic\_2E\_2D~\\
V10n)~V11m))))){\unicdcdcdhd}(({\unicdcdadad} V12n \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2EEXP~\\
\mname{c\_2Enum\_2E0})~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V12n)))=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}(({\unicdcdadad} V13n \in ty\_2Enum\_2Enum .  ((ap~\\
(ap~c\_2Earithmetic\_2EEXP~\mname{c\_2Enum\_2E0})~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V13n)))=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}(({\unicdcdadad} V14n \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Earithmetic\_2EEXP~V14n)~\mname{c\_2Enum\_2E0})=\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))){\unicdcdcdhd}\\
(({\unicdcdadad} V15n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V16m \in ty\_2Enum\_2Enum .  \\
((ap~(ap~c\_2Earithmetic\_2EEXP~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V15n))~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V16m))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~(ap~c\_2Earithmetic\_2EEXP~V15n)~V16m))))){\unicdcdcdhd}(((ap~\mname{c\_2Enum\_2ESUC}~\\
\mname{c\_2Enum\_2E0})=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))){\unicdcdcdhd}(({\unicdcdadad} V17n \in ty\_2Enum\_2Enum .  (\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V17n))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Enum\_2ESUC}~V17n)))){\unicdcdcdhd}(((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~\mname{c\_2Enum\_2E0})=\\
\mname{c\_2Enum\_2E0}){\unicdcdcdhd}(({\unicdcdadad} V18n \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V18n))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~V18n)))){\unicdcdcdhd}(({\unicdcdadad} V19n \in ty\_2Enum\_2Enum .  \\
(((ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V19n)=\mname{c\_2Enum\_2E0}){\unicdbdjded}(V19n=\mname{c\_2Earithmetic\_2EZERO}))){\unicdcdcdhd}\\
(({\unicdcdadad} V20n \in ty\_2Enum\_2Enum .  ((\mname{c\_2Enum\_2E0}=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V20n)){\unicdbdjded}(V20n=\mname{c\_2Earithmetic\_2EZERO}))){\unicdcdcdhd}(({\unicdcdadad} V21n \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V22m \in ty\_2Enum\_2Enum .  (((ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V21n)=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V22m)){\unicdbdjded}(V21n=V22m)))){\unicdcdcdhd}\\
(({\unicdcdadad} V23n \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\\
V23n)~\mname{c\_2Enum\_2E0})){\unicdbdjded}False)){\unicdcdcdhd}(({\unicdcdadad} V24n \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\mname{c\_2Enum\_2E0})~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V24n))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\mname{c\_2Earithmetic\_2EZERO})~\\
V24n)))){\unicdcdcdhd}(({\unicdcdadad} V25n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V26m \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V25n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V26m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\\
V25n)~V26m))))){\unicdcdcdhd}(({\unicdcdadad} V27n \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E}~\\
\mname{c\_2Enum\_2E0})~V27n)){\unicdbdjded}False)){\unicdcdcdhd}(({\unicdcdadad} V28n \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V28n))~\mname{c\_2Enum\_2E0})){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\mname{c\_2Earithmetic\_2EZERO})~\\
V28n)))){\unicdcdcdhd}(({\unicdcdadad} V29n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V30m \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V29n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V30m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Eprim\_\_rec\_2E\_3C}~\\
V30m)~V29n))))){\unicdcdcdhd}(({\unicdcdadad} V31n \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
\mname{c\_2Enum\_2E0})~V31n)){\unicdbdjded}True)){\unicdcdcdhd}(({\unicdcdadad} V32n \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V32n))~\mname{c\_2Enum\_2E0})){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~V32n)~\\
\mname{c\_2Earithmetic\_2EZERO})))){\unicdcdcdhd}(({\unicdcdadad} V33n \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V34m \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V33n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V34m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~V33n)~V34m))))){\unicdcdcdhd}(\\
({\unicdcdadad} V35n \in ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E\_3D}~\\
V35n)~\mname{c\_2Enum\_2E0})){\unicdbdjded}True)){\unicdcdcdhd}(({\unicdcdadad} V36n \in ty\_2Enum\_2Enum .  \\
((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E\_3D}~\mname{c\_2Enum\_2E0})~V36n)){\unicdbdjded}(V36n=\\
\mname{c\_2Enum\_2E0}))){\unicdcdcdhd}(({\unicdcdadad} V37n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V38m \in \\
ty\_2Enum\_2Enum .  ((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3E\_3D}~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
V37n))~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V38m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
V38m)~V37n))))){\unicdcdcdhd}(({\unicdcdadad} V39n \in ty\_2Enum\_2Enum .  ((p~(ap~c\_2Earithmetic\_2EODD~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V39n))){\unicdbdjded}(p~(ap~c\_2Earithmetic\_2EODD~\\
V39n)))){\unicdcdcdhd}(({\unicdcdadad} V40n \in ty\_2Enum\_2Enum .  ((p~(ap~c\_2Earithmetic\_2EEVEN~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~V40n))){\unicdbdjded}(p~(ap~c\_2Earithmetic\_2EEVEN~\\
V40n)))){\unicdcdcdhd}((\preoh (p~(ap~c\_2Earithmetic\_2EODD~\mname{c\_2Enum\_2E0}))){\unicdcdcdhd}(p~(\\
ap~c\_2Earithmetic\_2EEVEN~\mname{c\_2Enum\_2E0})))))))))))))))))))))))))))))))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfegjgdhehchjgcg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1m \in ty\_2Enum\_2Enum .  (\\
((ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\mname{c\_2Earithmetic\_2EZERO})~\\
V0n))=V0n){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~\mname{c\_2Earithmetic\_2EZERO}))=V0n){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiZ}~(\\
ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))~(\\
ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~(\\
ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}\\
(((ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\mname{c\_2Earithmetic\_2EZERO})~\\
V0n))=(ap~\mname{c\_2Enum\_2ESUC}~V0n)){\unicdcdcdhd}(((ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~\mname{c\_2Earithmetic\_2EZERO}))=(ap~\mname{c\_2Enum\_2ESUC}~V0n)){\unicdcdcdhd}(((ap~\\
\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}(\\
((ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~V1m)))){\unicdcdcdhd}\\
(((ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\mname{c\_2Earithmetic\_2EZERO})~\\
V0n))=(ap~\mname{c\_2Enumeral\_2EiiSUC}~V0n)){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiiSUC}~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V0n)~\mname{c\_2Earithmetic\_2EZERO}))=(\\
ap~\mname{c\_2Enumeral\_2EiiSUC}~V0n)){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(\\
ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1m)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Enum\_2ESUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~V1m)))){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~V1m)))){\unicdcdcdhd}(((ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m)))=\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~V1m)))){\unicdcdcdhd}((ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m)))=\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Enumeral\_2EiiSUC}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0n)~V1m)))))))))))))))))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfbgegeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1m \in ty\_2Enum\_2Enum .  (\\
((\mname{c\_2Earithmetic\_2EZERO}=(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)){\unicdbdjded}False){\unicdcdcdhd}\\
((((ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)=\mname{c\_2Earithmetic\_2EZERO}){\unicdbdjded}\\
False){\unicdcdcdhd}(((\mname{c\_2Earithmetic\_2EZERO}=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n)){\unicdbdjded}False){\unicdcdcdhd}((((ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n)=\mname{c\_2Earithmetic\_2EZERO}){\unicdbdjded}\\
False){\unicdcdcdhd}((((ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1m)){\unicdbdjded}False){\unicdcdcdhd}((((ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n)=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1m)){\unicdbdjded}False){\unicdcdcdhd}((((ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)=(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1m)){\unicdbdjded}(V0n=V1m)){\unicdcdcdhd}(((ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n)=(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1m)){\unicdbdjded}(V0n=V1m)))))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpffgbh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1m \in ty\_2Enum\_2Enum .  (\\
((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\mname{c\_2Earithmetic\_2EZERO})~V0n)){\unicdbdjded}\\
True){\unicdcdcdhd}(((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~\mname{c\_2Earithmetic\_2EZERO})){\unicdbdjded}False){\unicdcdcdhd}(((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n))~\mname{c\_2Earithmetic\_2EZERO})){\unicdbdjded}False){\unicdcdcdhd}\\
(((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
V0n)~V1m))){\unicdcdcdhd}(((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
V0n)~V1m))){\unicdcdcdhd}(((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1m))){\unicdbdjded}(\preoh (p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
V1m)~V0n)))){\unicdcdcdhd}((p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V0n))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1m))){\unicdbdjded}(p~(ap~(ap~\mname{c\_2Earithmetic\_2E\_3C\_3D}~\\
V0n)~V1m)))))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfmgehfg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~\mname{c\_2Earithmetic\_2EZERO})=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}\\
(((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))=\\
\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}(({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~\\
\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~V0n))))){\unicdcdcdhd}(({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  \\
((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1n)))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1n)))){\unicdcdcdhd}({\unicdcdadad} V2n \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2n))=(ap~\mname{c\_2Earithmetic\_2EBIT1}~V2n)))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfahchfg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  (((ap~\mname{c\_2Enumeral\_2EiDUB}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))=(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Enumeral\_2EiDUB}~V0n))){\unicdcdcdhd}\\
(((ap~\mname{c\_2Enumeral\_2EiDUB}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n))=(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))){\unicdcdcdhd}((ap~\\
\mname{c\_2Enumeral\_2EiDUB}~\mname{c\_2Earithmetic\_2EZERO})=\mname{c\_2Earithmetic\_2EZERO}))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfejgeeffcepfpfchfgngpgghbgmg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((p~(ap~c\_2Earithmetic\_2EEVEN~\mname{c\_2Earithmetic\_2EZERO})){\unicdcdcdhd}\\
((p~(ap~c\_2Earithmetic\_2EEVEN~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n))){\unicdcdcdhd}\\
((\preoh (p~(ap~c\_2Earithmetic\_2EEVEN~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)))){\unicdcdcdhd}\\
((\preoh (p~(ap~c\_2Earithmetic\_2EODD~\mname{c\_2Earithmetic\_2EZERO}))){\unicdcdcdhd}((\\
\preoh (p~(ap~c\_2Earithmetic\_2EODD~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0n)))){\unicdcdcdhd}\\
(p~(ap~c\_2Earithmetic\_2EODD~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n)))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpffgghfgogpgegeg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0acc \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  \\
(((ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\mname{c\_2Earithmetic\_2EZERO})~V0acc)=\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V0acc)){\unicdcdcdhd}(((ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1n))~V0acc)=(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1n)))~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~V0acc))){\unicdcdcdhd}((ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1n))~V0acc)=(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1n))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0acc)))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeogfhngfgchbgmgpfpfehfgihahpfpfigfgmgah}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(({\unicdcdadad} V0x \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Enumeral\_2Eonecount~\\
\mname{c\_2Earithmetic\_2EZERO})~V0x)=V0x)){\unicdcdcdhd}(({\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V2x \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Enumeral\_2Eonecount~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1n))~V2x)=(ap~(ap~c\_2Enumeral\_2Eonecount~\\
V1n)~(ap~\mname{c\_2Enum\_2ESUC}~V2x))))){\unicdcdcdhd}({\unicdcdadad} V3n \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V4x \in ty\_2Enum\_2Enum .  ((ap~(ap~c\_2Enumeral\_2Eonecount~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V3n))~V4x)=\mname{c\_2Earithmetic\_2EZERO})))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfepgogfgdgpgfhogehpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(((ap~c\_2Enumeral\_2Eexactlog~\mname{c\_2Earithmetic\_2EZERO})=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}\\
(({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ((ap~c\_2Enumeral\_2Eexactlog~(\\
ap~\mname{c\_2Earithmetic\_2EBIT1}~V0n))=\mname{c\_2Earithmetic\_2EZERO})){\unicdcdcdhd}({\unicdcdadad} V1n \in \\
ty\_2Enum\_2Enum .  ((ap~c\_2Enumeral\_2Eexactlog~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1n))=(ap~(ap~(\mname{c\_2Ebool\_2ELET}~ty\_2Enum\_2Enum~ty\_2Enum\_2Enum)~\\
({\uniddcgcg} V2x \in ty\_2Enum\_2Enum .  (ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~ty\_2Enum\_2Enum)~\\
(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~ty\_2Enum\_2Enum)~V2x)~\mname{c\_2Earithmetic\_2EZERO}))~\\
\mname{c\_2Earithmetic\_2EZERO})~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V2x))))~(ap~\\
(ap~c\_2Enumeral\_2Eonecount~V1n)~\mname{c\_2Earithmetic\_2EZERO}))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfefgihbgdgehmgpghgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0x \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2Earithmetic\_2EDIV2}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~V0x))=V0x))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfeeejegfcdpfpfcejeefbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1x \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V2y \in ty\_2Enum\_2Enum .  (((ap~(ap~c\_2Earithmetic\_2E\_2A~\mname{c\_2Earithmetic\_2EZERO})~\\
V0n)=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}(((ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V0n)~\mname{c\_2Earithmetic\_2EZERO})=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}(((ap~\\
(ap~c\_2Earithmetic\_2E\_2A~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1x))~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~V2y))=(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V2y))){\unicdcdcdhd}\\
(((ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1x))~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y))=(ap~(ap~(\mname{c\_2Ebool\_2ELET}~ty\_2Enum\_2Enum~\\
ty\_2Enum\_2Enum)~({\uniddcgcg} V3n \in ty\_2Enum\_2Enum .  (ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~\\
ty\_2Enum\_2Enum)~(ap~c\_2Earithmetic\_2EODD~V3n))~(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EDIV2}~V3n))~(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1x))))~(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y)))))~(ap~c\_2Enumeral\_2Eexactlog~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y)))){\unicdcdcdhd}(((ap~(ap~c\_2Earithmetic\_2E\_2A~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V2y))=\\
(ap~(ap~(\mname{c\_2Ebool\_2ELET}~ty\_2Enum\_2Enum~ty\_2Enum\_2Enum)~({\uniddcgcg} V4m \in \\
ty\_2Enum\_2Enum .  (ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~ty\_2Enum\_2Enum)~\\
(ap~c\_2Earithmetic\_2EODD~V4m))~(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EDIV2}~V4m))~(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V2y))))~(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V2y)))))~(ap~c\_2Enumeral\_2Eexactlog~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1x)))){\unicdcdcdhd}((ap~(ap~c\_2Earithmetic\_2E\_2A~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y))=\\
(ap~(ap~(\mname{c\_2Ebool\_2ELET}~ty\_2Enum\_2Enum~ty\_2Enum\_2Enum)~({\uniddcgcg} V5m \in \\
ty\_2Enum\_2Enum .  (ap~(ap~(\mname{c\_2Ebool\_2ELET}~ty\_2Enum\_2Enum~ty\_2Enum\_2Enum)~\\
({\uniddcgcg} V6n \in ty\_2Enum\_2Enum .  (ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~ty\_2Enum\_2Enum)~\\
(ap~c\_2Earithmetic\_2EODD~V5m))~(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~\\
(ap~\mname{c\_2Earithmetic\_2EDIV2}~V5m))~(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V2y))))~(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~ty\_2Enum\_2Enum)~(ap~c\_2Earithmetic\_2EODD~\\
V6n))~(ap~(ap~c\_2Enumeral\_2Etexp\_\_help~(ap~\mname{c\_2Earithmetic\_2EDIV2}~\\
V6n))~(ap~\mname{c\_2Eprim\_\_rec\_2EPRE}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1x))))~\\
(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V1x))~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y))))))~(ap~c\_2Enumeral\_2Eexactlog~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2y)))))~(ap~c\_2Enumeral\_2Eexactlog~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V1x))))))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfefgogfhngfgchbgmgpfpfngfhmgeh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0n \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V1m \in ty\_2Enum\_2Enum .  (\\
((ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~\mname{c\_2Earithmetic\_2EZERO})~\\
V0n)=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}(((ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~\\
V0n)~\mname{c\_2Earithmetic\_2EZERO})=\mname{c\_2Earithmetic\_2EZERO}){\unicdcdcdhd}(((ap~\\
(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
V0n))~V1m)=(ap~\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
(ap~\mname{c\_2Enumeral\_2EiDUB}~(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~\\
V0n)~V1m)))~V1m))){\unicdcdcdhd}((ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~V0n))~V1m)=(ap~\mname{c\_2Enumeral\_2EiDUB}~(ap~\\
\mname{c\_2Enumeral\_2EiZ}~(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~(ap~\mname{c\_2Enumeral\_2Einternal\_\_mult}~\\
V0n)~V1m))~V1m)))))))))\end{array}
\label{hyp:ehigngpfcdfeogfhngfgchbgmgpfcdfejgogehfgchogbgmgpfpfngfhmgehpfpfdgigbgchbgdgehfgchjgdhbgehjgpgog}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  ((ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~V0m))~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a)~V1n))=(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~(ap~c\_2Earithmetic\_2E\_2B~\\
V0m)~V1n)))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehhpgchegpfpfbgegegpfpfogcdhh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0m \in ty\_2Enum\_2Enum .  (\\
{\unicdcdadad} V1n \in ty\_2Enum\_2Enum .  ((ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~V0m))~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a)~V1n))=(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~(ap~c\_2Earithmetic\_2E\_2A~\\
V0m)~V1n)))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehhpgchegpfpfngfhmgpfpfogcdhh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0v \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ({\unicdcdadad} V1w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ({\unicdcdadad} V2x \in \\
(ty\_2Efcp\_2Ecart~2~A\_27a) .  ((ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~\\
V0v)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V1w)~V2x))=(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~\\
A\_27a)~V0v)~V1w))~V2x)))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehfpecfeepfpfbeeeeepfpfbedfdfpede}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0v \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ({\unicdcdadad} V1w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ((ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~\\
A\_27a)~V0v)~V1w)=(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V1w)~V0v))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehfpecfeepfpfbeeeeepfpfdepenene}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0v \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ({\unicdcdadad} V1w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ({\unicdcdadad} V2x \in \\
(ty\_2Efcp\_2Ecart~2~A\_27a) .  ((ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~\\
V0v)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~V1w)~V2x))=(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~\\
A\_27a)~V0v)~V1w))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~V0v)~V2x))))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehfpecfeepfpfmefegeefpfpfbeeeeepfpfeejedfefcfjece}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0v \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ({\unicdcdadad} V1w \in (ty\_2Efcp\_2Ecart~2~A\_27a) .  ((ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~\\
A\_27a)~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~V0v)~V1w))=(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~\\
A\_27a)~V0v))~V1w))))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehfpecfeepfpfoefehepfpfmeneffme}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0w \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a) .  ((ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27a)~V0w)=(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_mul}~A\_27a)~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27a)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))~V0w)))\end{array}
\label{hyp:ehigngpfcdfehhpgchegdhpfcdfehfpecfeepfpfoefehepfpfneffme}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfebgmgjghgogngfgogehpfcdfebgmgjghgogfgegpfpfogfhngfgchjgdg}
$$\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27a0 .  nonempty~A\_27a0{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a1 .  nonempty~A\_27a1{\unicdbdjdcd}{\unicdcdadad} A\_27a10 .  nonempty~A\_27a10{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a11 .  nonempty~A\_27a11{\unicdbdjdcd}{\unicdcdadad} A\_27a12 .  nonempty~A\_27a12{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a13 .  nonempty~A\_27a13{\unicdbdjdcd}{\unicdcdadad} A\_27a14 .  nonempty~A\_27a14{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a15 .  nonempty~A\_27a15{\unicdbdjdcd}{\unicdcdadad} A\_27a16 .  nonempty~A\_27a16{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a17 .  nonempty~A\_27a17{\unicdbdjdcd}{\unicdcdadad} A\_27a18 .  nonempty~A\_27a18{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a19 .  nonempty~A\_27a19{\unicdbdjdcd}{\unicdcdadad} A\_27a2 .  nonempty~A\_27a2{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a20 .  nonempty~A\_27a20{\unicdbdjdcd}{\unicdcdadad} A\_27a21 .  nonempty~A\_27a21{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a22 .  nonempty~A\_27a22{\unicdbdjdcd}{\unicdcdadad} A\_27a23 .  nonempty~A\_27a23{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a24 .  nonempty~A\_27a24{\unicdbdjdcd}{\unicdcdadad} A\_27a25 .  nonempty~A\_27a25{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a26 .  nonempty~A\_27a26{\unicdbdjdcd}{\unicdcdadad} A\_27a27 .  nonempty~A\_27a27{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a3 .  nonempty~A\_27a3{\unicdbdjdcd}{\unicdcdadad} A\_27a4 .  nonempty~A\_27a4{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a5 .  nonempty~A\_27a5{\unicdbdjdcd}{\unicdcdadad} A\_27a6 .  nonempty~A\_27a6{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a7 .  nonempty~A\_27a7{\unicdbdjdcd}{\unicdcdadad} A\_27a8 .  nonempty~A\_27a8{\unicdbdjdcd}\\
{\unicdcdadad} A\_27a9 .  nonempty~A\_27a9{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}\\
{\unicdcdadad} A\_27c .  nonempty~A\_27c{\unicdbdjdcd}{\unicdcdadad} A\_27d .  nonempty~A\_27d{\unicdbdjdcd}{\unicdcdadad} A\_27e .  \\
nonempty~A\_27e{\unicdbdjdcd}{\unicdcdadad} A\_27f .  nonempty~A\_27f{\unicdbdjdcd}{\unicdcdadad} A\_27g .  nonempty~\\
A\_27g{\unicdbdjdcd}{\unicdcdadad} A\_27h .  nonempty~A\_27h{\unicdbdjdcd}{\unicdcdadad} A\_27i .  nonempty~A\_27i{\unicdbdjdcd}\\
{\unicdcdadad} A\_27j .  nonempty~A\_27j{\unicdbdjdcd}{\unicdcdadad} A\_27k .  nonempty~A\_27k{\unicdbdjdcd}{\unicdcdadad} A\_27l .  \\
nonempty~A\_27l{\unicdbdjdcd}{\unicdcdadad} A\_27m .  nonempty~A\_27m{\unicdbdjdcd}{\unicdcdadad} A\_27n .  nonempty~\\
A\_27n{\unicdbdjdcd}{\unicdcdadad} A\_27o .  nonempty~A\_27o{\unicdbdjdcd}{\unicdcdadad} A\_27p .  nonempty~A\_27p{\unicdbdjdcd}\\
{\unicdcdadad} A\_27q .  nonempty~A\_27q{\unicdbdjdcd}{\unicdcdadad} A\_27r .  nonempty~A\_27r{\unicdbdjdcd}{\unicdcdadad} A\_27s .  \\
nonempty~A\_27s{\unicdbdjdcd}{\unicdcdadad} A\_27t .  nonempty~A\_27t{\unicdbdjdcd}{\unicdcdadad} A\_27u .  nonempty~\\
A\_27u{\unicdbdjdcd}{\unicdcdadad} A\_27v .  nonempty~A\_27v{\unicdbdjdcd}{\unicdcdadad} A\_27w .  nonempty~A\_27w{\unicdbdjdcd}\\
{\unicdcdadad} A\_27x .  nonempty~A\_27x{\unicdbdjdcd}{\unicdcdadad} A\_27y .  nonempty~A\_27y{\unicdbdjdcd}{\unicdcdadad} A\_27z .  \\
nonempty~A\_27z{\unicdbdjdcd}(({\unicdcdadad} V0x \in ty\_2Enum\_2Enum .  (p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V0x)))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V1x \in ty\_2Enum\_2Enum .  (p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27b)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27b)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V1x))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V2x \in ty\_2Enum\_2Enum .  (p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27c)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27c)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V2x)))))){\unicdcdcdhd}(({\unicdcdadad} V3x \in ty\_2Enum\_2Enum .  \\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27d)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27d)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27d)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V3x))))))))){\unicdcdcdhd}(({\unicdcdadad} V4x \in ty\_2Enum\_2Enum .  \\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27e)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~\\
A\_27e)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27e)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V4x)))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V5x \in ty\_2Enum\_2Enum .  (p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27f)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(\mname{c\_2Ewords\_2Eword\_\_2comp}~A\_27f)~\\
(ap~(\mname{c\_2Ewords\_2En2w}~A\_27f)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT2}~V5x))))))){\unicdcdcdhd}(({\unicdcdadad} V6x \in A\_27g .  ({\unicdcdadad} V7y \in \\
(ty\_2Efcp\_2Ecart~2~A\_27h) .  ({\unicdcdadad} V8f \in (ty\_2Enum\_2Enum^{{A\_27g}}) .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27h)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27h)~V7y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27h)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V8f~V6x))))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27h)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27h)~V7y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27h)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V9x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V10y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27i) .  ({\unicdcdadad} V11f \in A\_27j .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27i)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27i)~V10y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27i)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V9x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27i)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27i)~V10y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27i)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}(({\unicdcdadad} V12x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V13y \in (ty\_2Efcp\_2Ecart~2~A\_27k) .  ({\unicdcdadad} V14f \in A\_27l .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27k)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27k)~V13y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27k)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V12x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27k)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27k)~V13y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27k)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}(({\unicdcdadad} V15x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V16y \in (ty\_2Efcp\_2Ecart~2~A\_27m) .  ({\unicdcdadad} V17f \in A\_27n .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27m)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27m)~V16y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27m)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V15x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27m)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27m)~V16y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27m)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V18x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V19y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27o) .  ({\unicdcdadad} V20f \in A\_27p .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27o)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27o)~V19y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27o)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V18x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27o)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V19y)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V21x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V22y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27q) .  ({\unicdcdadad} V23f \in A\_27r .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27q)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27q)~V22y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27q)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V21x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27q)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27q)~V22y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27q)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}(({\unicdcdadad} V24x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V25y \in (ty\_2Efcp\_2Ecart~2~A\_27s) .  ({\unicdcdadad} V26f \in A\_27t .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27s)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27s)~V25y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27s)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V24x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27s)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27s)~V25y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27s)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}(({\unicdcdadad} V27x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V28y \in (ty\_2Efcp\_2Ecart~2~A\_27u) .  ({\unicdcdadad} V29f \in A\_27v .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27u)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27u)~V28y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27u)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V27x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27u)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27u)~V28y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27u)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V30x \in A\_27w .  ({\unicdcdadad} V31y \in (ty\_2Efcp\_2Ecart~2~A\_27x) .  \\
({\unicdcdadad} V32f \in (ty\_2Enum\_2Enum^{{A\_27w}}) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27x)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27x)~V31y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27x)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V32f~V30x))))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27x)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27x)~V31y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27x)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V33x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V34y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27y) .  ({\unicdcdadad} V35f \in A\_27z .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27y)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27y)~V34y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27y)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V33x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27y)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27y)~V34y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27y)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}(({\unicdcdadad} V36x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V37y \in (ty\_2Efcp\_2Ecart~2~A\_27a0) .  ({\unicdcdadad} V38f \in A\_27a1 .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a0)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a0)~V37y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a0)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V36x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a0)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a0)~V37y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a0)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}(({\unicdcdadad} V39x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V40y \in (ty\_2Efcp\_2Ecart~2~A\_27a2) .  ({\unicdcdadad} V41f \in A\_27a3 .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a2)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a2)~V40y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a2)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V39x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a2)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a2)~V40y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a2)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V42x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V43y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a4) .  ({\unicdcdadad} V44f \in A\_27a5 .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a4)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a4)~V43y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a4)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V42x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a4)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V43y)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V45x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V46y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a6) .  ({\unicdcdadad} V47f \in A\_27a7 .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a6)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a6)~V46y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a6)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V45x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a6)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~(ap~(ap~\\
(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a6)~V46y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a6)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}(({\unicdcdadad} V48x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V49y \in (ty\_2Efcp\_2Ecart~2~A\_27a8) .  ({\unicdcdadad} V50f \in A\_27a9 .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a8)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a8)~V49y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a8)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~V48x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a8)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a8)~V49y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a8)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}(({\unicdcdadad} V51x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V52y \in (ty\_2Efcp\_2Ecart~2~A\_27a10) .  ({\unicdcdadad} V53f \in A\_27a11 .  \\
((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a10)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a10)~V52y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a10)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V51x)))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a10)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a10)~V52y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a10)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V54x \in A\_27a12 .  ({\unicdcdadad} V55y \in (ty\_2Efcp\_2Ecart~2~A\_27a13) .  \\
({\unicdcdadad} V56f \in (ty\_2Enum\_2Enum^{{A\_27a12}}) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a13)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a13)~\\
V55y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a13)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V56f~\\
V54x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a13)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a13)~V55y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a13)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V57x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V58y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a14) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a14)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a14)~V58y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a14)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V57x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a14)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a14)~\\
V58y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a14)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V59x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V60y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a15) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a15)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a15)~V60y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a15)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V59x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a15)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~V60y))))){\unicdcdcdhd}(({\unicdcdadad} V61x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V62y \in (ty\_2Efcp\_2Ecart~2~A\_27a16) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a16)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a16)~\\
V62y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a16)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V61x))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a16)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a16)~V62y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a16)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V63x \in A\_27a17 .  ({\unicdcdadad} V64y \in (ty\_2Efcp\_2Ecart~2~A\_27a18) .  \\
({\unicdcdadad} V65f \in (ty\_2Enum\_2Enum^{{A\_27a17}}) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a18)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a18)~\\
V64y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a18)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V65f~\\
V63x)))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a18)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a18)~V64y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a18)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V66x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V67y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a19) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a19)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a19)~V67y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a19)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~V66x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a19)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a19)~\\
V67y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a19)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V68x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V69y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a20) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a20)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a20)~V69y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a20)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~V68x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a20)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~V69y))))){\unicdcdcdhd}(({\unicdcdadad} V70x \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V71y \in (ty\_2Efcp\_2Ecart~2~A\_27a21) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a21)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a21)~\\
V71y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a21)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~V70x))))))){\unicdbdjded}\\
(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a21)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\\
\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a21)~V71y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a21)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V72x \in A\_27a22 .  ({\unicdcdadad} V73y \in (ty\_2Efcp\_2Ecart~2~A\_27a23) .  \\
({\unicdcdadad} V74f \in (ty\_2Enum\_2Enum^{{A\_27a22}}) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a23)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a23)~\\
V73y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a23)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V74f~V72x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a23)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a23)~\\
V73y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a23)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V75x \in A\_27a24 .  ({\unicdcdadad} V76y \in (ty\_2Efcp\_2Ecart~2~A\_27a25) .  \\
({\unicdcdadad} V77f \in (ty\_2Enum\_2Enum^{{A\_27a24}}) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a25)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a25)~\\
V76y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a25)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~(ap~V77f~V75x))))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~\\
A\_27a25)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a25)~\\
V76y)~(ap~(\mname{c\_2Ewords\_2En2w}~A\_27a25)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V78x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V79y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a26) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a26)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_add}~A\_27a26)~V79y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a26)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V78x)))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a26)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V79y))))){\unicdcdcdhd}\\
({\unicdcdadad} V80x \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V81y \in (ty\_2Efcp\_2Ecart~\\
2~A\_27a27) .  ((p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a27)~(ap~\\
\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~\\
(ap~(ap~(\mname{c\_2Ewords\_2Eword\_\_sub}~A\_27a27)~V81y)~(ap~(\mname{c\_2Ewords\_2En2w}~\\
A\_27a27)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT2}~\\
V80x)))))){\unicdbdjded}(p~(ap~(ap~(\mname{c\_2Ealignment\_2Ealigned}~A\_27a27)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V81y))))))))))))))))))))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
