\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\_2EnumRing\_2Enum\_\_ring\_\_thms (TMHKZe4uPKU68pKDH29vtBugqR85ybxcNDe)}
\maketitle
Let $ ty\_2EternaryComparisons\_2Eordering : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2EternaryComparisons\_2Eordering}}\label{hyp:ogfgpfehjhpfcdfeehfgchogbgchjhdepgngahbgchjgdhpgogdhpfcdfepgchegfgchjgoghg}
\end{equation}
Let $ ty\_2Equote\_2Eindex : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Equote\_2Eindex}}\label{hyp:ogfgpfehjhpfcdfebhfhpgehfgpfcdfejgogegfgih}
\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 $ 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\_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 $ ty\_2Enum\_2Enum : {\iota}$ be given.
Assume the following.
\begin{equation}
{{nonempty}~{ty\_2Enum\_2Enum}}\label{hyp:ogfgpfehjhpfcdfeogfhngpfcdfeogfhng}
\end{equation}
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}
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:dgpfcdfengjgogpfcdfepfddee}
We define $\mname{c\_2Emin\_2E\_3D}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} x \in {A} .  {{\uniddcgcg} y \in {A} .  {{inj\_\_o}~{({{x}={y}})}}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngpfcdfead}
We define $\mname{c\_2Enum\_2E0}$ to be ${({{{ap}~{c\_2Enum\_2EABS\_\_num}}~{c\_2Enum\_2EZERO\_\_REP}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfekffecfpe}
We define $\mname{c\_2Earithmetic\_2EZERO}$ to be ${\mname{c\_2Enum\_2E0}}$.
\end{definition}
Let $ c\_2Enum\_2EREP\_\_num : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2EREP\_\_num} \in {({{omega}^{{ty\_2Enum\_2Enum}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfecffeafpfpfogfhng}
\end{equation}
Let $ c\_2Enum\_2ESUC\_\_REP : {\iota}$ be given.
Assume the following.
\begin{equation}
{{c\_2Enum\_2ESUC\_\_REP} \in {({{omega}^{{omega}}})}}\label{hyp:ngfgngpfdgpfcdfeogfhngpfcdfedfffdepfpfcffeaf}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfeef}
We define $\mname{c\_2Ebool\_2ET}$ to be ${({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{2}}})}})}}~{({{\uniddcgcg} V0x \in {2} .  {V0x}})}})}}~{({{\uniddcgcg} V1x \in {2} .  {V1x}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdbd}
We define $\mname{c\_2Ebool\_2E\_21}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{A\_27a}}})}})}}~{V0P}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {\mname{c\_2Ebool\_2ET}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngpfcdfedfffde}
We define $\mname{c\_2Enum\_2ESUC}$ to be ${{\uniddcgcg} V0m \in {ty\_2Enum\_2Enum} .  {({{{ap}~{c\_2Enum\_2EABS\_\_num}}~{({{{ap}~{c\_2Enum\_2ESUC\_\_REP}}~{({{{ap}~{c\_2Enum\_2EREP\_\_num}}~{V0m}})}})}})}}$.
\end{definition}
Let $ c\_2Earithmetic\_2E\_2B : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2E\_2B \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepfcdce}
\end{equation}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfecejeefbd}
We define $\mname{c\_2Earithmetic\_2EBIT1}$ to be ${{\uniddcgcg} V0n \in {ty\_2Enum\_2Enum} .  {({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{({{{ap}~{c\_2Earithmetic\_2E\_2B}}~{V0n}})}}~{({{{ap}~{\mname{c\_2Enum\_2ESUC}}}~{\mname{c\_2Enum\_2E0}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfebgchjgehigngfgehjgdgpfcdfeoeffnefecfbeme}
We define $\mname{c\_2Earithmetic\_2ENUMERAL}$ to be ${{\uniddcgcg} V0x \in {ty\_2Enum\_2Enum} .  {V0x}}$.
\end{definition}
\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:dgpfcdfecgpgpgmgpfcdfepfcdgepffdde}
We define $\mname{c\_2Ebool\_2E\_2F\_5C}$ to be ${({{\uniddcgcg} V0t1 \in {2} .  {({{\uniddcgcg} V1t2 \in {2} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V2t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t1}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V1t2}})}}~{V2t}})}})}})}}~{V2t}})}})}})}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfedad}
We define $\mname{c\_2Emin\_2E\_40}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} P \in {{2}^{{A}}} .  {{\mathbf{if}}~{({{\unicdcdaddd} x \in {A} .  {{p}~{({{{ap}~{P}}~{x}})}}})}~{\mathbf{then}}~{({{the}~{({{\uniddcgcg} x .  {{{x} \in {A}}{\unicdcdcdhd}{{p}~{({{{ap}~{P}}~{x}})}}}})}})}~{\mathbf{else}}~{({{the}~{({{\uniddcgcg} x .  {{x} \in {A}}})}})}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def: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:dgpfcdfecgpgpgmgpfcdfepfhdfe}
We define $\mname{c\_2Ebool\_2E\_7E}$ to be ${({{\uniddcgcg} V0t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t}})}}~{\mname{c\_2Ebool\_2EF}}})}})}$.
\end{definition}
\begin{definition}\label{def: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\_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\_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}
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 $ 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\_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\_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\_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\_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 $ ty\_2Ecanonical\_2Espolynom : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Ecanonical\_2Espolynom}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfedgbgogpgogjgdgbgmgpfcdfedhahpgmgjhogpgng}
\end{equation}
Let $ c\_2Ecanonical\_2ESPmult : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ESPmult~A\_27a \in \\
(((ty\_2Ecanonical\_2Espolynom~A\_27a)^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedfafngfhmgeh}
\end{equation}
Let $ c\_2Ecanonical\_2ESPplus : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ESPplus~A\_27a \in \\
(((ty\_2Ecanonical\_2Espolynom~A\_27a)^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedfafahmgfhdh}
\end{equation}
Let $ c\_2Ecanonical\_2ESPvar : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ESPvar~A\_27a \in (\\
(ty\_2Ecanonical\_2Espolynom~A\_27a)^{{ty\_2Equote\_2Eindex}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedfafghbgch}
\end{equation}
Let $ c\_2Ecanonical\_2ESPconst : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2ESPconst~A\_27a \in \\
((ty\_2Ecanonical\_2Espolynom~A\_27a)^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedfafdgpgogdheh}
\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\_2Esemi\_\_ring\_\_SRM : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~\\
A\_27a \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfdfcfne}
\end{equation}
Let $ c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~\\
A\_27a \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfdfcfaf}
\end{equation}
Let $ c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0~\\
A\_27a \in (A\_27a^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfdfcfad}
\end{equation}
Let $ c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~\\
A\_27a \in (A\_27a^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfdfcfbd}
\end{equation}
\begin{definition}\label{def:dgpfcdfedhfgngjgpfpfchjgoghgpfcdfejgdhpfpfdhfgngjgpfpfchjgoghg}
We define $\mname{c\_2Esemi\_\_ring\_2Eis\_\_semi\_\_ring}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0r \in {({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{V1n}})}}~{V2m}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{V3n}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{V4m}})}}~{V5p}})}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{V6n}})}}~{V7m}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{V8n}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{V9m}})}}~{V10p}})}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0}~{A\_27a}})}}~{V0r}})}})}}~{V13n}})}})}}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0}~{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\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{V14n}})}}~{V15m}})}})}}~{V16p}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP}~{A\_27a}})}}~{V0r}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{V14n}})}}~{V16p}})}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM}~{A\_27a}})}}~{V0r}})}}~{V15m}})}}~{V16p}})}})}})}})}})}})}})}})}})}})}})}})}})}})}})}})}}}$.
\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\_2Einterp\_\_sp : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Einterp\_\_sp~A\_27a \in \\
(((A\_27a^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})^{{({{ty\_2Equote\_2Evarmap}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfdhah}
\end{equation}
Let $ c\_2Earithmetic\_2E\_2A : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}c\_2Earithmetic\_2E\_2A \in ((ty\_2Enum\_2Enum^{{ty\_2Enum\_2Enum}})^{{ty\_2Enum\_2Enum}})\end{array}
\label{hyp:ngfgngpfdgpfcdfebgchjgehigngfgehjgdgpfcdfepfcdbe}
\end{equation}
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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgogehfgchahpfpfdhah}
We define $\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_sp}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
Let $ c\_2Ecanonical\_2Espolynom\_\_normalize : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ecanonical\_2Espolynom\_\_normalize~\\
A\_27a \in (((ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a)^{{({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})}})^{{({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfedgbgogpgogjgdgbgmgpfcdfedhahpgmgjhogpgngpfpfogpgchngbgmgjgkhfg}
\end{equation}
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:dgpfcdfedgbgogpgogjgdgbgmgpfcdfedhahpgmgjhogpgngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2Ecanonical\_2Espolynom\_\_simplify}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} V0sr \in {({{ty\_2Esemi\_\_ring\_2Esemi\_\_ring}~{A\_27a}})} .  {{\uniddcgcg} V1x \in {({{ty\_2Ecanonical\_2Espolynom}~{A\_27a}})} .  {({{{ap}~{({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify}~{A\_27a}})}}~{V0sr}})}}~{({{{ap}~{({{{ap}~{({{c\_2Ecanonical\_2Espolynom\_\_normalize}~{A\_27a}})}}~{V0sr}})}}~{V1x}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdhahpgmgjhogpgngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_simplify}$ to be ${({{{ap}~{({{\mname{c\_2Ecanonical\_2Espolynom\_\_simplify}}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdhahpgmgjhogpgngpfpfogpgchngbgmgjgkhfg}
We define $\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Espolynom\_\_normalize}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgogehfgchahpfpfdgdh}
We define $\mname{c\_2EnumRing\_2Enum\_\_interp\_\_cs}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_cs}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgdgdhpfpfbgfhih}
We define $\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Eics\_\_aux}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgogehfgchahpfpfng}
We define $\mname{c\_2EnumRing\_2Enum\_\_interp\_\_m}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_m}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgogehfgchahpfpfghmg}
We define $\mname{c\_2EnumRing\_2Enum\_\_interp\_\_vl}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Einterp\_\_vl}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfjgghmgpfpfbgfhih}
We define $\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Eivl\_\_aux}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhjgngahmgjgggjh}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfahchpgeg}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchdd}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchcd}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgch}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfghbgchmgjgdhehpfpfjgogdhfgcheh}
We define $\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Evarlist\_\_insert}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfngpgogpgngpfpfjgogdhfgcheh}
We define $\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Emonom\_\_insert}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\end{definition}
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:dgpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdgbgogpgogjgdgbgmgpfpfdhfhngpfpfngfgchhgfg}
We define $\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}$ to be ${({{{ap}~{({{c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge}~{ty\_2Enum\_2Enum}})}}~{({{{ap}~{({{{ap}~{({{{ap}~{({{{ap}~{({{c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring}~{ty\_2Enum\_2Enum}})}}~{\mname{c\_2Enum\_2E0}}})}}~{({{{ap}~{\mname{c\_2Earithmetic\_2ENUMERAL}}}~{({{{ap}~{\mname{c\_2Earithmetic\_2EBIT1}}}~{\mname{c\_2Earithmetic\_2EZERO}}})}})}})}}~{c\_2Earithmetic\_2E\_2B}})}}~{c\_2Earithmetic\_2E\_2A}})}})}$.
\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\_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\_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\_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\_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 $ 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}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1y \in \\
A\_27a .  ((V0x=V1y){\unicdbdjded}(V1y=V0x))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfefebfpfpfdfjfnepfpffebf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V1t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
({\unicdcdadad} V2sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V3l2 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V4l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V5c2 \in A\_27a .  ({\unicdcdadad} V6c1 \in A\_27a .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~V2sr)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V6c1)~V4l1)~V1t1))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V5c2)~V3l2)~V0t2))=\\
(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V4l1)~V3l2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V6c1)~\\
V4l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~\\
V2sr)~V1t1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V5c2)~\\
V3l2)~V0t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V2sr)~V6c1)~\\
V5c2))~V4l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V2sr)~V1t1)~V0t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
A\_27a)~V5c2)~V3l2)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V2sr)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V6c1)~\\
V4l1)~V1t1))~V0t2))))))))))){\unicdcdcdhd}(({\unicdcdadad} V7t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V8t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
({\unicdcdadad} V9sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V10l2 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V11l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V12c1 \in A\_27a .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V9sr)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V12c1)~\\
V11l1)~V8t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V10l2)~\\
V7t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V11l1)~V10l2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
V12c1)~V11l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V9sr)~V8t1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V10l2)~V7t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V9sr)~V12c1)~\\
(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V9sr)))~V11l1)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~V9sr)~\\
V8t1)~V7t2)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V10l2)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~V9sr)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V12c1)~V11l1)~\\
V8t1))~V7t2)))))))))){\unicdcdcdhd}(({\unicdcdadad} V13t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V14t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
({\unicdcdadad} V15sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V16l2 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V17l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V18c2 \in A\_27a .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V15sr)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V17l1)~\\
V14t1))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V18c2)~\\
V16l2)~V13t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V17l1)~V16l2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V17l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~\\
V15sr)~V14t1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
V18c2)~V16l2)~V13t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
A\_27a)~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V15sr)~\\
(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V15sr))~V18c2))~\\
V17l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~\\
V15sr)~V14t1)~V13t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
A\_27a)~V18c2)~V16l2)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V15sr)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V17l1)~\\
V14t1))~V13t2)))))))))){\unicdcdcdhd}(({\unicdcdadad} V19t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V20t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
({\unicdcdadad} V21sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V22l2 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V23l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V21sr)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V23l1)~\\
V20t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V22l2)~\\
V19t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V23l1)~V22l2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V23l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~\\
V21sr)~V20t1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V22l2)~\\
V19t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~(ap~\\
(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V21sr)~(ap~(\\
c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V21sr))~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~\\
A\_27a)~V21sr)))~V23l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V21sr)~V20t1)~V19t2)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
A\_27a)~V22l2)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V21sr)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V23l1)~\\
V20t1))~V19t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V24sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V25s1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~V24sr)~\\
V25s1)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=V25s1))){\unicdcdcdhd}(({\unicdcdadad} V26v6 \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ({\unicdcdadad} V27v5 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V28v4 \in A\_27a .  ({\unicdcdadad} V29sr \in (\\
ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V29sr)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V28v4)~V27v5)~V26v6))=(\\
ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V28v4)~V27v5)~V26v6)))))){\unicdcdcdhd}\\
({\unicdcdadad} V30v8 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ({\unicdcdadad} V31v7 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V32sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V32sr)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
A\_27a)~V31v7)~V30v8))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
A\_27a)~V31v7)~V30v8)))))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfngfgchhgfgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V1sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  \\
({\unicdcdadad} V2l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V3l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V4c2 \in A\_27a .  \\
({\unicdcdadad} V5c1 \in A\_27a .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~\\
A\_27a)~V1sr)~V5c1)~V3l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
A\_27a)~V4c2)~V2l2)~V0t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V3l1)~V2l2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V5c1)~\\
V3l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V4c2)~V2l2)~\\
V0t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~(ap~(ap~\\
(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V1sr)~V5c1)~V4c2))~\\
V3l1)~V0t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V4c2)~\\
V2l2)~(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~A\_27a)~V1sr)~\\
V5c1)~V3l1)~V0t2)))))))))){\unicdcdcdhd}(({\unicdcdadad} V6t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V7sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  \\
({\unicdcdadad} V8l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V9l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V10c1 \in A\_27a .  \\
((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~A\_27a)~V7sr)~V10c1)~\\
V9l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V8l2)~V6t2))=\\
(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V9l1)~V8l2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V10c1)~\\
V9l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V8l2)~V6t2)))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~\\
A\_27a)~V7sr)~V10c1)~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~\\
V7sr)))~V9l1)~V6t2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V8l2)~(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~A\_27a)~V7sr)~\\
V10c1)~V9l1)~V6t2))))))))){\unicdcdcdhd}({\unicdcdadad} V11sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V12l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V13c1 \in A\_27a .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~\\
A\_27a)~V11sr)~V13c1)~V12l1)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V13c1)~V12l1)~\\
(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfengpgogpgngpfpfjgogdhfgchehpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V1sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  \\
({\unicdcdadad} V2l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V3l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V4c2 \in A\_27a .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Evarlist\_\_insert~A\_27a)~V1sr)~V3l1)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V4c2)~V2l2)~V0t2))=\\
(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V3l1)~V2l2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V3l1)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V4c2)~V2l2)~V0t2)))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~\\
A\_27a)~V1sr)~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V1sr))~\\
V4c2))~V3l1)~V0t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
V4c2)~V2l2)~(ap~(ap~(ap~(c\_2Ecanonical\_2Evarlist\_\_insert~A\_27a)~\\
V1sr)~V3l1)~V0t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V5t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V6sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  \\
({\unicdcdadad} V7l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V8l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Evarlist\_\_insert~\\
A\_27a)~V6sr)~V8l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V7l2)~V5t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_compare~\\
ty\_2Equote\_2Eindex~ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~\\
V8l1)~V7l2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V8l1)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V7l2)~V5t2)))~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~\\
A\_27a)~V6sr)~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V6sr))~\\
(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~V6sr)))~V8l1)~V5t2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V7l2)~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2Evarlist\_\_insert~A\_27a)~V6sr)~V8l1)~V5t2)))))))){\unicdcdcdhd}\\
({\unicdcdadad} V9sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V10l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Evarlist\_\_insert~\\
A\_27a)~V9sr)~V10l1)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V10l1)~(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a)))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfeghbgchmgjgdhehpfpfjgogdhfgchehpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1c0 \in A\_27a .  ({\unicdcdadad} V2c \in A\_27a .  ({\unicdcdadad} V3l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V4t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~\\
A\_27a)~V0sr)~V1c0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
V2c)~V3l)~V4t))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~A\_27a)~V0sr)~V1c0)~\\
V2c))~V3l)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~\\
A\_27a)~V0sr)~V1c0)~V4t)))))))){\unicdcdcdhd}(({\unicdcdadad} V5sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V6c0 \in A\_27a .  ({\unicdcdadad} V7l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V8t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~\\
A\_27a)~V5sr)~V6c0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V7l)~V8t))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V6c0)~\\
V7l)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~A\_27a)~\\
V5sr)~V6c0)~V8t))))))){\unicdcdcdhd}({\unicdcdadad} V9sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V10c0 \in A\_27a .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar~\\
A\_27a)~V9sr)~V10c0)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V2c \in A\_27a .  ({\unicdcdadad} V3l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V4t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~A\_27a)~V0sr)~\\
V1l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V2c)~V3l)~\\
V4t))=(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~A\_27a)~V0sr)~\\
V2c)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V1l0)~V3l))~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~\\
A\_27a)~V0sr)~V1l0)~V4t)))))))){\unicdcdcdhd}(({\unicdcdadad} V5sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V6l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V7l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V8t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~\\
A\_27a)~V5sr)~V6l0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V7l)~V8t))=(ap~(ap~(ap~(c\_2Ecanonical\_2Evarlist\_\_insert~A\_27a)~\\
V5sr)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V6l0)~V7l))~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~\\
A\_27a)~V5sr)~V6l0)~V8t))))))){\unicdcdcdhd}({\unicdcdadad} V9sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V10l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~A\_27a)~\\
V9sr)~V10l0)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchcdpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1c0 \in A\_27a .  ({\unicdcdadad} V2l0 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V3c \in A\_27a .  ({\unicdcdadad} V4l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V5t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~\\
A\_27a)~V0sr)~V1c0)~V2l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
A\_27a)~V3c)~V4l)~V5t))=(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~\\
A\_27a)~V0sr)~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~A\_27a)~\\
V0sr)~V1c0)~V3c))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
ty\_2Equote\_2Eindex)~\mname{c\_2Equote\_2Eindex\_\_lt})~V2l0)~V4l))~(ap~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~A\_27a)~V0sr)~\\
V1c0)~V2l0)~V5t))))))))){\unicdcdcdhd}(({\unicdcdadad} V6sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V7c0 \in A\_27a .  ({\unicdcdadad} V8l0 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V9l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V10t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~A\_27a)~\\
V6sr)~V7c0)~V8l0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V9l)~V10t))=(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Emonom\_\_insert~A\_27a)~\\
V6sr)~V7c0)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
ty\_2Equote\_2Eindex)~\mname{c\_2Equote\_2Eindex\_\_lt})~V8l0)~V9l))~(ap~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~A\_27a)~V6sr)~\\
V7c0)~V8l0)~V10t)))))))){\unicdcdcdhd}({\unicdcdadad} V11sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V12c0 \in A\_27a .  ({\unicdcdadad} V13l0 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~\\
A\_27a)~V11sr)~V12c0)~V13l0)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=\\
(c\_2Ecanonical\_2ENil\_\_monom~A\_27a)))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhdgbgmgbgchddpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1c1 \in A\_27a .  ({\unicdcdadad} V2l1 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V3t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ({\unicdcdadad} V4s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~A\_27a)~V0sr)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V1c1)~V2l1)~V3t1))~\\
V4s2)=(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~\\
V0sr)~(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar3~\\
A\_27a)~V0sr)~V1c1)~V2l1)~V4s2))~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~\\
A\_27a)~V0sr)~V3t1)~V4s2)))))))){\unicdcdcdhd}(({\unicdcdadad} V5sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V6l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V7t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ({\unicdcdadad} V8s2 \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~\\
A\_27a)~V5sr)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V6l1)~\\
V7t1))~V8s2)=(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~\\
A\_27a)~V5sr)~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_scalar2~\\
A\_27a)~V5sr)~V6l1)~V8s2))~(ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~\\
A\_27a)~V5sr)~V7t1)~V8s2))))))){\unicdcdcdhd}({\unicdcdadad} V9sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V10s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~A\_27a)~V9sr)~\\
(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))~V10s2)=(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfahchpgegpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1c \in A\_27a .  ({\unicdcdadad} V2l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V3t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~A\_27a)~V0sr)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V1c)~V2l)~V3t))=\\
(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~A\_27a)~V1c)~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0~\\
A\_27a)~V0sr)))~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~\\
A\_27a)~V0sr)~V3t))~(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~A\_27a)~V1c)~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~\\
A\_27a)~V0sr)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~\\
V2l)~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~A\_27a)~\\
V0sr)~V3t)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V1c)~\\
V2l)~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~A\_27a)~\\
V0sr)~V3t))))))))){\unicdcdcdhd}(({\unicdcdadad} V4sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V5l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V6t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~A\_27a)~V4sr)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V5l)~V6t))=(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V5l)~(ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~\\
A\_27a)~V4sr)~V6t)))))){\unicdcdcdhd}({\unicdcdadad} V7sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ((ap~(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_simplify~\\
A\_27a)~V7sr)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a)))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedgbgogpgogjgdgbgmgpfpfdhfhngpfpfdhjgngahmgjgggjhpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2x \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Eivl\_\_aux~\\
A\_27a)~V0sr)~V1vm)~V2x)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=\\
(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V2x)~V1vm))))){\unicdcdcdhd}({\unicdcdadad} V3sr \in \\
(ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~\\
A\_27a) .  ({\unicdcdadad} V5x \in ty\_2Equote\_2Eindex .  ({\unicdcdadad} V6x\_27 \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V7t\_27 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Eivl\_\_aux~A\_27a)~V3sr)~V4vm)~V5x)~(\\
ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V6x\_27)~V7t\_27))=\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~A\_27a)~V3sr)~(ap~\\
(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V5x)~V4vm))~(ap~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2Eivl\_\_aux~A\_27a)~V3sr)~V4vm)~V6x\_27)~V7t\_27)))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgghmgpfpfbgfhihpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ((ap~(ap~(\\
ap~(c\_2Ecanonical\_2Einterp\_\_vl~A\_27a)~V0sr)~V1vm)~(c\_2Elist\_2ENIL~\\
ty\_2Equote\_2Eindex))=(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~\\
A\_27a)~V0sr)))){\unicdcdcdhd}({\unicdcdadad} V2sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V3vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V4x \in \\
ty\_2Equote\_2Eindex .  ({\unicdcdadad} V5t \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_vl~A\_27a)~V2sr)~V3vm)~(ap~\\
(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V4x)~V5t))=(ap~(ap~(\\
ap~(ap~(c\_2Ecanonical\_2Eivl\_\_aux~A\_27a)~V2sr)~V3vm)~V4x)~V5t)))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfghmgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2c \in \\
A\_27a .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_m~A\_27a)~V0sr)~\\
V1vm)~V2c)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=V2c)))){\unicdcdcdhd}({\unicdcdadad} V3sr \in \\
(ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~\\
A\_27a) .  ({\unicdcdadad} V5c \in A\_27a .  ({\unicdcdadad} V6x \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V7t \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~(ap~\\
(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_m~A\_27a)~V3sr)~V4vm)~V5c)~(ap~\\
(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V6x)~V7t))=(ap~(ap~(\\
ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~A\_27a)~V3sr)~V5c)~(ap~(ap~\\
(ap~(ap~(c\_2Ecanonical\_2Eivl\_\_aux~A\_27a)~V3sr)~V4vm)~V6x)~V7t)))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfngpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2a \in \\
A\_27a .  ((ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V0sr)~\\
V1vm)~V2a)~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))=V2a)))){\unicdcdcdhd}(({\unicdcdadad} V3sr \in \\
(ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~\\
A\_27a) .  ({\unicdcdadad} V5a \in A\_27a .  ({\unicdcdadad} V6l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V7t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V3sr)~V4vm)~V5a)~(\\
ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V6l)~V7t))=(ap~(\\
ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V3sr)~V5a)~(ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V3sr)~V4vm)~(ap~(ap~\\
(ap~(c\_2Ecanonical\_2Einterp\_\_vl~A\_27a)~V3sr)~V4vm)~V6l))~V7t)))))))){\unicdcdcdhd}\\
({\unicdcdadad} V8sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V9vm \in \\
(ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V10a \in A\_27a .  ({\unicdcdadad} V11c \in \\
A\_27a .  ({\unicdcdadad} V12l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V13t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~A\_27a) .  ((ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V8sr)~V9vm)~V10a)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V11c)~V12l)~V13t))=\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~V8sr)~V10a)~\\
(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V8sr)~V9vm)~(ap~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_m~A\_27a)~V8sr)~V9vm)~V11c)~\\
V12l))~V13t)))))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgdgdhpfpfbgfhihpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ((ap~(ap~(\\
ap~(c\_2Ecanonical\_2Einterp\_\_cs~A\_27a)~V0sr)~V1vm)~(c\_2Ecanonical\_2ENil\_\_monom~\\
A\_27a))=(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0~A\_27a)~V0sr)))){\unicdcdcdhd}\\
(({\unicdcdadad} V2sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V3vm \in \\
(ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V4l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V5t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_cs~A\_27a)~V2sr)~\\
V3vm)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~V4l)~V5t))=\\
(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V2sr)~V3vm)~(ap~\\
(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_vl~A\_27a)~V2sr)~V3vm)~V4l))~V5t)))))){\unicdcdcdhd}\\
({\unicdcdadad} V6sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V7vm \in \\
(ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V8c \in A\_27a .  ({\unicdcdadad} V9l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V10t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_cs~A\_27a)~V6sr)~\\
V7vm)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V8c)~V9l)~\\
V10t))=(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Eics\_\_aux~A\_27a)~V6sr)~\\
V7vm)~(ap~(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_m~A\_27a)~V6sr)~V7vm)~\\
V8c)~V9l))~V10t)))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfdgdhpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1i \in ty\_2Equote\_2Eindex .  ((ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~\\
A\_27a)~V0sr)~(ap~(c\_2Ecanonical\_2ESPvar~A\_27a)~V1i))=(ap~(ap~(\\
c\_2Ecanonical\_2ECons\_\_varlist~A\_27a)~(ap~(ap~(c\_2Elist\_2ECONS~\\
ty\_2Equote\_2Eindex)~V1i)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex)))~\\
(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))))){\unicdcdcdhd}(({\unicdcdadad} V2sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V3c \in A\_27a .  ((ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~\\
A\_27a)~V2sr)~(ap~(c\_2Ecanonical\_2ESPconst~A\_27a)~V3c))=(ap~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_monom~A\_27a)~V3c)~(c\_2Elist\_2ENIL~\\
ty\_2Equote\_2Eindex))~(c\_2Ecanonical\_2ENil\_\_monom~A\_27a))))){\unicdcdcdhd}\\
(({\unicdcdadad} V4sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V5l \in \\
(ty\_2Ecanonical\_2Espolynom~A\_27a) .  ({\unicdcdadad} V6r \in (ty\_2Ecanonical\_2Espolynom~\\
A\_27a) .  ((ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~\\
V4sr)~(ap~(ap~(c\_2Ecanonical\_2ESPplus~A\_27a)~V5l)~V6r))=(ap~(ap~\\
(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_merge~A\_27a)~V4sr)~(ap~\\
(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~V4sr)~V5l))~\\
(ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~V4sr)~V6r)))))){\unicdcdcdhd}\\
({\unicdcdadad} V7sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V8l \in \\
(ty\_2Ecanonical\_2Espolynom~A\_27a) .  ({\unicdcdadad} V9r \in (ty\_2Ecanonical\_2Espolynom~\\
A\_27a) .  ((ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~\\
V7sr)~(ap~(ap~(c\_2Ecanonical\_2ESPmult~A\_27a)~V8l)~V9r))=(ap~(ap~\\
(ap~(c\_2Ecanonical\_2Ecanonical\_\_sum\_\_prod~A\_27a)~V7sr)~(ap~(\\
ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~V7sr)~V8l))~(\\
ap~(ap~(c\_2Ecanonical\_2Espolynom\_\_normalize~A\_27a)~V7sr)~V9r)))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedhahpgmgjhogpgngpfpfogpgchngbgmgjgkhfgpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2c \in \\
A\_27a .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V0sr)~V1vm)~\\
(ap~(c\_2Ecanonical\_2ESPconst~A\_27a)~V2c))=V2c)))){\unicdcdcdhd}(({\unicdcdadad} V3sr \in \\
(ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~\\
A\_27a) .  ({\unicdcdadad} V5i \in ty\_2Equote\_2Eindex .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~\\
A\_27a)~V3sr)~V4vm)~(ap~(c\_2Ecanonical\_2ESPvar~A\_27a)~V5i))=(ap~\\
(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V5i)~V4vm))))){\unicdcdcdhd}(({\unicdcdadad} V6sr \in \\
(ty\_2Esemi\_\_ring\_2Esemi\_\_ring~A\_27a) .  ({\unicdcdadad} V7vm \in (ty\_2Equote\_2Evarmap~\\
A\_27a) .  ({\unicdcdadad} V8p1 \in (ty\_2Ecanonical\_2Espolynom~A\_27a) .  ({\unicdcdadad} V9p2 \in \\
(ty\_2Ecanonical\_2Espolynom~A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~\\
A\_27a)~V6sr)~V7vm)~(ap~(ap~(c\_2Ecanonical\_2ESPplus~A\_27a)~V8p1)~\\
V9p2))=(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~\\
V6sr)~(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V6sr)~V7vm)~\\
V8p1))~(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V6sr)~V7vm)~\\
V9p2))))))){\unicdcdcdhd}({\unicdcdadad} V10sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ({\unicdcdadad} V11vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V12p1 \in \\
(ty\_2Ecanonical\_2Espolynom~A\_27a) .  ({\unicdcdadad} V13p2 \in (ty\_2Ecanonical\_2Espolynom~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V10sr)~\\
V11vm)~(ap~(ap~(c\_2Ecanonical\_2ESPmult~A\_27a)~V12p1)~V13p2))=\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~A\_27a)~V10sr)~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V10sr)~V11vm)~V12p1))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V10sr)~V11vm)~V13p2))))))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfejgogehfgchahpfpfdhahpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0sr \in (ty\_2Esemi\_\_ring\_2Esemi\_\_ring~\\
A\_27a) .  ((p~(ap~(\mname{c\_2Esemi\_\_ring\_2Eis\_\_semi\_\_ring}~A\_27a)~V0sr)){\unicdbdjdcd}\\
({\unicdcdadad} V1vm \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2p \in (ty\_2Ecanonical\_2Espolynom~\\
A\_27a) .  ((ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_cs~A\_27a)~V0sr)~\\
V1vm)~(ap~(ap~(\mname{c\_2Ecanonical\_2Espolynom\_\_simplify}~A\_27a)~V0sr)~\\
V2p))=(ap~(ap~(ap~(c\_2Ecanonical\_2Einterp\_\_sp~A\_27a)~V0sr)~V1vm)~\\
V2p))))))\end{array}
\label{hyp:ehigngpfcdfedgbgogpgogjgdgbgmgpfcdfedhahpgmgjhogpgngjgbgmgpfpfdhjgngahmgjgggjhpfpfpglg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}(p~(ap~(\mname{c\_2Esemi\_\_ring\_2Eis\_\_semi\_\_ring}~ty\_2Enum\_2Enum)~(ap~\\
(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~ty\_2Enum\_2Enum)~\\
\mname{c\_2Enum\_2E0})~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\\
\mname{c\_2Earithmetic\_2EZERO})))~c\_2Earithmetic\_2E\_2B)~c\_2Earithmetic\_2E\_2A)))\end{array}
\label{hyp:ehigngpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfdhfgngjgpfpfchjgoghg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1v2 \in \\
(ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V2v1 \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)~V0x)~V2v1)~V1v2))=V0x)))){\unicdcdcdhd}\\
(({\unicdcdadad} V3x \in A\_27a .  ({\unicdcdadad} V4v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V5v1 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V6i1 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~(ap~c\_2Equote\_2ERight\_\_idx~\\
V6i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~A\_27a)~V3x)~V5v1)~V4v2))=\\
(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V6i1)~V4v2)))))){\unicdcdcdhd}((\\
{\unicdcdadad} V7x \in A\_27a .  ({\unicdcdadad} V8v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V9v1 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V10i1 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~(ap~c\_2Equote\_2ELeft\_\_idx~\\
V10i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~A\_27a)~V7x)~V9v1)~V8v2))=\\
(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V10i1)~V9v1)))))){\unicdcdcdhd}(\\
{\unicdcdadad} V11i \in ty\_2Equote\_2Eindex .  ((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
A\_27a)~V11i)~(c\_2Equote\_2EEmpty\_\_vm~A\_27a))=(ap~(\mname{c\_2Emin\_2E\_40}~\\
A\_27a)~({\uniddcgcg} V12x \in A\_27a .  \mname{c\_2Ebool\_2ET})))))))\end{array}
\label{hyp:ehigngpfcdfebhfhpgehfgpfcdfeghbgchngbgahpfpfggjgogegpfpfegfggg}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0a \in A\_27a .  ({\unicdcdadad} V1a0 \in \\
A\_27a .  ({\unicdcdadad} V2f \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V3f0 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  \\
((ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR0~A\_27a)~(ap~(ap~(ap~(ap~\\
(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~A\_27a)~V0a)~V1a0)~\\
V2f)~V3f0))=V0a))))){\unicdcdcdhd}(({\unicdcdadad} V4a \in A\_27a .  ({\unicdcdadad} V5a0 \in A\_27a .  \\
({\unicdcdadad} V6f \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V7f0 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  \\
((ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SR1~A\_27a)~(ap~(ap~(ap~(ap~\\
(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~A\_27a)~V4a)~V5a0)~\\
V6f)~V7f0))=V5a0))))){\unicdcdcdhd}(({\unicdcdadad} V8a \in A\_27a .  ({\unicdcdadad} V9a0 \in A\_27a .  \\
({\unicdcdadad} V10f \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V11f0 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  \\
((ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRP~A\_27a)~(ap~(ap~(ap~(ap~\\
(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~A\_27a)~V8a)~V9a0)~\\
V10f)~V11f0))=V10f))))){\unicdcdcdhd}({\unicdcdadad} V12a \in A\_27a .  ({\unicdcdadad} V13a0 \in \\
A\_27a .  ({\unicdcdadad} V14f \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V15f0 \in ((\\
A\_27a^{{A\_27a}})^{{A\_27a}}) .  ((ap~(c\_2Esemi\_\_ring\_2Esemi\_\_ring\_\_SRM~\\
A\_27a)~(ap~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~\\
A\_27a)~V12a)~V13a0)~V14f)~V15f0))=V15f0))))))))\end{array}
\label{hyp:ehigngpfcdfedhfgngjgpfpfchjgoghgpfcdfedhfgngjgpfpfchjgoghgpfpfbgdgdgfgdhdhpgchdh}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfeogfhngcfjgoghgpfcdfeogfhngpfpfchjgoghgpfpfehigngdh}
$$\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}((p~(ap~(\mname{c\_2Esemi\_\_ring\_2Eis\_\_semi\_\_ring}~\\
ty\_2Enum\_2Enum)~(ap~(ap~(ap~(ap~(c\_2Esemi\_\_ring\_2Erecordtype\_2Esemi\_\_ring~\\
ty\_2Enum\_2Enum)~\mname{c\_2Enum\_2E0})~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(\\
ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~c\_2Earithmetic\_2E\_2B)~\\
c\_2Earithmetic\_2E\_2A))){\unicdcdcdhd}(({\unicdcdadad} V0vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V1p \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~V0vm)~V1p)=(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_cs}~\\
V0vm)~(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_simplify}~V1p))))){\unicdcdcdhd}(\\
((({\unicdcdadad} V2vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V3c \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~V2vm)~\\
(ap~(c\_2Ecanonical\_2ESPconst~ty\_2Enum\_2Enum)~V3c))=V3c))){\unicdcdcdhd}\\
(({\unicdcdadad} V4vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V5i \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~\\
V4vm)~(ap~(c\_2Ecanonical\_2ESPvar~ty\_2Enum\_2Enum)~V5i))=(ap~(\\
ap~(c\_2Equote\_2Evarmap\_\_find~ty\_2Enum\_2Enum)~V5i)~V4vm)))){\unicdcdcdhd}\\
(({\unicdcdadad} V6vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V7p1 \in \\
(ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V8p2 \in \\
(ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~\\
V6vm)~(ap~(ap~(c\_2Ecanonical\_2ESPplus~ty\_2Enum\_2Enum)~V7p1)~V8p2))=\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~\\
V6vm)~V7p1))~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~V6vm)~V8p2)))))){\unicdcdcdhd}\\
({\unicdcdadad} V9vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V10p1 \in \\
(ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V11p2 \in \\
(ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~\\
V9vm)~(ap~(ap~(c\_2Ecanonical\_2ESPmult~ty\_2Enum\_2Enum)~V10p1)~\\
V11p2))=(ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~\\
V9vm)~V10p1))~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_sp}~V9vm)~V11p2))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V12x \in A\_27a .  ({\unicdcdadad} V13v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V14v1 \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)~V12x)~V14v1)~V13v2))=V12x)))){\unicdcdcdhd}(({\unicdcdadad} V15x \in A\_27a .  (\\
{\unicdcdadad} V16v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V17v1 \in (\\
ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V18i1 \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~(ap~c\_2Equote\_2ERight\_\_idx~\\
V18i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~A\_27a)~V15x)~V17v1)~V16v2))=\\
(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V18i1)~V16v2)))))){\unicdcdcdhd}\\
(({\unicdcdadad} V19x \in A\_27a .  ({\unicdcdadad} V20v2 \in (ty\_2Equote\_2Evarmap~A\_27a) .  \\
({\unicdcdadad} V21v1 \in (ty\_2Equote\_2Evarmap~A\_27a) .  ({\unicdcdadad} V22i1 \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~\\
(ap~c\_2Equote\_2ELeft\_\_idx~V22i1))~(ap~(ap~(ap~(c\_2Equote\_2ENode\_\_vm~\\
A\_27a)~V19x)~V21v1)~V20v2))=(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
A\_27a)~V22i1)~V21v1)))))){\unicdcdcdhd}({\unicdcdadad} V23i \in ty\_2Equote\_2Eindex .  \\
((ap~(ap~(c\_2Equote\_2Evarmap\_\_find~A\_27a)~V23i)~(c\_2Equote\_2EEmpty\_\_vm~\\
A\_27a))=(ap~(\mname{c\_2Emin\_2E\_40}~A\_27a)~({\uniddcgcg} V24x \in A\_27a .  \mname{c\_2Ebool\_2ET})))))))){\unicdcdcdhd}\\
((({\unicdcdadad} V25t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V26t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V27l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V28l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V29c2 \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V30c1 \in ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V30c1)~\\
V28l1)~V26t1))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V29c2)~V27l2)~V25t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V28l1)~V27l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V30c1)~\\
V28l1)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V26t1)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V29c2)~\\
V27l2)~V25t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V30c1)~V29c2))~V28l1)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
V26t1)~V25t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V29c2)~V27l2)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V30c1)~\\
V28l1)~V26t1))~V25t2)))))))))){\unicdcdcdhd}(({\unicdcdadad} V31t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V32t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V33l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V34l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V35c1 \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V35c1)~\\
V34l1)~V32t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V33l2)~V31t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V34l1)~V33l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V35c1)~\\
V34l1)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V32t1)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V33l2)~\\
V31t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V35c1)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V34l1)~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V32t1)~V31t2)))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V33l2)~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V35c1)~V34l1)~\\
V32t1))~V31t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V36t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V37t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V38l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V39l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V40c2 \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V39l1)~\\
V37t1))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V40c2)~V38l2)~V36t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V39l1)~V38l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V39l1)~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V37t1)~(ap~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V40c2)~\\
V38l2)~V36t2))))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V40c2))~V39l1)~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V37t1)~V36t2)))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V40c2)~\\
V38l2)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V39l1)~V37t1))~\\
V36t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V41t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V42t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V43l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V44l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Enum\_2Enum)~V44l1)~V42t1))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Enum\_2Enum)~V43l2)~V41t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V44l1)~V43l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V44l1)~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~V42t1)~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V43l2)~V41t2))))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~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}))))~V44l1)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
V42t1)~V41t2)))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V43l2)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V44l1)~V42t1))~\\
V41t2)))))))){\unicdcdcdhd}(({\unicdcdadad} V45s1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
V45s1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))=V45s1)){\unicdcdcdhd}\\
(({\unicdcdadad} V46v6 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V47v5 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V48v4 \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Enum\_2Enum)~V48v4)~V47v5)~V46v6))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Enum\_2Enum)~V48v4)~V47v5)~V46v6))))){\unicdcdcdhd}({\unicdcdadad} V49v8 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V50v7 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V50v7)~V49v8))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V50v7)~V49v8)))))))))){\unicdcdcdhd}((({\unicdcdadad} V51t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V52l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V53l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V54c2 \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V55c1 \in ty\_2Enum\_2Enum .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~\\
V55c1)~V53l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V54c2)~V52l2)~V51t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V53l1)~V52l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V55c1)~\\
V53l1)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V54c2)~V52l2)~V51t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Enum\_2Enum)~(ap~(ap~c\_2Earithmetic\_2E\_2B~V55c1)~V54c2))~V53l1)~\\
V51t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V54c2)~V52l2)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~V55c1)~\\
V53l1)~V51t2))))))))){\unicdcdcdhd}(({\unicdcdadad} V56t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V57l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V58l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V59c1 \in \\
ty\_2Enum\_2Enum .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~\\
V59c1)~V58l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V57l2)~V56t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V58l1)~V57l2))~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V59c1)~\\
V58l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V57l2)~V56t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~V59c1)~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~V58l1)~\\
V56t2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V57l2)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~V59c1)~V58l1)~\\
V56t2)))))))){\unicdcdcdhd}({\unicdcdadad} V60l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V61c1 \in ty\_2Enum\_2Enum .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~\\
V61c1)~V60l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))=\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V61c1)~\\
V60l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))))))){\unicdcdcdhd}\\
((({\unicdcdadad} V62t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V63l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V64l1 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V65c2 \in ty\_2Enum\_2Enum .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~V64l1)~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V65c2)~V63l2)~\\
V62t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V64l1)~V63l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V64l1)~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V65c2)~\\
V63l2)~V62t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
(ap~(ap~c\_2Earithmetic\_2E\_2B~(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\\
\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))~V65c2))~V64l1)~\\
V62t2))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V65c2)~V63l2)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~V64l1)~\\
V62t2)))))))){\unicdcdcdhd}(({\unicdcdadad} V66t2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V67l2 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V68l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~V68l1)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Enum\_2Enum)~V67l2)~V66t2))=(ap~(ap~(ap~(ap~(\mname{c\_2EternaryComparisons\_2Eordering\_\_CASE}~\\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum))~(ap~(ap~(\\
ap~(c\_2EternaryComparisons\_2Elist\_\_compare~ty\_2Equote\_2Eindex~\\
ty\_2Equote\_2Eindex)~c\_2Equote\_2Eindex\_\_compare)~V68l1)~V67l2))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V68l1)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V67l2)~\\
V66t2)))~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~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}))))~V68l1)~\\
V66t2))~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V67l2)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~V68l1)~V66t2))))))){\unicdcdcdhd}\\
({\unicdcdadad} V69l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~V69l1)~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V69l1)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum)))))){\unicdcdcdhd}(\\
(({\unicdcdadad} V70c0 \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V71c \in ty\_2Enum\_2Enum .  \\
({\unicdcdadad} V72l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V73t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  ((ap~(ap~\\
\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}~V70c0)~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V71c)~V72l)~V73t))=\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~(ap~\\
(ap~c\_2Earithmetic\_2E\_2A~V70c0)~V71c))~V72l)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}~\\
V70c0)~V73t))))))){\unicdcdcdhd}(({\unicdcdadad} V74c0 \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V75l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V76t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}~\\
V74c0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V75l)~V76t))=(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V74c0)~V75l)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}~\\
V74c0)~V76t)))))){\unicdcdcdhd}({\unicdcdadad} V77c0 \in ty\_2Enum\_2Enum .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar}~\\
V77c0)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))=(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))))){\unicdcdcdhd}((({\unicdcdadad} V78l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V79c \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V80l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V81t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~\\
V78l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V79c)~V80l)~V81t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~\\
V79c)~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V78l0)~V80l))~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~\\
V78l0)~V81t))))))){\unicdcdcdhd}(({\unicdcdadad} V82l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V83l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V84t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  ((ap~(ap~\\
\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~V82l0)~(ap~(ap~(\\
c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V83l)~V84t))=\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_varlist\_\_insert}~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
ty\_2Equote\_2Eindex)~\mname{c\_2Equote\_2Eindex\_\_lt})~V82l0)~V83l))~(ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~V82l0)~V84t)))))){\unicdcdcdhd}\\
({\unicdcdadad} V85l0 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~V85l0)~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))=(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))))){\unicdcdcdhd}\\
((({\unicdcdadad} V86c0 \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V87l0 \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V88c \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V89l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V90t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~\\
V86c0)~V87l0)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~\\
V88c)~V89l)~V90t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~\\
(ap~(ap~c\_2Earithmetic\_2E\_2A~V86c0)~V88c))~(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~\\
ty\_2Equote\_2Eindex)~\mname{c\_2Equote\_2Eindex\_\_lt})~V87l0)~V89l))~(ap~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~V86c0)~V87l0)~\\
V90t)))))))){\unicdcdcdhd}(({\unicdcdadad} V91c0 \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V92l0 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V93l \in (ty\_2Elist\_2Elist~\\
ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V94t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~\\
V91c0)~V92l0)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V93l)~V94t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_monom\_\_insert}~V91c0)~\\
(ap~(ap~(ap~(c\_2EternaryComparisons\_2Elist\_\_merge~ty\_2Equote\_2Eindex)~\\
\mname{c\_2Equote\_2Eindex\_\_lt})~V92l0)~V93l))~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~\\
V91c0)~V92l0)~V94t))))))){\unicdcdcdhd}({\unicdcdadad} V95c0 \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V96l0 \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~\\
V95c0)~V96l0)~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))=\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum)))))){\unicdcdcdhd}((({\unicdcdadad} V97c1 \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V98l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V99t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V100s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~(ap~(ap~(ap~\\
(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V97c1)~V98l1)~\\
V99t1))~V100s2)=(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar3}~V97c1)~\\
V98l1)~V100s2))~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~\\
V99t1)~V100s2))))))){\unicdcdcdhd}(({\unicdcdadad} V101l1 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V102t1 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V103s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Enum\_2Enum)~V101l1)~V102t1))~V103s2)=(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_scalar2}~V101l1)~\\
V103s2))~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~V102t1)~\\
V103s2)))))){\unicdcdcdhd}({\unicdcdadad} V104s2 \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))~V104s2)=(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))))){\unicdcdcdhd}((({\unicdcdadad} V105c \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V106l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V107t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~\\
(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V105c)~\\
V106l)~V107t))=(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~ty\_2Enum\_2Enum)~V105c)~\\
\mname{c\_2Enum\_2E0}))~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~\\
V107t))~(ap~(ap~(ap~(\mname{c\_2Ebool\_2ECOND}~(ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum))~(ap~(ap~(\mname{c\_2Emin\_2E\_3D}~ty\_2Enum\_2Enum)~V105c)~\\
(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO}))))~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V106l)~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~V107t)))~(\\
ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V105c)~\\
V106l)~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~V107t)))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V108l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V109t \in \\
(ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  ((ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V108l)~\\
V109t))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V108l)~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~V109t))))){\unicdcdcdhd}\\
((ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))=(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum)))){\unicdcdcdhd}\\
((({\unicdcdadad} V110vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V111x \in \\
ty\_2Equote\_2Eindex .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}~\\
V110vm)~V111x)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=(ap~(ap~\\
(c\_2Equote\_2Evarmap\_\_find~ty\_2Enum\_2Enum)~V111x)~V110vm)))){\unicdcdcdhd}\\
({\unicdcdadad} V112vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V113x \in \\
ty\_2Equote\_2Eindex .  ({\unicdcdadad} V114x\_27 \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V115t\_27 \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  (\\
(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}~V112vm)~V113x)~(ap~(ap~\\
(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V114x\_27)~V115t\_27))=\\
(ap~(ap~c\_2Earithmetic\_2E\_2A~(ap~(ap~(c\_2Equote\_2Evarmap\_\_find~\\
ty\_2Enum\_2Enum)~V113x)~V112vm))~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}~\\
V112vm)~V114x\_27)~V115t\_27)))))))){\unicdcdcdhd}((({\unicdcdadad} V116vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_vl}~V116vm)~\\
(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex))=(ap~\mname{c\_2Earithmetic\_2ENUMERAL}~\\
(ap~\mname{c\_2Earithmetic\_2EBIT1}~\mname{c\_2Earithmetic\_2EZERO})))){\unicdcdcdhd}({\unicdcdadad} V117vm \in \\
(ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V118x \in ty\_2Equote\_2Eindex .  \\
({\unicdcdadad} V119t \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ((ap~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_vl}~V117vm)~(ap~(ap~(c\_2Elist\_2ECONS~\\
ty\_2Equote\_2Eindex)~V118x)~V119t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}~\\
V117vm)~V118x)~V119t)))))){\unicdcdcdhd}((({\unicdcdadad} V120vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V121c \in ty\_2Enum\_2Enum .  ((ap~(ap~(ap~\\
\mname{c\_2EnumRing\_2Enum\_\_interp\_\_m}~V120vm)~V121c)~(c\_2Elist\_2ENIL~\\
ty\_2Equote\_2Eindex))=V121c))){\unicdcdcdhd}({\unicdcdadad} V122vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V123c \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V124x \in \\
ty\_2Equote\_2Eindex .  ({\unicdcdadad} V125t \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_m}~V122vm)~V123c)~(ap~(\\
ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~V124x)~V125t))=(ap~(\\
ap~c\_2Earithmetic\_2E\_2A~V123c)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ivl\_\_aux}~\\
V122vm)~V124x)~V125t)))))))){\unicdcdcdhd}((({\unicdcdadad} V126vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V127a \in ty\_2Enum\_2Enum .  ((ap~(ap~(ap~\\
\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~V126vm)~V127a)~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum))=V127a))){\unicdcdcdhd}(({\unicdcdadad} V128vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V129a \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V130l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V131t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~V128vm)~\\
V129a)~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~\\
V130l)~V131t))=(ap~(ap~c\_2Earithmetic\_2E\_2B~V129a)~(ap~(ap~(ap~\\
\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~V128vm)~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_vl}~\\
V128vm)~V130l))~V131t))))))){\unicdcdcdhd}({\unicdcdadad} V132vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ({\unicdcdadad} V133a \in ty\_2Enum\_2Enum .  ({\unicdcdadad} V134c \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V135l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V136t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
((ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~V132vm)~V133a)~(ap~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V134c)~V135l)~\\
V136t))=(ap~(ap~c\_2Earithmetic\_2E\_2B~V133a)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~\\
V132vm)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_m}~V132vm)~V134c)~\\
V135l))~V136t)))))))))){\unicdcdcdhd}((({\unicdcdadad} V137vm \in (ty\_2Equote\_2Evarmap~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_cs}~V137vm)~\\
(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum))=\mname{c\_2Enum\_2E0})){\unicdcdcdhd}\\
(({\unicdcdadad} V138vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V139l \in \\
(ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  ({\unicdcdadad} V140t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~\\
ty\_2Enum\_2Enum) .  ((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_cs}~V138vm)~\\
(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~ty\_2Enum\_2Enum)~V139l)~\\
V140t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~V138vm)~(ap~(\\
ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_vl}~V138vm)~V139l))~V140t))))){\unicdcdcdhd}\\
({\unicdcdadad} V141vm \in (ty\_2Equote\_2Evarmap~ty\_2Enum\_2Enum) .  ({\unicdcdadad} V142c \in \\
ty\_2Enum\_2Enum .  ({\unicdcdadad} V143l \in (ty\_2Elist\_2Elist~ty\_2Equote\_2Eindex) .  \\
({\unicdcdadad} V144t \in (ty\_2Ecanonical\_2Ecanonical\_\_sum~ty\_2Enum\_2Enum) .  \\
((ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_cs}~V141vm)~(ap~(ap~(ap~(c\_2Ecanonical\_2ECons\_\_monom~\\
ty\_2Enum\_2Enum)~V142c)~V143l)~V144t))=(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_ics\_\_aux}~\\
V141vm)~(ap~(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_interp\_\_m}~V141vm)~V142c)~\\
V143l))~V144t)))))))){\unicdcdcdhd}((({\unicdcdadad} V145i \in ty\_2Equote\_2Eindex .  \\
((ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~(ap~(c\_2Ecanonical\_2ESPvar~\\
ty\_2Enum\_2Enum)~V145i))=(ap~(ap~(c\_2Ecanonical\_2ECons\_\_varlist~\\
ty\_2Enum\_2Enum)~(ap~(ap~(c\_2Elist\_2ECONS~ty\_2Equote\_2Eindex)~\\
V145i)~(c\_2Elist\_2ENIL~ty\_2Equote\_2Eindex)))~(c\_2Ecanonical\_2ENil\_\_monom~\\
ty\_2Enum\_2Enum)))){\unicdcdcdhd}(({\unicdcdadad} V146c \in ty\_2Enum\_2Enum .  ((ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~\\
(ap~(c\_2Ecanonical\_2ESPconst~ty\_2Enum\_2Enum)~V146c))=(ap~(ap~\\
(ap~(c\_2Ecanonical\_2ECons\_\_monom~ty\_2Enum\_2Enum)~V146c)~(c\_2Elist\_2ENIL~\\
ty\_2Equote\_2Eindex))~(c\_2Ecanonical\_2ENil\_\_monom~ty\_2Enum\_2Enum)))){\unicdcdcdhd}\\
(({\unicdcdadad} V147l \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V148r \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
((ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~(ap~(ap~(c\_2Ecanonical\_2ESPplus~\\
ty\_2Enum\_2Enum)~V147l)~V148r))=(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_merge}~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~V147l))~(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~\\
V148r))))){\unicdcdcdhd}({\unicdcdadad} V149l \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
({\unicdcdadad} V150r \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
((ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~(ap~(ap~(c\_2Ecanonical\_2ESPmult~\\
ty\_2Enum\_2Enum)~V149l)~V150r))=(ap~(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_prod}~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~V149l))~(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~\\
V150r)))))))){\unicdcdcdhd}({\unicdcdadad} V151x \in (ty\_2Ecanonical\_2Espolynom~ty\_2Enum\_2Enum) .  \\
((ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_simplify}~V151x)=(ap~\mname{c\_2EnumRing\_2Enum\_\_canonical\_\_sum\_\_simplify}~\\
(ap~\mname{c\_2EnumRing\_2Enum\_\_spolynom\_\_normalize}~V151x)))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
