\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{l72\_descip\_1 (TMH5FWPZTjji5BGGNGGRGfwEE61gdFYpiXV)}
\maketitle
Let $ m2\_finseq\_2 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}}$ be given.
Let $ k6\_margrel1 : {\iota}$ be given.
Let $ k4\_finseq\_2 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Let $ np\_\_64 : {\iota}$ be given.
Let $ k25\_descip\_1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Let $ k27\_descip\_1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Let $ v2\_xxreal\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ m2\_subset\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}}$ be given.
Let $ k1\_numbers : {\iota}$ be given.
Let $ k5\_numbers : {\iota}$ be given.
Let $ m1\_subset\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}$ be given.
Let $ m1\_finseq\_2 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{o}}}$ be given.
Let $ k4\_ordinal1 : {\iota}$ be given.
Let $ v7\_ordinal1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k10\_descip\_1 : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}}$ be given.
Let $ np\_\_1 : {\iota}$ be given.
Let $ np\_\_40 : {\iota}$ be given.
Let $ np\_\_2 : {\iota}$ be given.
Let $ np\_\_8 : {\iota}$ be given.
Let $ np\_\_3 : {\iota}$ be given.
Let $ np\_\_48 : {\iota}$ be given.
Let $ np\_\_4 : {\iota}$ be given.
Let $ np\_\_16 : {\iota}$ be given.
Let $ np\_\_5 : {\iota}$ be given.
Let $ np\_\_56 : {\iota}$ be given.
Let $ np\_\_6 : {\iota}$ be given.
Let $ np\_\_24 : {\iota}$ be given.
Let $ np\_\_7 : {\iota}$ be given.
Let $ np\_\_32 : {\iota}$ be given.
Let $ np\_\_9 : {\iota}$ be given.
Let $ np\_\_39 : {\iota}$ be given.
Let $ np\_\_10 : {\iota}$ be given.
Let $ np\_\_11 : {\iota}$ be given.
Let $ np\_\_47 : {\iota}$ be given.
Let $ np\_\_12 : {\iota}$ be given.
Let $ np\_\_15 : {\iota}$ be given.
Let $ np\_\_13 : {\iota}$ be given.
Let $ np\_\_55 : {\iota}$ be given.
Let $ np\_\_14 : {\iota}$ be given.
Let $ np\_\_23 : {\iota}$ be given.
Let $ np\_\_63 : {\iota}$ be given.
Let $ np\_\_31 : {\iota}$ be given.
Let $ np\_\_17 : {\iota}$ be given.
Let $ np\_\_38 : {\iota}$ be given.
Let $ np\_\_18 : {\iota}$ be given.
Let $ np\_\_19 : {\iota}$ be given.
Let $ np\_\_46 : {\iota}$ be given.
Let $ np\_\_20 : {\iota}$ be given.
Let $ np\_\_21 : {\iota}$ be given.
Let $ np\_\_54 : {\iota}$ be given.
Let $ np\_\_22 : {\iota}$ be given.
Let $ np\_\_62 : {\iota}$ be given.
Let $ np\_\_30 : {\iota}$ be given.
Let $ np\_\_25 : {\iota}$ be given.
Let $ np\_\_37 : {\iota}$ be given.
Let $ np\_\_26 : {\iota}$ be given.
Let $ np\_\_27 : {\iota}$ be given.
Let $ np\_\_45 : {\iota}$ be given.
Let $ np\_\_28 : {\iota}$ be given.
Let $ np\_\_29 : {\iota}$ be given.
Let $ np\_\_53 : {\iota}$ be given.
Let $ np\_\_61 : {\iota}$ be given.
Let $ np\_\_33 : {\iota}$ be given.
Let $ np\_\_36 : {\iota}$ be given.
Let $ np\_\_34 : {\iota}$ be given.
Let $ np\_\_35 : {\iota}$ be given.
Let $ np\_\_44 : {\iota}$ be given.
Let $ np\_\_52 : {\iota}$ be given.
Let $ np\_\_60 : {\iota}$ be given.
Let $ np\_\_41 : {\iota}$ be given.
Let $ np\_\_42 : {\iota}$ be given.
Let $ np\_\_43 : {\iota}$ be given.
Let $ np\_\_51 : {\iota}$ be given.
Let $ np\_\_59 : {\iota}$ be given.
Let $ np\_\_49 : {\iota}$ be given.
Let $ np\_\_50 : {\iota}$ be given.
Let $ np\_\_58 : {\iota}$ be given.
Let $ np\_\_57 : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}((v2\_xxreal\_0~np\_\_64){\unicdcdcdhd}(m2\_subset\_1~np\_\_64~k1\_numbers~k5\_numbers)){\unicdcdcdhd}\\
((m1\_subset\_1~np\_\_64~k5\_numbers){\unicdcdcdhd}(m1\_subset\_1~np\_\_64~k1\_numbers))\end{array}
\label{hyp:dhahdggdedpfogfhngfgchbgmgdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  (m1\_finseq\_2~X1~X0){\unicdbdjdcd}({\unicdcdadad} X2 .  (m2\_finseq\_2~\\
X2~X0~X1){\unicdbdjded}(m1\_subset\_1~X2~X1))\end{array}
\label{hyp:chfgegfgggjgogjgehjgpgogpfngcdpfggjgogdhfgbhpfcd}
\end{equation}
Assume the following.
\begin{equation}
{{k5\_numbers}={k4\_ordinal1}}\label{hyp:chfgegfgggjgogjgehjgpgogpflgfdpfogfhngcgfgchdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  {\unicdcdadad} X1 .  (v7\_ordinal1~X0){\unicdbdjdcd}(m1\_finseq\_2~(k4\_finseq\_2~\\
X0~X1)~X1)\end{array}
\label{hyp:egehpflgedpfggjgogdhfgbhpfcd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (m1\_subset\_1~X0~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
(m2\_finseq\_2~(k27\_descip\_1~X0)~k6\_margrel1~(k4\_finseq\_2~np\_\_64~\\
k6\_margrel1))\end{array}
\label{hyp:egehpflgcdhdpfegfgdhdgjgahpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (m2\_finseq\_2~X0~k6\_margrel1~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
({\unicdcdadad} X1 .  (m2\_finseq\_2~X1~k6\_margrel1~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
((X1=k27\_descip\_1~X0){\unicdbdjded}((k10\_descip\_1~np\_\_64~X1~np\_\_1=k10\_descip\_1~\\
np\_\_64~X0~np\_\_40){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_2=k10\_descip\_1~\\
np\_\_64~X0~np\_\_8){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_3=k10\_descip\_1~\\
np\_\_64~X0~np\_\_48){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_4=k10\_descip\_1~\\
np\_\_64~X0~np\_\_16){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_5=k10\_descip\_1~\\
np\_\_64~X0~np\_\_56){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_6=k10\_descip\_1~\\
np\_\_64~X0~np\_\_24){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_7=k10\_descip\_1~\\
np\_\_64~X0~np\_\_64){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_8=k10\_descip\_1~\\
np\_\_64~X0~np\_\_32){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_9=k10\_descip\_1~\\
np\_\_64~X0~np\_\_39){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_10=k10\_descip\_1~\\
np\_\_64~X0~np\_\_7){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_11=k10\_descip\_1~\\
np\_\_64~X0~np\_\_47){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_12=k10\_descip\_1~\\
np\_\_64~X0~np\_\_15){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_13=k10\_descip\_1~\\
np\_\_64~X0~np\_\_55){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_14=k10\_descip\_1~\\
np\_\_64~X0~np\_\_23){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_15=k10\_descip\_1~\\
np\_\_64~X0~np\_\_63){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_16=k10\_descip\_1~\\
np\_\_64~X0~np\_\_31){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_17=k10\_descip\_1~\\
np\_\_64~X0~np\_\_38){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_18=k10\_descip\_1~\\
np\_\_64~X0~np\_\_6){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_19=k10\_descip\_1~\\
np\_\_64~X0~np\_\_46){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_20=k10\_descip\_1~\\
np\_\_64~X0~np\_\_14){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_21=k10\_descip\_1~\\
np\_\_64~X0~np\_\_54){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_22=k10\_descip\_1~\\
np\_\_64~X0~np\_\_22){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_23=k10\_descip\_1~\\
np\_\_64~X0~np\_\_62){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_24=k10\_descip\_1~\\
np\_\_64~X0~np\_\_30){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_25=k10\_descip\_1~\\
np\_\_64~X0~np\_\_37){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_26=k10\_descip\_1~\\
np\_\_64~X0~np\_\_5){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_27=k10\_descip\_1~\\
np\_\_64~X0~np\_\_45){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_28=k10\_descip\_1~\\
np\_\_64~X0~np\_\_13){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_29=k10\_descip\_1~\\
np\_\_64~X0~np\_\_53){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_30=k10\_descip\_1~\\
np\_\_64~X0~np\_\_21){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_31=k10\_descip\_1~\\
np\_\_64~X0~np\_\_61){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_32=k10\_descip\_1~\\
np\_\_64~X0~np\_\_29){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_33=k10\_descip\_1~\\
np\_\_64~X0~np\_\_36){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_34=k10\_descip\_1~\\
np\_\_64~X0~np\_\_4){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_35=k10\_descip\_1~\\
np\_\_64~X0~np\_\_44){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_36=k10\_descip\_1~\\
np\_\_64~X0~np\_\_12){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_37=k10\_descip\_1~\\
np\_\_64~X0~np\_\_52){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_38=k10\_descip\_1~\\
np\_\_64~X0~np\_\_20){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_39=k10\_descip\_1~\\
np\_\_64~X0~np\_\_60){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_40=k10\_descip\_1~\\
np\_\_64~X0~np\_\_28){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_41=k10\_descip\_1~\\
np\_\_64~X0~np\_\_35){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_42=k10\_descip\_1~\\
np\_\_64~X0~np\_\_3){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_43=k10\_descip\_1~\\
np\_\_64~X0~np\_\_43){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_44=k10\_descip\_1~\\
np\_\_64~X0~np\_\_11){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_45=k10\_descip\_1~\\
np\_\_64~X0~np\_\_51){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_46=k10\_descip\_1~\\
np\_\_64~X0~np\_\_19){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_47=k10\_descip\_1~\\
np\_\_64~X0~np\_\_59){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_48=k10\_descip\_1~\\
np\_\_64~X0~np\_\_27){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_49=k10\_descip\_1~\\
np\_\_64~X0~np\_\_34){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_50=k10\_descip\_1~\\
np\_\_64~X0~np\_\_2){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_51=k10\_descip\_1~\\
np\_\_64~X0~np\_\_42){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_52=k10\_descip\_1~\\
np\_\_64~X0~np\_\_10){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_53=k10\_descip\_1~\\
np\_\_64~X0~np\_\_50){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_54=k10\_descip\_1~\\
np\_\_64~X0~np\_\_18){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_55=k10\_descip\_1~\\
np\_\_64~X0~np\_\_58){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_56=k10\_descip\_1~\\
np\_\_64~X0~np\_\_26){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_57=k10\_descip\_1~\\
np\_\_64~X0~np\_\_33){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_58=k10\_descip\_1~\\
np\_\_64~X0~np\_\_1){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_59=k10\_descip\_1~\\
np\_\_64~X0~np\_\_41){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_60=k10\_descip\_1~\\
np\_\_64~X0~np\_\_9){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_61=k10\_descip\_1~\\
np\_\_64~X0~np\_\_49){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_62=k10\_descip\_1~\\
np\_\_64~X0~np\_\_17){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_63=k10\_descip\_1~\\
np\_\_64~X0~np\_\_57){\unicdcdcdhd}(k10\_descip\_1~np\_\_64~X1~np\_\_64=k10\_descip\_1~\\
np\_\_64~X0~np\_\_25))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}
\label{hyp:egbdgdpfegfgdhdgjgahpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  (m2\_finseq\_2~X0~k6\_margrel1~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
({\unicdcdadad} X1 .  (m2\_finseq\_2~X1~k6\_margrel1~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
((X1=k25\_descip\_1~X0){\unicdbdjded}((k10\_descip\_1~np\_\_64~X1~np\_\_1=k10\_descip\_1~\\
np\_\_64~X0~np\_\_58){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_2=k10\_descip\_1~\\
np\_\_64~X0~np\_\_50){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_3=k10\_descip\_1~\\
np\_\_64~X0~np\_\_42){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_4=k10\_descip\_1~\\
np\_\_64~X0~np\_\_34){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_5=k10\_descip\_1~\\
np\_\_64~X0~np\_\_26){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_6=k10\_descip\_1~\\
np\_\_64~X0~np\_\_18){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_7=k10\_descip\_1~\\
np\_\_64~X0~np\_\_10){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_8=k10\_descip\_1~\\
np\_\_64~X0~np\_\_2){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_9=k10\_descip\_1~\\
np\_\_64~X0~np\_\_60){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_10=k10\_descip\_1~\\
np\_\_64~X0~np\_\_52){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_11=k10\_descip\_1~\\
np\_\_64~X0~np\_\_44){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_12=k10\_descip\_1~\\
np\_\_64~X0~np\_\_36){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_13=k10\_descip\_1~\\
np\_\_64~X0~np\_\_28){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_14=k10\_descip\_1~\\
np\_\_64~X0~np\_\_20){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_15=k10\_descip\_1~\\
np\_\_64~X0~np\_\_12){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_16=k10\_descip\_1~\\
np\_\_64~X0~np\_\_4){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_17=k10\_descip\_1~\\
np\_\_64~X0~np\_\_62){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_18=k10\_descip\_1~\\
np\_\_64~X0~np\_\_54){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_19=k10\_descip\_1~\\
np\_\_64~X0~np\_\_46){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_20=k10\_descip\_1~\\
np\_\_64~X0~np\_\_38){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_21=k10\_descip\_1~\\
np\_\_64~X0~np\_\_30){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_22=k10\_descip\_1~\\
np\_\_64~X0~np\_\_22){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_23=k10\_descip\_1~\\
np\_\_64~X0~np\_\_14){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_24=k10\_descip\_1~\\
np\_\_64~X0~np\_\_6){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_25=k10\_descip\_1~\\
np\_\_64~X0~np\_\_64){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_26=k10\_descip\_1~\\
np\_\_64~X0~np\_\_56){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_27=k10\_descip\_1~\\
np\_\_64~X0~np\_\_48){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_28=k10\_descip\_1~\\
np\_\_64~X0~np\_\_40){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_29=k10\_descip\_1~\\
np\_\_64~X0~np\_\_32){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_30=k10\_descip\_1~\\
np\_\_64~X0~np\_\_24){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_31=k10\_descip\_1~\\
np\_\_64~X0~np\_\_16){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_32=k10\_descip\_1~\\
np\_\_64~X0~np\_\_8){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_33=k10\_descip\_1~\\
np\_\_64~X0~np\_\_57){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_34=k10\_descip\_1~\\
np\_\_64~X0~np\_\_49){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_35=k10\_descip\_1~\\
np\_\_64~X0~np\_\_41){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_36=k10\_descip\_1~\\
np\_\_64~X0~np\_\_33){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_37=k10\_descip\_1~\\
np\_\_64~X0~np\_\_25){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_38=k10\_descip\_1~\\
np\_\_64~X0~np\_\_17){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_39=k10\_descip\_1~\\
np\_\_64~X0~np\_\_9){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_40=k10\_descip\_1~\\
np\_\_64~X0~np\_\_1){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_41=k10\_descip\_1~\\
np\_\_64~X0~np\_\_59){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_42=k10\_descip\_1~\\
np\_\_64~X0~np\_\_51){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_43=k10\_descip\_1~\\
np\_\_64~X0~np\_\_43){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_44=k10\_descip\_1~\\
np\_\_64~X0~np\_\_35){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_45=k10\_descip\_1~\\
np\_\_64~X0~np\_\_27){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_46=k10\_descip\_1~\\
np\_\_64~X0~np\_\_19){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_47=k10\_descip\_1~\\
np\_\_64~X0~np\_\_11){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_48=k10\_descip\_1~\\
np\_\_64~X0~np\_\_3){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_49=k10\_descip\_1~\\
np\_\_64~X0~np\_\_61){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_50=k10\_descip\_1~\\
np\_\_64~X0~np\_\_53){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_51=k10\_descip\_1~\\
np\_\_64~X0~np\_\_45){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_52=k10\_descip\_1~\\
np\_\_64~X0~np\_\_37){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_53=k10\_descip\_1~\\
np\_\_64~X0~np\_\_29){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_54=k10\_descip\_1~\\
np\_\_64~X0~np\_\_21){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_55=k10\_descip\_1~\\
np\_\_64~X0~np\_\_13){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_56=k10\_descip\_1~\\
np\_\_64~X0~np\_\_5){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_57=k10\_descip\_1~\\
np\_\_64~X0~np\_\_63){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_58=k10\_descip\_1~\\
np\_\_64~X0~np\_\_55){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_59=k10\_descip\_1~\\
np\_\_64~X0~np\_\_47){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_60=k10\_descip\_1~\\
np\_\_64~X0~np\_\_39){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_61=k10\_descip\_1~\\
np\_\_64~X0~np\_\_31){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_62=k10\_descip\_1~\\
np\_\_64~X0~np\_\_23){\unicdcdcdhd}((k10\_descip\_1~np\_\_64~X1~np\_\_63=k10\_descip\_1~\\
np\_\_64~X0~np\_\_15){\unicdcdcdhd}(k10\_descip\_1~np\_\_64~X1~np\_\_64=k10\_descip\_1~\\
np\_\_64~X0~np\_\_7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}
\label{hyp:egbdedpfegfgdhdgjgahpfbd}
\end{equation}
Assume the following.
\begin{equation}
{{\unicdcdadad} X0 .  {{({{{m1\_subset\_1}~{X0}}~{k4\_ordinal1}})}{\unicdbdjdcd}{({{v7\_ordinal1}~{X0}})}}}\label{hyp:dgdgidpfpgchegjgogbgmgbd}
\end{equation}
\begin{theorem}\label{thm:mghdcdpfegfgdhdgjgahpfbd}
$$\begin{array}{c}{\unicdcdadad} X0 .  (m2\_finseq\_2~X0~k6\_margrel1~(k4\_finseq\_2~np\_\_64~k6\_margrel1)){\unicdbdjdcd}\\
(k25\_descip\_1~(k27\_descip\_1~X0)=X0)\end{array}$$
\end{theorem}
\end{document}
