\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\_2Efrac\_2EFRAC\_\_ADD\_\_ASSOC (TMFgKoJYpKnnyC32Khasga8JYwtXZigd66Z)}
\maketitle
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfddee}
We define $\mname{c\_2Emin\_2E\_3D}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} x \in {A} .  {{\uniddcgcg} y \in {A} .  {{inj\_\_o}~{({{x}={y}})}}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfeef}
We define $\mname{c\_2Ebool\_2ET}$ to be ${({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{2}}})}})}}~{({{\uniddcgcg} V0x \in {2} .  {V0x}})}})}}~{({{\uniddcgcg} V1x \in {2} .  {V1x}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdbd}
We define $\mname{c\_2Ebool\_2E\_21}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{A\_27a}}})}})}}~{V0P}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {\mname{c\_2Ebool\_2ET}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def: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}
Let $ ty\_2Einteger\_2Eint : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Einteger\_2Eint}}\label{hyp:ogfgpfehjhpfcdfejgogehfghgfgchpfcdfejgogeh}
\end{equation}
Let $ ty\_2Epair\_2Eprod : {{\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\_2Epair\_2Eprod~\\
A0~A1)\end{array}
\label{hyp:ogfgpfehjhpfcdfeahbgjgchpfcdfeahchpgeg}
\end{equation}
Let $ ty\_2Efrac\_2Efrac : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Efrac\_2Efrac}}\label{hyp:ogfgpfehjhpfcdfeggchbgdgpfcdfeggchbgdg}
\end{equation}
Let $ c\_2Efrac\_2Erep\_\_frac : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Efrac\_2Erep\_\_frac \in ((ty\_2Epair\_2Eprod~ty\_2Einteger\_2Eint~\\
ty\_2Einteger\_2Eint)^{{ty\_2Efrac\_2Efrac}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeggchbgdgpfcdfechfgahpfpfggchbgdg}
\end{equation}
Let $ c\_2Epair\_2ESND : {{\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\_2Epair\_2ESND~\\
A\_27a~A\_27b \in (A\_27b^{{({{{ty\_2Epair\_2Eprod}~{A\_27a}}~{A\_27b}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfedfoeee}
\end{equation}
\begin{definition}\label{def:dgpfcdfeggchbgdgpfcdfeggchbgdgpfpfegogng}
We define $\mname{c\_2Efrac\_2Efrac\_\_dnm}$ to be ${{\uniddcgcg} V0f \in {ty\_2Efrac\_2Efrac} .  {({{{ap}~{({{{c\_2Epair\_2ESND}~{ty\_2Einteger\_2Eint}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{c\_2Efrac\_2Erep\_\_frac}}~{V0f}})}})}}$.
\end{definition}
Let $ ty\_2Enum\_2Enum : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Enum\_2Enum}}\label{hyp:ogfgpfehjhpfcdfeogfhngpfcdfeogfhng}
\end{equation}
Let $ c\_2Einteger\_2Eint\_\_REP\_\_CLASS : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Eint\_\_REP\_\_CLASS \in ((2^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})^{{ty\_2Einteger\_2Eint}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfejgogehpfpfcffeafpfpfdemebedfdf}
\end{equation}
\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:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfcffeaf}
We define $\mname{c\_2Einteger\_2Eint\_\_REP}$ to be ${{\uniddcgcg} V0a \in {ty\_2Einteger\_2Eint} .  {({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})}}~{({{{ap}~{c\_2Einteger\_2Eint\_\_REP\_\_CLASS}}~{V0a}})}})}}$.
\end{definition}
Let $ c\_2Einteger\_2Etint\_\_mul : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Etint\_\_mul \in (((ty\_2Epair\_2Eprod~ty\_2Enum\_2Enum~\\
ty\_2Enum\_2Enum)^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfngfhmg}
\end{equation}
Let $ c\_2Einteger\_2Etint\_\_eq : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Etint\_\_eq \in ((2^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpffgbh}
\end{equation}
Let $ c\_2Einteger\_2Eint\_\_ABS\_\_CLASS : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Eint\_\_ABS\_\_CLASS \in (ty\_2Einteger\_2Eint^{{({{2}^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfejgogehpfpfbecedfpfpfdemebedfdf}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfbecedf}
We define $\mname{c\_2Einteger\_2Eint\_\_ABS}$ to be ${{\uniddcgcg} V0r \in {({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})} .  {({{{ap}~{c\_2Einteger\_2Eint\_\_ABS\_\_CLASS}}~{({{{ap}~{c\_2Einteger\_2Etint\_\_eq}}~{V0r}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfngfhmg}
We define $\mname{c\_2Einteger\_2Eint\_\_mul}$ to be ${{\uniddcgcg} V0T1 \in {ty\_2Einteger\_2Eint} .  {{\uniddcgcg} V1T2 \in {ty\_2Einteger\_2Eint} .  {({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_ABS}}}~{({{{ap}~{({{{ap}~{c\_2Einteger\_2Etint\_\_mul}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V0T1}})}})}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V1T2}})}})}})}}}$.
\end{definition}
Let $ c\_2Epair\_2EFST : {{\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\_2Epair\_2EFST~\\
A\_27a~A\_27b \in (A\_27a^{{({{{ty\_2Epair\_2Eprod}~{A\_27a}}~{A\_27b}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfegedfef}
\end{equation}
\begin{definition}\label{def:dgpfcdfeggchbgdgpfcdfeggchbgdgpfpfogngch}
We define $\mname{c\_2Efrac\_2Efrac\_\_nmr}$ to be ${{\uniddcgcg} V0f \in {ty\_2Efrac\_2Efrac} .  {({{{ap}~{({{{c\_2Epair\_2EFST}~{ty\_2Einteger\_2Eint}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{c\_2Efrac\_2Erep\_\_frac}}~{V0f}})}})}}$.
\end{definition}
Let $ c\_2Einteger\_2Etint\_\_add : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Etint\_\_add \in (((ty\_2Epair\_2Eprod~ty\_2Enum\_2Enum~\\
ty\_2Enum\_2Enum)^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfbgegeg}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfbgegeg}
We define $\mname{c\_2Einteger\_2Eint\_\_add}$ to be ${{\uniddcgcg} V0T1 \in {ty\_2Einteger\_2Eint} .  {{\uniddcgcg} V1T2 \in {ty\_2Einteger\_2Eint} .  {({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_ABS}}}~{({{{ap}~{({{{ap}~{c\_2Einteger\_2Etint\_\_add}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V0T1}})}})}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V1T2}})}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdgepffdde}
We define $\mname{c\_2Ebool\_2E\_2F\_5C}$ to be ${({{\uniddcgcg} V0t1 \in {2} .  {({{\uniddcgcg} V1t2 \in {2} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V2t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t1}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V1t2}})}}~{V2t}})}})}})}}~{V2t}})}})}})}})}})}$.
\end{definition}
Let $ c\_2Epair\_2EABS\_\_prod : {{\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\_2Epair\_2EABS\_\_prod~\\
A\_27a~A\_27b \in ((ty\_2Epair\_2Eprod~A\_27a~A\_27b)^{{({{({{2}^{{A\_27b}}})}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfebecedfpfpfahchpgeg}
\end{equation}
\begin{definition}\label{def:dgpfcdfeahbgjgchpfcdfepfcdde}
We define $\mname{c\_2Epair\_2E\_2C}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} V0x \in {A\_27a} .  {{\uniddcgcg} V1y \in {A\_27b} .  {({{{ap}~{({{{c\_2Epair\_2EABS\_\_prod}~{A\_27a}}~{A\_27b}})}}~{({{\uniddcgcg} V2a \in {A\_27a} .  {({{\uniddcgcg} V3b \in {A\_27b} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V2a}})}}~{V0x}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27b}})}}~{V3b}})}}~{V1y}})}})}})}})}})}}}}}$.
\end{definition}
Let $ c\_2Efrac\_2Eabs\_\_frac : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Efrac\_2Eabs\_\_frac \in (ty\_2Efrac\_2Efrac^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Einteger\_2Eint}}~{ty\_2Einteger\_2Eint}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeggchbgdgpfcdfebgcgdhpfpfggchbgdg}
\end{equation}
\begin{definition}\label{def:dgpfcdfeggchbgdgpfcdfeggchbgdgpfpfbgegeg}
We define $\mname{c\_2Efrac\_2Efrac\_\_add}$ to be ${{\uniddcgcg} V0f1 \in {ty\_2Efrac\_2Efrac} .  {{\uniddcgcg} V1f2 \in {ty\_2Efrac\_2Efrac} .  {({{{ap}~{c\_2Efrac\_2Eabs\_\_frac}}~{({{{ap}~{({{{ap}~{({{{\mname{c\_2Epair\_2E\_2C}}~{ty\_2Einteger\_2Eint}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_add}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_mul}}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_nmr}}}~{V0f1}})}})}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_dnm}}}~{V1f2}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_mul}}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_nmr}}}~{V1f2}})}})}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_dnm}}}~{V0f1}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_mul}}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_dnm}}}~{V0f1}})}})}}~{({{{ap}~{\mname{c\_2Efrac\_2Efrac\_\_dnm}}}~{V1f2}})}})}})}})}}}$.
\end{definition}
Let $ c\_2Einteger\_2Eint\_\_of\_\_num : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Einteger\_2Eint\_\_of\_\_num} \in {({{ty\_2Einteger\_2Eint}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfejgogehpfpfpgggpfpfogfhng}
\end{equation}
Let $ c\_2Einteger\_2Etint\_\_lt : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Etint\_\_lt \in ((2^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfmgeh}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfmgeh}
We define $\mname{c\_2Einteger\_2Eint\_\_lt}$ to be ${{\uniddcgcg} V0T1 \in {ty\_2Einteger\_2Eint} .  {{\uniddcgcg} V1T2 \in {ty\_2Einteger\_2Eint} .  {({{{ap}~{({{{ap}~{c\_2Einteger\_2Etint\_\_lt}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V0T1}})}})}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V1T2}})}})}}}$.
\end{definition}
Let $ c\_2Einteger\_2Etint\_\_neg : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Einteger\_2Etint\_\_neg \in ((ty\_2Epair\_2Eprod~ty\_2Enum\_2Enum~\\
ty\_2Enum\_2Enum)^{{({{{ty\_2Epair\_2Eprod}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfogfghg}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfogfghg}
We define $\mname{c\_2Einteger\_2Eint\_\_neg}$ to be ${{\uniddcgcg} V0T1 \in {ty\_2Einteger\_2Eint} .  {({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_ABS}}}~{({{{ap}~{c\_2Einteger\_2Etint\_\_neg}}~{({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_REP}}}~{V0T1}})}})}})}}$.
\end{definition}
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 $ 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: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: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}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfbd}
We define $\mname{c\_2Einteger\_2Etint\_\_1}$ to be ${({{{ap}~{({{{ap}~{({{{\mname{c\_2Epair\_2E\_2C}}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfbd}
We define $\mname{c\_2Einteger\_2Eint\_\_1}$ to be ${({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_ABS}}}~{\mname{c\_2Einteger\_2Etint\_\_1}}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfeehjgogehpfpfad}
We define $\mname{c\_2Einteger\_2Etint\_\_0}$ to be ${({{{ap}~{({{{ap}~{({{{\mname{c\_2Epair\_2E\_2C}}~{ty\_2Enum\_2Enum}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchpfcdfejgogehpfpfad}
We define $\mname{c\_2Einteger\_2Eint\_\_0}$ to be ${({{{ap}~{\mname{c\_2Einteger\_2Eint\_\_ABS}}}~{\mname{c\_2Einteger\_2Etint\_\_0}}})}$.
\end{definition}
Let $ ty\_2Ering\_2Ering : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Ering\_2Ering}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfechjgoghgpfcdfechjgoghg}
\end{equation}
Let $ c\_2Ering\_2Erecordtype\_2Ering : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Erecordtype\_2Ering~\\
A\_27a \in ((((((ty\_2Ering\_2Ering~A\_27a)^{{({{A\_27a}^{{A\_27a}}})}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}})^{{A\_27a}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechfgdgpgchegehjhahfgpfcdfechjgoghg}
\end{equation}
Let $ ty\_2Ecanonical\_2Ecanonical\_\_sum : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A0 .  nonempty~A0{\unicdbdjdcd}nonempty~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A0)\end{array}
\label{hyp:ogfgpfehjhpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhng}
\end{equation}
Let $ ty\_2EringNorm\_2Epolynom : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2EringNorm\_2Epolynom}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfechjgoghgoepgchngpfcdfeahpgmgjhogpgng}
\end{equation}
Let $ c\_2EringNorm\_2Epolynom\_\_normalize : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2Epolynom\_\_normalize~\\
A\_27a \in (((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeahpgmgjhogpgngpfpfogpgchngbgmgjgkhfg}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfahpgmgjhogpgngpfpfogpgchngbgmgjgkhfg}
We define $\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}$ to be ${({{{ap}~{({{c\_2EringNorm\_2Epolynom\_\_normalize}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ering\_2Ering\_\_RM : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RM~A\_27a \in (((\\
A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfne}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RP : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RP~A\_27a \in (((\\
A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfaf}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R1~A\_27a \in (A\_27a^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfbd}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R0 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R0~A\_27a \in (A\_27a^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfad}
\end{equation}
Let $ ty\_2Esemi\_\_ring\_2Esemi\_\_ring : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghg}
\end{equation}
Let $ c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~\\
A\_27a \in (((((ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a)^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}})^{{A\_27a}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfgngjgpfpfchjgoghgpfcdfechfgdgpgchegehjhahfgpfcdfedhfgngjgpfpfchjgoghg}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfpggg}
We define $\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{A\_27a}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_R0}~{A\_27a}})}}~{V0r}})}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_R1}~{A\_27a}})}}~{V0r}})}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
Let $ ty\_2Equote\_2Evarmap : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Equote\_2Evarmap}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfebhfhpgehfgpfcdfeghbgchngbgah}
\end{equation}
Let $ c\_2Ecanonical\_2Eics\_\_aux : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Eics\_\_aux~A\_27a \in \\
((((A\_27a^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{A\_27a}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgdgdhpfpfbgfhih}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfjgdgdhpfpfbgfhih}
We define $\mname{c\_2EringNorm\_2Er\_\_ics\_\_aux}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Eics\_\_aux}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfjgdgdhpfpfbgfhih}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_ics\_\_aux}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ ty\_2Equote\_2Eindex : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Equote\_2Eindex}}\label{hyp:ogfgpfehjhpfcdfebhfhpgehfgpfcdfejgogegfgih}
\end{equation}
Let $ ty\_2Elist\_2Elist : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Elist\_2Elist}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfemgjgdhehpfcdfemgjgdheh}
\end{equation}
Let $ c\_2Ecanonical\_2Einterp\_\_m : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Einterp\_\_m~A\_27a \in \\
((((A\_27a^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{A\_27a}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfng}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfjgogehfgchahpfpfng}
We define $\mname{c\_2EringNorm\_2Er\_\_interp\_\_m}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_m}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfjgogehfgchahpfpfng}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_m}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_interp\_\_m}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Einterp\_\_vl : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Einterp\_\_vl~A\_27a \in \\
(((A\_27a^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfghmg}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfjgogehfgchahpfpfghmg}
We define $\mname{c\_2EringNorm\_2Er\_\_interp\_\_vl}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_vl}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfjgogehfgchahpfpfghmg}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_vl}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_interp\_\_vl}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Eivl\_\_aux : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Eivl\_\_aux~A\_27a \in \\
((((A\_27a^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{ty\_2Equote\_2Eindex}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgghmgpfpfbgfhih}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfjgghmgpfpfbgfhih}
We define $\mname{c\_2EringNorm\_2Er\_\_ivl\_\_aux}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Eivl\_\_aux}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfjgghmgpfpfbgfhih}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_ivl\_\_aux}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~\\
A\_27a \in (((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhjgngahmgjgggjh}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_simplify}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_simplify}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~\\
A\_27a \in ((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfahchpgeg}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfahchpgeg}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_prod}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfahchpgeg}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_prod}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~\\
A\_27a \in (((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{A\_27a}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchdd}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchdd}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar3}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchdd}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar3}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~\\
A\_27a \in ((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchcd}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchcd}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar2}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchcd}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar2}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~\\
A\_27a \in ((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{A\_27a}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgch}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgch}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgch}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_scalar}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Evarlist\_\_insert : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Evarlist\_\_insert~\\
A\_27a \in ((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfeghbgchmgjgdhehpfpfjgogdhfgcheh}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfghbgchmgjgdhehpfpfjgogdhfgcheh}
We define $\mname{c\_2EringNorm\_2Er\_\_varlist\_\_insert}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Evarlist\_\_insert}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfghbgchmgjgdhehpfpfjgogdhfgcheh}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_varlist\_\_insert}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Emonom\_\_insert : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Emonom\_\_insert~\\
A\_27a \in (((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{A\_27a}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfengpgogpgngpfpfjgogdhfgcheh}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfngpgogpgngpfpfjgogdhfgcheh}
We define $\mname{c\_2EringNorm\_2Er\_\_monom\_\_insert}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Emonom\_\_insert}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfngpgogpgngpfpfjgogdhfgcheh}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_monom\_\_insert}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2ENil\_\_monom : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ENil\_\_monom~A\_27a \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfeoejgmgpfpfngpgogpgng}
\end{equation}
Let $ c\_2Ecanonical\_2ECons\_\_varlist : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ECons\_\_varlist~\\
A\_27a \in (((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedepgogdhpfpfghbgchmgjgdheh}
\end{equation}
Let $ c\_2Ecanonical\_2ECons\_\_monom : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ECons\_\_monom~A\_27a \in \\
((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{ty\_2Equote\_2Eindex}})}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedepgogdhpfpfngpgogpgng}
\end{equation}
Let $ c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a \in ((((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfngfgchhgfg}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfngfgchhgfg}
We define $\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_merge}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfngfgchhgfg}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_merge}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Equote\_2EEmpty\_\_vm : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Equote\_2EEmpty\_\_vm~A\_27a \in (\\
ty\_2Equote\_2Evarmap~A\_27a)\end{array}
\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfefengahehjhpfpfghng}
\end{equation}
Let $ c\_2Equote\_2ENode\_\_vm : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Equote\_2ENode\_\_vm~A\_27a \in ((\\
((ty\_2Equote\_2Evarmap~A\_27a)^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfeoepgegfgpfpfghng}
\end{equation}
Let $ c\_2EringNorm\_2EPopp : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2EPopp~A\_27a \in ((ty\_2EringNorm\_2Epolynom~\\
A\_27a)^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeafpgahah}
\end{equation}
Let $ c\_2EringNorm\_2EPmult : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2EPmult~A\_27a \in ((\\
(ty\_2EringNorm\_2Epolynom~A\_27a)^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeafngfhmgeh}
\end{equation}
Let $ c\_2EringNorm\_2EPplus : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2EPplus~A\_27a \in ((\\
(ty\_2EringNorm\_2Epolynom~A\_27a)^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeafahmgfhdh}
\end{equation}
Let $ c\_2Equote\_2Evarmap\_\_find : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Equote\_2Evarmap\_\_find~A\_27a \in \\
((A\_27a^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{ty\_2Equote\_2Eindex}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfeghbgchngbgahpfpfggjgogeg}
\end{equation}
Let $ c\_2EringNorm\_2EPvar : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2EPvar~A\_27a \in ((ty\_2EringNorm\_2Epolynom~\\
A\_27a)^{{ty\_2Equote\_2Eindex}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeafghbgch}
\end{equation}
Let $ c\_2EringNorm\_2EPconst : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2EPconst~A\_27a \in (\\
(ty\_2EringNorm\_2Epolynom~A\_27a)^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfeafdgpgogdheh}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfeahpgmgjhogpgngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EringNorm\_2Epolynom\_\_simplify}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {{\uniddcgcg} V1x \in {({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_canonical\_\_sum\_\_simplify}}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{c\_2EringNorm\_2Epolynom\_\_normalize}~{A\_27a}})}}~{V0r}})}}~{V1x}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfahpgmgjhogpgngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_simplify}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Epolynom\_\_simplify}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Einterp\_\_cs : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Einterp\_\_cs~A\_27a \in \\
(((A\_27a^{{({{ty\_2Ecanonical\_2Ecanonical\_\_sum}~{A\_27a}})}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfdgdh}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgoepgchngpfcdfechpfpfjgogehfgchahpfpfdgdh}
We define $\mname{c\_2EringNorm\_2Er\_\_interp\_\_cs}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_cs}~{A\_27a}})}}~{({{{ap}~{({{\mname{c\_2Ering\_2Esemi\_\_ring\_\_of}}~{A\_27a}})}}~{V0r}})}})}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchpfpfjgogehfgchahpfpfdgdh}
We define $\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_cs}$ to be ${({{{ap}~{({{\mname{c\_2EringNorm\_2Er\_\_interp\_\_cs}}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2EringNorm\_2Einterp\_\_p : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EringNorm\_2Einterp\_\_p~A\_27a \in \\
(((A\_27a^{{({{ty\_2EringNorm\_2Epolynom}~{A\_27a}})}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgoepgchngpfcdfejgogehfgchahpfpfah}
\end{equation}
\begin{definition}\label{def:dgpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfjgogehfgchahpfpfah}
We define $\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}$ to be ${({{{ap}~{({{c\_2EringNorm\_2Einterp\_\_p}~{ty\_2Einteger\_2Eint}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Erecordtype\_2Ering}~{ty\_2Einteger\_2Eint}})}}~{\mname{c\_2Einteger\_2Eint\_\_0}}})}}~{\mname{c\_2Einteger\_2Eint\_\_1}}})}}~{\mname{c\_2Einteger\_2Eint\_\_add}}})}}~{\mname{c\_2Einteger\_2Eint\_\_mul}}})}}~{\mname{c\_2Einteger\_2Eint\_\_neg}}})}})}$.
\end{definition}
Let $ c\_2Ering\_2Ering\_\_RN : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RN~A\_27a \in ((A\_27a^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfoe}
\end{equation}
\begin{definition}\label{def:dgpfcdfechjgoghgpfcdfejgdhpfpfchjgoghg}
We define $\mname{c\_2Ering\_2Eis\_\_ring}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Ering\_2Ering}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V1n \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V2m \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V1n}})}}~{V2m}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V2m}})}}~{V1n}})}})}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V3n \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V4m \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V5p \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V3n}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V4m}})}}~{V5p}})}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V3n}})}}~{V4m}})}})}}~{V5p}})}})}})}})}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V6n \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V7m \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V6n}})}}~{V7m}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V7m}})}}~{V6n}})}})}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V8n \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V9m \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V10p \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V8n}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V9m}})}}~{V10p}})}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V8n}})}}~{V9m}})}})}}~{V10p}})}})}})}})}})}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V11n \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_R0}~{A\_27a}})}}~{V0r}})}})}}~{V11n}})}})}}~{V11n}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V12n \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_R1}~{A\_27a}})}}~{V0r}})}})}}~{V12n}})}})}}~{V12n}})}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V13n \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V13n}})}}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RN}~{A\_27a}})}}~{V0r}})}}~{V13n}})}})}})}}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_R0}~{A\_27a}})}}~{V0r}})}})}})}})}})}}~{({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V14n \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V15m \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{A\_27a}})}}~{({{\uniddcgcg} V16p \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{V14n}})}}~{V15m}})}})}}~{V16p}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V14n}})}}~{V16p}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Ering\_2Ering\_\_RM}~{A\_27a}})}}~{V0r}})}}~{V15m}})}}~{V16p}})}})}})}})}})}})}})}})}})}})}})}})}})}})}})}})}}}$.
\end{definition}
Let $ c\_2Equote\_2ERight\_\_idx : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Equote\_2ERight\_\_idx} \in {({{ty\_2Equote\_2Eindex}^{{ty\_2Equote\_2Eindex}}})}}\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfecfjghgigehpfpfjgegih}
\end{equation}
Let $ c\_2Equote\_2ELeft\_\_idx : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Equote\_2ELeft\_\_idx} \in {({{ty\_2Equote\_2Eindex}^{{ty\_2Equote\_2Eindex}}})}}\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfemefgggehpfpfjgegih}
\end{equation}
Let $ c\_2Equote\_2EEnd\_\_idx : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Equote\_2EEnd\_\_idx} \in {ty\_2Equote\_2Eindex}}\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfefeogegpfpfjgegih}
\end{equation}
Let $ ty\_2EternaryComparisons\_2Eordering : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2EternaryComparisons\_2Eordering}}\label{hyp:ogfgpfehjhpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghg}
\end{equation}
Let $ c\_2Equote\_2Eindex\_\_compare : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Equote\_2Eindex\_\_compare \in ((ty\_2EternaryComparisons\_2Eordering^{{ty\_2Equote\_2Eindex}})^{{ty\_2Equote\_2Eindex}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebhfhpgehfgpfcdfejgogegfgihpfpfdgpgngahbgchfg}
\end{equation}
Let $ c\_2EternaryComparisons\_2ELESS : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2EternaryComparisons\_2ELESS} \in {ty\_2EternaryComparisons\_2Eordering}}\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfemefedfdf}
\end{equation}
\begin{definition}\label{def:dgpfcdfebhfhpgehfgpfcdfejgogegfgihpfpfmgeh}
We define $\mname{c\_2Equote\_2Eindex\_\_lt}$ to be ${{\uniddcgcg} V0i1 \in {ty\_2Equote\_2Eindex} .  {{\uniddcgcg} V1i2 \in {ty\_2Equote\_2Eindex} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2EternaryComparisons\_2Eordering}})}}~{({{{ap}~{({{{ap}~{c\_2Equote\_2Eindex\_\_compare}}~{V0i1}})}}~{V1i2}})}})}}~{c\_2EternaryComparisons\_2ELESS}})}}}$.
\end{definition}
Let $ c\_2EternaryComparisons\_2Enum2ordering : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2EternaryComparisons\_2Enum2ordering \in (ty\_2EternaryComparisons\_2Eordering^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfeogfhngcdpgchegfgchjgoghg}
\end{equation}
\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\_2EternaryComparisons\_2Eordering2num : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2EternaryComparisons\_2Eordering2num \in (ty\_2Enum\_2Enum^{{ty\_2EternaryComparisons\_2Eordering}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghgcdogfhng}
\end{equation}
\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: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:dgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghgpfpfdebedffe}
We define $\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0x \in {ty\_2EternaryComparisons\_2Eordering} .  {{\uniddcgcg} V1v0 \in {A\_27a} .  {{\uniddcgcg} V2v1 \in {A\_27a} .  {{\uniddcgcg} V3v2 \in {A\_27a} .  {({{{ap}~{({{\uniddcgcg} V4m \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Eprim\_\_rec\_2E\_3C}}}~{V4m}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}})}}~{V1v0}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{A\_27a}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{ty\_2Enum\_2Enum}})}}~{V4m}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}})}}~{V2v1}})}}~{V3v2}})}})}})}}~{({{{ap}~{c\_2EternaryComparisons\_2Eordering2num}}~{V0x}})}})}}}}}}$.
\end{definition}
Let $ c\_2EternaryComparisons\_2EGREATER : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2EternaryComparisons\_2EGREATER \in ty\_2EternaryComparisons\_2Eordering\end{array}
\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfehecffebeeffecf}
\end{equation}
Let $ c\_2EternaryComparisons\_2EEQUAL : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2EternaryComparisons\_2EEQUAL} \in {ty\_2EternaryComparisons\_2Eordering}}\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfefebfffbeme}
\end{equation}
Let $ c\_2EternaryComparisons\_2Elist\_\_compare : {{\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\_2EternaryComparisons\_2Elist\_\_compare~\\
A\_27a~A\_27b \in (((ty\_2EternaryComparisons\_2Eordering^{{({{ty\_2Elist\_2Elist}~{A\_27b}})}})^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{({{({{ty\_2EternaryComparisons\_2Eordering}^{{A\_27b}}})}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfemgjgdhehpfpfdgpgngahbgchfg}
\end{equation}
Let $ c\_2Elist\_2ECONS : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2ECONS~A\_27a \in (((ty\_2Elist\_2Elist~\\
A\_27a)^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfedepeoedf}
\end{equation}
Let $ c\_2Elist\_2ENIL : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2ENIL~A\_27a \in (ty\_2Elist\_2Elist~\\
A\_27a)\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfeoejeme}
\end{equation}
Let $ c\_2EternaryComparisons\_2Elist\_\_merge : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a \in ((((ty\_2Elist\_2Elist~A\_27a)^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{({{({{2}^{{A\_27a}}})}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfemgjgdhehpfpfngfgchhgfg}
\end{equation}
Assume the following.
\begin{equation}
{True}\label{hyp:ehigngpfcdfecgpgpgmgpfcdfeefcfffefie}
\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} 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}
\begin{array}{c}({\unicdcdadad} V0f \in ty\_2Efrac\_2Efrac .  (p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~\\
(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\mname{c\_2Enum\_2E0}))~(ap~\mname{c\_2Efrac\_2Efrac\_\_dnm}~\\
V0f))))\end{array}
\label{hyp:ehigngpfcdfeggchbgdgpfcdfegecfbedepfpfeeoeneafpedf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0a \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V1b \in ty\_2Einteger\_2Eint .  \\
((p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\\
\mname{c\_2Enum\_2E0}))~V1b)){\unicdbdjdcd}((ap~\mname{c\_2Efrac\_2Efrac\_\_nmr}~(ap~c\_2Efrac\_2Eabs\_\_frac~\\
(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~ty\_2Einteger\_2Eint~ty\_2Einteger\_2Eint)~\\
V0a)~V1b)))=V0a))))\end{array}
\label{hyp:ehigngpfcdfeggchbgdgpfcdfeoenecf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0a \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V1b \in ty\_2Einteger\_2Eint .  \\
((p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\\
\mname{c\_2Enum\_2E0}))~V1b)){\unicdbdjdcd}((ap~\mname{c\_2Efrac\_2Efrac\_\_dnm}~(ap~c\_2Efrac\_2Eabs\_\_frac~\\
(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~ty\_2Einteger\_2Eint~ty\_2Einteger\_2Eint)~\\
V0a)~V1b)))=V1b))))\end{array}
\label{hyp:ehigngpfcdfeggchbgdgpfcdfeeeoene}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}({\unicdcdadad} V0a \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V1b \in ty\_2Einteger\_2Eint .  \\
((p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\\
\mname{c\_2Enum\_2E0}))~V0a)){\unicdbdjdcd}((p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\\
\mname{c\_2Enum\_2E0}))~V1b)){\unicdbdjdcd}(p~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_lt}~(ap~c\_2Einteger\_2Eint\_\_of\_\_num~\\
\mname{c\_2Enum\_2E0}))~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~V0a)~V1b)))))))\end{array}
\label{hyp:ehigngpfcdfejgogehfeihehfgogdhjgpgogpfcdfejeoeefpfpfneffmepfpfafpedfpfpfdfjeheoe}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}((p~(ap~(\mname{c\_2Ering\_2Eis\_\_ring}~ty\_2Einteger\_2Eint)~\\
(ap~(ap~(ap~(ap~(ap~(c\_2Ering\_2Erecordtype\_2Ering~ty\_2Einteger\_2Eint)~\\
\mname{c\_2Einteger\_2Eint\_\_0})~\mname{c\_2Einteger\_2Eint\_\_1})~\mname{c\_2Einteger\_2Eint\_\_add})~\\
\mname{c\_2Einteger\_2Eint\_\_mul})~\mname{c\_2Einteger\_2Eint\_\_neg}))){\unicdcdcdhd}(({\unicdcdadad} V0vm \in \\
(ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V1p \in (ty\_2EringNorm\_2Epolynom~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~\\
V0vm)~V1p)=(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_cs}~V0vm)~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_simplify}~V1p))))){\unicdcdcdhd}(((\\
({\unicdcdadad} V2vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V3c \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~\\
V2vm)~(ap~(c\_2EringNorm\_2EPconst~ty\_2Einteger\_2Eint)~V3c))=\\
V3c))){\unicdcdcdhd}(({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V5i \in ty\_2Equote\_2Eindex .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~\\
V4vm)~(ap~(c\_2EringNorm\_2EPvar~ty\_2Einteger\_2Eint)~V5i))=(ap~\\
(ap~(c\_2Equote\_2Evarmap\_\_find~ty\_2Einteger\_2Eint)~V5i)~V4vm)))){\unicdcdcdhd}\\
(({\unicdcdadad} V6vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  (\\
{\unicdcdadad} V7p1 \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V8p2 \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V6vm)~(ap~(ap~(c\_2EringNorm\_2EPplus~\\
ty\_2Einteger\_2Eint)~V7p1)~V8p2))=(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V6vm)~V7p1))~(ap~(ap~\\
\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V6vm)~V8p2)))))){\unicdcdcdhd}(({\unicdcdadad} V9vm \in \\
(ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V10p1 \in (\\
ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V11p2 \in \\
(ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~\\
V9vm)~(ap~(ap~(c\_2EringNorm\_2EPmult~ty\_2Einteger\_2Eint)~V10p1)~\\
V11p2))=(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~\\
V9vm)~V10p1))~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V9vm)~\\
V11p2)))))){\unicdcdcdhd}({\unicdcdadad} V12vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V13p1 \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V12vm)~(ap~(c\_2EringNorm\_2EPopp~\\
ty\_2Einteger\_2Eint)~V13p1))=(ap~\mname{c\_2Einteger\_2Eint\_\_neg}~(ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_interp\_\_p}~V12vm)~V13p1))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V14x \in A\_27a .  ({\unicdcdadad} V15v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V16v1 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
A\_27a)~c\_2Equote\_2EEnd\_\_idx)~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~\\
A\_27a)~V14x)~V16v1)~V15v2))=V14x)))){\unicdcdcdhd}(({\unicdcdadad} V17x \in A\_27a .  (\\
{\unicdcdadad} V18v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V19v1 \in (\\
ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V20i1 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~(ap~c\_2Equote\_2ERight\_\_idx~\\
V20i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~A\_27a)~V17x)~V19v1)~V18v2))=\\
(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V20i1)~V18v2)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V21x \in A\_27a .  ({\unicdcdadad} V22v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V23v1 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V24i1 \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~\\
(ap~c\_2Equote\_2ELeft\_\_idx~V24i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~\\
A\_27a)~V21x)~V23v1)~V22v2))=(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
A\_27a)~V24i1)~V23v1)))))){\unicdcdcdhd}({\unicdcdadad} V25i \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V25i)~(c\_2Equote\_2EEmpty\_\_vm~\\
A\_27a))=(ap~(\mname{c\_2Emin\_2E\_40}~A\_27a)~({\uniddcgcg} V26x \in A\_27a .  \mname{c\_2Ebool\_2ET})))))))){\unicdcdcdhd}\\
((({\unicdcdadad} V27t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V28t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V29l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V30l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V31c2 \in ty\_2Einteger\_2Eint .  \\
({\unicdcdadad} V32c1 \in ty\_2Einteger\_2Eint .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V32c1)~V30l1)~V28t1))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~V31c2)~V29l2)~V27t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V30l1)~V29l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V32c1)~V30l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V28t1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V31c2)~V29l2)~V27t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V32c1)~V31c2))~\\
V30l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V28t1)~V27t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V31c2)~V29l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V32c1)~V30l1)~V28t1))~V27t2)))))))))){\unicdcdcdhd}(({\unicdcdadad} V33t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V34t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V35l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V36l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V37c1 \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V37c1)~V36l1)~V34t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~V35l2)~V33t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V36l1)~V35l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V37c1)~V36l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V34t1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V35l2)~V33t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V37c1)~\mname{c\_2Einteger\_2Eint\_\_1}))~\\
V36l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V34t1)~V33t2)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V35l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V37c1)~V36l1)~V34t1))~V33t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V38t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V39t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V40l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V41l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V42c2 \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V41l1)~V39t1))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V42c2)~V40l2)~V38t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V41l1)~V40l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V41l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V39t1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V42c2)~V40l2)~V38t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~\mname{c\_2Einteger\_2Eint\_\_1})~\\
V42c2))~V41l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V39t1)~V38t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V42c2)~V40l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V41l1)~V39t1))~V38t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V43t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V44t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V45l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V46l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~V46l1)~\\
V44t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V45l2)~V43t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V46l1)~V45l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V46l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V44t1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V45l2)~V43t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~\mname{c\_2Einteger\_2Eint\_\_1})~\mname{c\_2Einteger\_2Eint\_\_1}))~\\
V46l1)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V44t1)~V43t2)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V45l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V46l1)~V44t1))~V43t2)))))))){\unicdcdcdhd}(({\unicdcdadad} V47s1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
V47s1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=V47s1)){\unicdcdcdhd}\\
(({\unicdcdadad} V48v6 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V49v5 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V50v4 \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~V50v4)~V49v5)~\\
V48v6))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V50v4)~V49v5)~V48v6))))){\unicdcdcdhd}({\unicdcdadad} V51v8 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V52v7 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~(\\
c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~V52v7)~V51v8))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~V52v7)~V51v8)))))))))){\unicdcdcdhd}((({\unicdcdadad} V53t2 \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V54l2 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V55l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V56c2 \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V57c1 \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V57c1)~V55l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V56c2)~V54l2)~V53t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V55l1)~V54l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V57c1)~V55l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V56c2)~V54l2)~V53t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V57c1)~V56c2))~\\
V55l1)~V53t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V56c2)~V54l2)~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V57c1)~V55l1)~V53t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V58t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V59l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V60l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V61c1 \in \\
ty\_2Einteger\_2Eint .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V61c1)~V60l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V59l2)~V58t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V60l1)~V59l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V61c1)~V60l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V59l2)~V58t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V61c1)~\mname{c\_2Einteger\_2Eint\_\_1}))~\\
V60l1)~V58t2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V59l2)~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~V61c1)~\\
V60l1)~V58t2)))))))){\unicdcdcdhd}({\unicdcdadad} V62l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V63c1 \in ty\_2Einteger\_2Eint .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V63c1)~V62l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V63c1)~V62l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))))))){\unicdcdcdhd}\\
((({\unicdcdadad} V64t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V65l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V66l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V67c2 \in ty\_2Einteger\_2Eint .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~V66l1)~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V67c2)~V65l2)~V64t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V66l1)~V65l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V66l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V67c2)~V65l2)~V64t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~\mname{c\_2Einteger\_2Eint\_\_1})~\\
V67c2))~V66l1)~V64t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~V67c2)~V65l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~\\
V66l1)~V64t2)))))))){\unicdcdcdhd}(({\unicdcdadad} V68t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V69l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V70l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~V70l1)~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~V69l2)~\\
V68t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint))~(ap~\\
(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V70l1)~V69l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V70l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V69l2)~V68t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~\mname{c\_2Einteger\_2Eint\_\_1})~\mname{c\_2Einteger\_2Eint\_\_1}))~\\
V70l1)~V68t2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V69l2)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~V70l1)~\\
V68t2))))))){\unicdcdcdhd}({\unicdcdadad} V71l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~V71l1)~(\\
c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~V71l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint)))))){\unicdcdcdhd}\\
((({\unicdcdadad} V72c0 \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V73c \in ty\_2Einteger\_2Eint .  \\
({\unicdcdadad} V74l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V75t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  ((ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}~V72c0)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V73c)~V74l)~V75t))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~V72c0)~V73c))~V74l)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}~\\
V72c0)~V75t))))))){\unicdcdcdhd}(({\unicdcdadad} V76c0 \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V77l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V78t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}~\\
V76c0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V77l)~V78t))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V76c0)~V77l)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}~\\
V76c0)~V78t)))))){\unicdcdcdhd}({\unicdcdadad} V79c0 \in ty\_2Einteger\_2Eint .  ((ap~(\\
ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar}~V79c0)~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Einteger\_2Eint))))){\unicdcdcdhd}((({\unicdcdadad} V80l0 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V81c \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V82l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V83t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~\\
V80l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V81c)~V82l)~V83t))=(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V81c)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V80l0)~V82l))~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~\\
V80l0)~V83t))))))){\unicdcdcdhd}(({\unicdcdadad} V84l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V85l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V86t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  ((ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~V84l0)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V85l)~V86t))=(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_varlist\_\_insert}~\\
(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V84l0)~V85l))~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~\\
V84l0)~V86t)))))){\unicdcdcdhd}({\unicdcdadad} V87l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~\\
V87l0)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=(\\
c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))))){\unicdcdcdhd}((({\unicdcdadad} V88c0 \in \\
ty\_2Einteger\_2Eint .  ({\unicdcdadad} V89l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V90c \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V91l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V92t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V88c0)~V89l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V90c)~V91l)~V92t))=(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~V88c0)~V90c))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
ty\_2Equote\_2Eindex)~\mname{c\_2Equote\_2Eindex\_\_lt})~V89l0)~V91l))~(ap~\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V88c0)~V89l0)~V92t)))))))){\unicdcdcdhd}(({\unicdcdadad} V93c0 \in ty\_2Einteger\_2Eint .  \\
({\unicdcdadad} V94l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V95l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V96t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V93c0)~V94l0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V95l)~V96t))=(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_monom\_\_insert}~\\
V93c0)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V94l0)~V95l))~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V93c0)~V94l0)~V96t))))))){\unicdcdcdhd}({\unicdcdadad} V97c0 \in ty\_2Einteger\_2Eint .  \\
({\unicdcdadad} V98l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V97c0)~V98l0)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint)))))){\unicdcdcdhd}(((\\
{\unicdcdadad} V99c1 \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V100l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V101t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V102s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V99c1)~V100l1)~V101t1))~V102s2)=(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~\\
V99c1)~V100l1)~V102s2))~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~\\
V101t1)~V102s2))))))){\unicdcdcdhd}(({\unicdcdadad} V103l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V104t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V105s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~V103l1)~\\
V104t1))~V105s2)=(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar2}~\\
V103l1)~V105s2))~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~\\
V104t1)~V105s2)))))){\unicdcdcdhd}({\unicdcdadad} V106s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))~V106s2)=\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))))){\unicdcdcdhd}((({\unicdcdadad} V107c \in \\
ty\_2Einteger\_2Eint .  ({\unicdcdadad} V108l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V109t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V107c)~V108l)~V109t))=(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~ty\_2Einteger\_2Eint)~\\
V107c)~\mname{c\_2Einteger\_2Eint\_\_0}))~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
V109t))~(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~ty\_2Einteger\_2Eint)~\\
V107c)~\mname{c\_2Einteger\_2Eint\_\_1}))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~V108l)~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
V109t)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V107c)~V108l)~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
V109t)))))))){\unicdcdcdhd}(({\unicdcdadad} V110l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V111t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~(\\
ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~V110l)~\\
V111t))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V110l)~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
V111t))))){\unicdcdcdhd}((ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Einteger\_2Eint)))){\unicdcdcdhd}((({\unicdcdadad} V112vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V113x \in ty\_2Equote\_2Eindex .  ((\\
ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}~V112vm)~V113x)~\\
(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
ty\_2Einteger\_2Eint)~V113x)~V112vm)))){\unicdcdcdhd}({\unicdcdadad} V114vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V115x \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V116x\_27 \in \\
ty\_2Equote\_2Eindex .  ({\unicdcdadad} V117t\_27 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}~V114vm)~V115x)~\\
(ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V116x\_27)~V117t\_27))=\\
(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
ty\_2Einteger\_2Eint)~V115x)~V114vm))~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}~\\
V114vm)~V116x\_27)~V117t\_27)))))))){\unicdcdcdhd}((({\unicdcdadad} V118vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_vl}~\\
V118vm)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=\mname{c\_2Einteger\_2Eint\_\_1})){\unicdcdcdhd}\\
({\unicdcdadad} V119vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V120x \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V121t \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_vl}~\\
V119vm)~(ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V120x)~V121t))=\\
(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}~V119vm)~V120x)~\\
V121t)))))){\unicdcdcdhd}((({\unicdcdadad} V122vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V123c \in ty\_2Einteger\_2Eint .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_m}~\\
V122vm)~V123c)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=V123c))){\unicdcdcdhd}\\
({\unicdcdadad} V124vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V125c \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V126x \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V127t \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_m}~V124vm)~V125c)~(\\
ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V126x)~V127t))=(\\
ap~(ap~\mname{c\_2Einteger\_2Eint\_\_mul}~V125c)~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ivl\_\_aux}~\\
V124vm)~V126x)~V127t)))))))){\unicdcdcdhd}((({\unicdcdadad} V128vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V129a \in ty\_2Einteger\_2Eint .  ((\\
ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~V128vm)~V129a)~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint))=V129a))){\unicdcdcdhd}\\
(({\unicdcdadad} V130vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V131a \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V132l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V133t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~\\
V130vm)~V131a)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V132l)~V133t))=(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V131a)~(ap~(ap~(\\
ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~V130vm)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_vl}~\\
V130vm)~V132l))~V133t))))))){\unicdcdcdhd}({\unicdcdadad} V134vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V135a \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V136c \in \\
ty\_2Einteger\_2Eint .  ({\unicdcdadad} V137l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V138t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Einteger\_2Eint) .  \\
((ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~V134vm)~V135a)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V136c)~V137l)~V138t))=(ap~(ap~\mname{c\_2Einteger\_2Eint\_\_add}~V135a)~(\\
ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~V134vm)~(ap~(ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_m}~V134vm)~V136c)~V137l))~\\
V138t)))))))))){\unicdcdcdhd}((({\unicdcdadad} V139vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_cs}~V139vm)~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Einteger\_2Eint))=\mname{c\_2Einteger\_2Eint\_\_0})){\unicdcdcdhd}(({\unicdcdadad} V140vm \in \\
(ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V141l \in (\\
ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V142t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_cs}~\\
V140vm)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Einteger\_2Eint)~\\
V141l)~V142t))=(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~\\
V140vm)~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_vl}~V140vm)~\\
V141l))~V142t))))){\unicdcdcdhd}({\unicdcdadad} V143vm \in (ty\_2Equote\_2Evarmap~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V144c \in ty\_2Einteger\_2Eint .  ({\unicdcdadad} V145l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V146t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Einteger\_2Eint) .  ((ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_cs}~\\
V143vm)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Einteger\_2Eint)~\\
V144c)~V145l)~V146t))=(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_ics\_\_aux}~\\
V143vm)~(ap~(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_interp\_\_m}~V143vm)~\\
V144c)~V145l))~V146t)))))))){\unicdcdcdhd}((({\unicdcdadad} V147i \in ty\_2Equote\_2Eindex .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~(ap~(c\_2EringNorm\_2EPvar~\\
ty\_2Einteger\_2Eint)~V147i))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Einteger\_2Eint)~(ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~\\
V147i)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex)))~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Einteger\_2Eint)))){\unicdcdcdhd}(({\unicdcdadad} V148c \in ty\_2Einteger\_2Eint .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~(ap~(c\_2EringNorm\_2EPconst~\\
ty\_2Einteger\_2Eint)~V148c))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Einteger\_2Eint)~V148c)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Einteger\_2Eint)))){\unicdcdcdhd}(({\unicdcdadad} V149pl \in \\
(ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  ({\unicdcdadad} V150pr \in \\
(ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  ((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~\\
(ap~(ap~(c\_2EringNorm\_2EPplus~ty\_2Einteger\_2Eint)~V149pl)~V150pr))=\\
(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_merge}~(ap~\\
\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~V149pl))~(ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~\\
V150pr))))){\unicdcdcdhd}(({\unicdcdadad} V151pl \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
({\unicdcdadad} V152pr \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~(ap~(ap~(c\_2EringNorm\_2EPmult~\\
ty\_2Einteger\_2Eint)~V151pl)~V152pr))=(ap~(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_prod}~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~V151pl))~(ap~\\
\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~V152pr))))){\unicdcdcdhd}({\unicdcdadad} V153p \in \\
(ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  ((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~\\
(ap~(c\_2EringNorm\_2EPopp~ty\_2Einteger\_2Eint)~V153p))=(ap~(ap~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_scalar3}~(ap~\\
\mname{c\_2Einteger\_2Eint\_\_neg}~\mname{c\_2Einteger\_2Eint\_\_1}))~(c\_2Elist\_2ENIL~\\
ty\_2Equote\_2Eindex))~(ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~\\
V153p)))))))){\unicdcdcdhd}({\unicdcdadad} V154x \in (ty\_2EringNorm\_2Epolynom~ty\_2Einteger\_2Eint) .  \\
((ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_simplify}~V154x)=(ap~\mname{c\_2EintegerRing\_2Eint\_\_r\_\_canonical\_\_sum\_\_simplify}~\\
(ap~\mname{c\_2EintegerRing\_2Eint\_\_polynom\_\_normalize}~V154x)))))))))))))))))))))\end{array}
\label{hyp:ehigngpfcdfejgogehfghgfgchcfjgoghgpfcdfejgogehpfpfchjgoghgpfpfehigngdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(((ap~(ap~c\_2Equote\_2Eindex\_\_compare~c\_2Equote\_2EEnd\_\_idx)~\\
c\_2Equote\_2EEnd\_\_idx)=c\_2EternaryComparisons\_2EEQUAL){\unicdcdcdhd}(\\
({\unicdcdadad} V0v10 \in ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
c\_2Equote\_2EEnd\_\_idx)~(ap~c\_2Equote\_2ELeft\_\_idx~V0v10))=c\_2EternaryComparisons\_2ELESS)){\unicdcdcdhd}\\
(({\unicdcdadad} V1v11 \in ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
c\_2Equote\_2EEnd\_\_idx)~(ap~c\_2Equote\_2ERight\_\_idx~V1v11))=c\_2EternaryComparisons\_2ELESS)){\unicdcdcdhd}\\
(({\unicdcdadad} V2v2 \in ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
(ap~c\_2Equote\_2ELeft\_\_idx~V2v2))~c\_2Equote\_2EEnd\_\_idx)=c\_2EternaryComparisons\_2EGREATER)){\unicdcdcdhd}\\
(({\unicdcdadad} V3v3 \in ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
(ap~c\_2Equote\_2ERight\_\_idx~V3v3))~c\_2Equote\_2EEnd\_\_idx)=c\_2EternaryComparisons\_2EGREATER)){\unicdcdcdhd}\\
(({\unicdcdadad} V4n\_27 \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V5m\_27 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~c\_2Equote\_2Eindex\_\_compare~(ap~c\_2Equote\_2ELeft\_\_idx~\\
V4n\_27))~(ap~c\_2Equote\_2ELeft\_\_idx~V5m\_27))=(ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
V4n\_27)~V5m\_27)))){\unicdcdcdhd}(({\unicdcdadad} V6n\_27 \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V7m\_27 \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~(ap~\\
c\_2Equote\_2ELeft\_\_idx~V6n\_27))~(ap~c\_2Equote\_2ERight\_\_idx~V7m\_27))=\\
c\_2EternaryComparisons\_2ELESS))){\unicdcdcdhd}(({\unicdcdadad} V8n\_27 \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V9m\_27 \in ty\_2Equote\_2Eindex .  ((ap~(ap~c\_2Equote\_2Eindex\_\_compare~\\
(ap~c\_2Equote\_2ERight\_\_idx~V8n\_27))~(ap~c\_2Equote\_2ERight\_\_idx~\\
V9m\_27))=(ap~(ap~c\_2Equote\_2Eindex\_\_compare~V8n\_27)~V9m\_27)))){\unicdcdcdhd}\\
({\unicdcdadad} V10n\_27 \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V11m\_27 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~c\_2Equote\_2Eindex\_\_compare~(ap~c\_2Equote\_2ERight\_\_idx~\\
V10n\_27))~(ap~c\_2Equote\_2ELeft\_\_idx~V11m\_27))=c\_2EternaryComparisons\_2EGREATER)))))))))))\end{array}
\label{hyp:ehigngpfcdfebhfhpgehfgpfcdfejgogegfgihpfpfdgpgngahbgchfgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0v0 \in A\_27a .  ({\unicdcdadad} V1v1 \in \\
A\_27a .  ({\unicdcdadad} V2v2 \in A\_27a .  ((ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
A\_27a)~c\_2EternaryComparisons\_2ELESS)~V0v0)~V1v1)~V2v2)=V0v0)))){\unicdcdcdhd}\\
(({\unicdcdadad} V3v0 \in A\_27a .  ({\unicdcdadad} V4v1 \in A\_27a .  ({\unicdcdadad} V5v2 \in A\_27a .  \\
((ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~A\_27a)~\\
c\_2EternaryComparisons\_2EEQUAL)~V3v0)~V4v1)~V5v2)=V4v1)))){\unicdcdcdhd}\\
({\unicdcdadad} V6v0 \in A\_27a .  ({\unicdcdadad} V7v1 \in A\_27a .  ({\unicdcdadad} V8v2 \in A\_27a .  \\
((ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~A\_27a)~\\
c\_2EternaryComparisons\_2EGREATER)~V6v0)~V7v1)~V8v2)=V8v2))))))\end{array}
\label{hyp:ehigngpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghgpfpfdgbgdhfgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(({\unicdcdadad} V0x \in ty\_2EternaryComparisons\_2Eordering .  ((V0x=V0x){\unicdbdjded}\\
True)){\unicdcdcdhd}(((c\_2EternaryComparisons\_2ELESS=c\_2EternaryComparisons\_2EEQUAL){\unicdbdjded}\\
False){\unicdcdcdhd}(((c\_2EternaryComparisons\_2ELESS=c\_2EternaryComparisons\_2EGREATER){\unicdbdjded}\\
False){\unicdcdcdhd}(((c\_2EternaryComparisons\_2EEQUAL=c\_2EternaryComparisons\_2EGREATER){\unicdbdjded}\\
False){\unicdcdcdhd}(((c\_2EternaryComparisons\_2EEQUAL=c\_2EternaryComparisons\_2ELESS){\unicdbdjded}\\
False){\unicdcdcdhd}(((c\_2EternaryComparisons\_2EGREATER=c\_2EternaryComparisons\_2ELESS){\unicdbdjded}\\
False){\unicdcdcdhd}(((c\_2EternaryComparisons\_2EGREATER=c\_2EternaryComparisons\_2EEQUAL){\unicdbdjded}\\
False){\unicdcdcdhd}((((ap~c\_2EternaryComparisons\_2Eordering2num~c\_2EternaryComparisons\_2ELESS)=\\
\mname{c\_2Enum\_2E0}){\unicdcdcdhd}(((ap~c\_2EternaryComparisons\_2Eordering2num~\\
c\_2EternaryComparisons\_2EEQUAL)=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))){\unicdcdcdhd}((ap~c\_2EternaryComparisons\_2Eordering2num~\\
c\_2EternaryComparisons\_2EGREATER)=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO}))))){\unicdcdcdhd}(((ap~\\
c\_2EternaryComparisons\_2Enum2ordering~\mname{c\_2Enum\_2E0})=c\_2EternaryComparisons\_2ELESS){\unicdcdcdhd}\\
(((ap~c\_2EternaryComparisons\_2Enum2ordering~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))=c\_2EternaryComparisons\_2EEQUAL){\unicdcdcdhd}\\
((ap~c\_2EternaryComparisons\_2Enum2ordering~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT2}~\mname{c\_2Earithmetic\_2EZERO})))=c\_2EternaryComparisons\_2EGREATER)))))))))))\end{array}
\label{hyp:ehigngpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghgpfpffgbhpfpfegfgdg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}(\\
({\unicdcdadad} V0cmp \in ((ty\_2EternaryComparisons\_2Eordering^{{A\_27b}})^{{A\_27a}}) .  \\
((ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~A\_27a~A\_27b)~\\
V0cmp)~(c\_2Elist\_2ENIL~A\_27a))~(c\_2Elist\_2ENIL~A\_27b))=c\_2EternaryComparisons\_2EEQUAL)){\unicdcdcdhd}\\
(({\unicdcdadad} V1v9 \in (ty\_2Elist\_2Elist~A\_27b) .  ({\unicdcdadad} V2v8 \in A\_27b .  \\
({\unicdcdadad} V3cmp \in ((ty\_2EternaryComparisons\_2Eordering^{{A\_27b}})^{{A\_27a}}) .  \\
((ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~A\_27a~A\_27b)~\\
V3cmp)~(c\_2Elist\_2ENIL~A\_27a))~(ap~(ap~(c\_2Elist\_2ECONS~A\_27b)~\\
V2v8)~V1v9))=c\_2EternaryComparisons\_2ELESS)))){\unicdcdcdhd}(({\unicdcdadad} V4v5 \in \\
(ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V5v4 \in A\_27a .  ({\unicdcdadad} V6cmp \in \\
((ty\_2EternaryComparisons\_2Eordering^{{A\_27b}})^{{A\_27a}}) .  ((ap~(ap~\\
(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~A\_27a~A\_27b)~V6cmp)~\\
(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V5v4)~V4v5))~(c\_2Elist\_2ENIL~A\_27b))=\\
c\_2EternaryComparisons\_2EGREATER)))){\unicdcdcdhd}({\unicdcdadad} V7y \in A\_27b .  \\
({\unicdcdadad} V8x \in A\_27a .  ({\unicdcdadad} V9l2 \in (ty\_2Elist\_2Elist~A\_27b) .  \\
({\unicdcdadad} V10l1 \in (ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V11cmp \in ((\\
ty\_2EternaryComparisons\_2Eordering^{{A\_27b}})^{{A\_27a}}) .  ((ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~A\_27a~A\_27b)~V11cmp)~\\
(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V8x)~V10l1))~(ap~(ap~(c\_2Elist\_2ECONS~\\
A\_27b)~V7y)~V9l2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
ty\_2EternaryComparisons\_2Eordering)~(ap~(ap~V11cmp~V8x)~V7y))~\\
c\_2EternaryComparisons\_2ELESS)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
A\_27a~A\_27b)~V11cmp)~V10l1)~V9l2))~c\_2EternaryComparisons\_2EGREATER))))))))))\end{array}
\label{hyp:ehigngpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfemgjgdhehpfpfdgpgngahbgchfgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0l1 \in (ty\_2Elist\_2Elist~\\
A\_27a) .  ({\unicdcdadad} V1a\_\_lt \in ((2^{{A\_27a}})^{{A\_27a}}) .  ((ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a)~V1a\_\_lt)~V0l1)~(c\_2Elist\_2ENIL~A\_27a))=V0l1))){\unicdcdcdhd}(({\unicdcdadad} V2v5 \in \\
(ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V3v4 \in A\_27a .  ({\unicdcdadad} V4a\_\_lt \in \\
((2^{{A\_27a}})^{{A\_27a}}) .  ((ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a)~V4a\_\_lt)~(c\_2Elist\_2ENIL~A\_27a))~(ap~(ap~(c\_2Elist\_2ECONS~\\
A\_27a)~V3v4)~V2v5))=(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V3v4)~V2v5))))){\unicdcdcdhd}\\
({\unicdcdadad} V5y \in A\_27a .  ({\unicdcdadad} V6x \in A\_27a .  ({\unicdcdadad} V7l2 \in (ty\_2Elist\_2Elist~\\
A\_27a) .  ({\unicdcdadad} V8l1 \in (ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V9a\_\_lt \in \\
((2^{{A\_27a}})^{{A\_27a}}) .  ((ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a)~V9a\_\_lt)~(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V6x)~V8l1))~(ap~\\
(ap~(c\_2Elist\_2ECONS~A\_27a)~V5y)~V7l2))=(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~\\
(ty\_2Elist\_2Elist~A\_27a))~(ap~(ap~V9a\_\_lt~V6x)~V5y))~(ap~(ap~(c\_2Elist\_2ECONS~\\
A\_27a)~V6x)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a)~V9a\_\_lt)~V8l1)~(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V5y)~V7l2))))~\\
(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V5y)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
A\_27a)~V9a\_\_lt)~(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V6x)~V8l1))~V7l2)))))))))))\end{array}
\label{hyp:ehigngpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfemgjgdhehpfpfngfgchhgfgpfpfegfggg}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfeggchbgdgpfcdfegecfbedepfpfbeeeeepfpfbedfdfpede}
$$\begin{array}{c}({\unicdcdadad} V0a \in ty\_2Efrac\_2Efrac .  ({\unicdcdadad} V1b \in ty\_2Efrac\_2Efrac .  \\
({\unicdcdadad} V2c \in ty\_2Efrac\_2Efrac .  ((ap~(ap~\mname{c\_2Efrac\_2Efrac\_\_add}~\\
V0a)~(ap~(ap~\mname{c\_2Efrac\_2Efrac\_\_add}~V1b)~V2c))=(ap~(ap~\mname{c\_2Efrac\_2Efrac\_\_add}~\\
(ap~(ap~\mname{c\_2Efrac\_2Efrac\_\_add}~V0a)~V1b))~V2c)))))\end{array}$$
\end{theorem}
\end{document}
