\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{t27\_descip\_1 (TMZKS1AH6Ubv8WkrVHShPbKMH7NNSXWGnk8)}
\maketitle
Let $ np\_\_64 : {\iota}$ be given.
Let $ k6\_numbers : {\iota}$ be given.
Let $ np\_\_1 : {\iota}$ be given.
Let $ np\_\_2 : {\iota}$ be given.
Let $ np\_\_3 : {\iota}$ be given.
Let $ np\_\_4 : {\iota}$ be given.
Let $ np\_\_5 : {\iota}$ be given.
Let $ np\_\_6 : {\iota}$ be given.
Let $ np\_\_7 : {\iota}$ be given.
Let $ np\_\_8 : {\iota}$ be given.
Let $ np\_\_9 : {\iota}$ be given.
Let $ np\_\_10 : {\iota}$ be given.
Let $ np\_\_11 : {\iota}$ be given.
Let $ np\_\_12 : {\iota}$ be given.
Let $ np\_\_13 : {\iota}$ be given.
Let $ np\_\_14 : {\iota}$ be given.
Let $ np\_\_15 : {\iota}$ be given.
Let $ np\_\_16 : {\iota}$ be given.
Let $ np\_\_17 : {\iota}$ be given.
Let $ np\_\_18 : {\iota}$ be given.
Let $ np\_\_19 : {\iota}$ be given.
Let $ np\_\_20 : {\iota}$ be given.
Let $ np\_\_21 : {\iota}$ be given.
Let $ np\_\_22 : {\iota}$ be given.
Let $ np\_\_23 : {\iota}$ be given.
Let $ np\_\_24 : {\iota}$ be given.
Let $ np\_\_25 : {\iota}$ be given.
Let $ np\_\_26 : {\iota}$ be given.
Let $ np\_\_27 : {\iota}$ be given.
Let $ np\_\_28 : {\iota}$ be given.
Let $ np\_\_29 : {\iota}$ be given.
Let $ np\_\_30 : {\iota}$ be given.
Let $ np\_\_31 : {\iota}$ be given.
Let $ np\_\_32 : {\iota}$ be given.
Let $ np\_\_33 : {\iota}$ be given.
Let $ np\_\_34 : {\iota}$ be given.
Let $ np\_\_35 : {\iota}$ be given.
Let $ np\_\_36 : {\iota}$ be given.
Let $ np\_\_37 : {\iota}$ be given.
Let $ np\_\_38 : {\iota}$ be given.
Let $ np\_\_39 : {\iota}$ be given.
Let $ np\_\_40 : {\iota}$ be given.
Let $ np\_\_41 : {\iota}$ be given.
Let $ np\_\_42 : {\iota}$ be given.
Let $ np\_\_43 : {\iota}$ be given.
Let $ np\_\_44 : {\iota}$ be given.
Let $ np\_\_45 : {\iota}$ be given.
Let $ np\_\_46 : {\iota}$ be given.
Let $ np\_\_47 : {\iota}$ be given.
Let $ np\_\_48 : {\iota}$ be given.
Let $ np\_\_49 : {\iota}$ be given.
Let $ np\_\_50 : {\iota}$ be given.
Let $ np\_\_51 : {\iota}$ be given.
Let $ np\_\_52 : {\iota}$ be given.
Let $ np\_\_53 : {\iota}$ be given.
Let $ np\_\_54 : {\iota}$ be given.
Let $ np\_\_55 : {\iota}$ be given.
Let $ np\_\_56 : {\iota}$ be given.
Let $ np\_\_57 : {\iota}$ be given.
Let $ np\_\_58 : {\iota}$ be given.
Let $ np\_\_59 : {\iota}$ be given.
Let $ np\_\_60 : {\iota}$ be given.
Let $ np\_\_61 : {\iota}$ be given.
Let $ np\_\_62 : {\iota}$ be given.
Let $ np\_\_63 : {\iota}$ be given.
Let $ v7\_ordinal1 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ v1\_xboole\_0 : {{\iota}{\unicdbdjdcd}{o}}$ be given.
Let $ k2\_finseq\_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 $ k4\_ordinal1 : {\iota}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  ((v7\_ordinal1~X0){\unicdcdcdhd}(\preoh v1\_xboole\_0~X0)){\unicdbdjdcd}({\unicdcdadad} X1 .  \\
\preoh (X1 \in X0){\unicdcdcdhd}((X1{\unicdcdgdad}k6\_numbers){\unicdcdcdhd}(\preoh (X1 \in k2\_finseq\_1~X0){\unicdcdcdhd}(X1{\unicdcdgdad}X0))))\end{array}
\label{hyp:ehcdfdpfegfgdhdgjgahpfbd}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} X0 .  \preoh (X0 \in k2\_finseq\_1~np\_\_64){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_1){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_2){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_3){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_4){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_5){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_6){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_7){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_8){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_9){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_10){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_11){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_12){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_13){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_14){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_15){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_16){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_17){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_18){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_19){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_20){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_21){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_22){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_23){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_24){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_25){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_26){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_27){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_28){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_29){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_30){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_31){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_32){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_33){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_34){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_35){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_36){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_37){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_38){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_39){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_40){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_41){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_42){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_43){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_44){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_45){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_46){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_47){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_48){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_49){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_50){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_51){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_52){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_53){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_54){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_55){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_56){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_57){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_58){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_59){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_60){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_61){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_62){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_63){\unicdcdcdhd}(X0{\unicdcdgdad}np\_\_64))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}
\label{hyp:ehcdddpfegfgdhdgjgahpfbd}
\end{equation}
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}
{\preoh{{{v1\_xboole\_0}~{np\_\_64}}}}\label{hyp:dhahdggdedpfcgpgpgmgfg}
\end{equation}
Assume the following.
\begin{equation}
{{k5\_numbers}={k4\_ordinal1}}\label{hyp:chfgegfgggjgogjgehjgpgogpflgfdpfogfhngcgfgchdh}
\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:ehcdhdpfegfgdhdgjgahpfbd}
$$\begin{array}{c}{\unicdcdadad} X0 .  \preoh (X0 \in np\_\_64){\unicdcdcdhd}((X0{\unicdcdgdad}k6\_numbers){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_1){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_2){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_3){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_4){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_5){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_6){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_7){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_8){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_9){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_10){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_11){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_12){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_13){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_14){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_15){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_16){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_17){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_18){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_19){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_20){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_21){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_22){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_23){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_24){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_25){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_26){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_27){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_28){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_29){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_30){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_31){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_32){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_33){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_34){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_35){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_36){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_37){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_38){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_39){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_40){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_41){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_42){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_43){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_44){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_45){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_46){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_47){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_48){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_49){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_50){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_51){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_52){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_53){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_54){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_55){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_56){\unicdcdcdhd}\\
((X0{\unicdcdgdad}np\_\_57){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_58){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_59){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_60){\unicdcdcdhd}((X0{\unicdcdgdad}\\
np\_\_61){\unicdcdcdhd}((X0{\unicdcdgdad}np\_\_62){\unicdcdcdhd}(X0{\unicdcdgdad}np\_\_63))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
