\chapter{Recursion on Sets}
\section{EpsilonRec\_i}\label{feahdhjgmgpgogcffgdgpfjg}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfjg}
$\mname{In\_rec\_i}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & fac413e747a57408ad38b3855d3cde8673f86206e95ccdadff2b5babaf0c219e \\
Pure Object Address: & TMNdra6FF88BaWZhLQWoMVGDVkGgU5xZ1Px \\
Theory Object Id: & 93aac4fb93be5cc13a42b363fb830917e096fe0d5b269d4cae1a2675fc6fe442 \\
Theory Object Address: & TMKBpYHnteFb5wpr6cJ5KfTg3HrzRoSBByu
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp11:gech}
\end{equation}
\begin{verbatim}
In_rec_i_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfjgpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_i}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_i}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1106536fa01b17bf5ad01765e95f74fb2d59af6f6540159757750d84c1f699ae \\
Pure Prop Address: & TMS4niVmsvQx9jqComxMJ15nwcNzZqmdhRN \\
Theory Prop Id: & e8653b0bcd75b2d7d06c38f2ac4c66b817c99e8dc96d2647bd2daaee681a632e \\
Theory Prop Address: & TMbKwV8D2cMfE3R9MZ8SdtrUWVk2FfWMq91
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_ii}\label{feahdhjgmgpgogcffgdgpfjgjg}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{\iota}})}})}\unicdbdjdcd{({{\iota}\unicdbdjdcd{\iota}})}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfjgjg}
$\mname{In\_rec\_ii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{\iota}})}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f3c9abbc5074c0d68e744893a170de526469426a5e95400ae7fc81f74f412f7e \\
Pure Object Address: & TMKaBL68miPaU3awFWxavJ9vpffruAuJG6m \\
Theory Object Id: & 3841bd9652360e3358d466fb36d771d47d765b56ce11b4a446e1c8ee7792319a \\
Theory Object Address: & TMVfeCfjKozKnhDvd1g6ayuJytZPUtNbSQT
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{\iota}})}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp12:gech}
\end{equation}
\begin{verbatim}
In_rec_ii_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfjgjgpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_ii}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_ii}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f7aff626beae77fbb87e16d4b62b6dbf1d4e1fc8b4151ab95e33ff0a7eece1fd \\
Pure Prop Address: & TMc1r8kDpq8yTVrxstWVdBTkGu4bAHa2KqZ \\
Theory Prop Id: & 7bb1e907bd4a595013dd5253579a59ded78c5fc86a4aba5c0e6af261615e64e4 \\
Theory Prop Address: & TMF2cwdAE8DvbpFHHjfMdf7jfwBbgauH5K1
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_iii}\label{feahdhjgmgpgogcffgdgpfjgjgjg}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}})}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfjgjgjg}
$\mname{In\_rec\_iii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9b3a85b85e8269209d0ca8bf18ef658e56f967161bf5b7da5e193d24d345dd06 \\
Pure Object Address: & TMGS3HxzKZpy47SjRNptZvfW3hGeTR87kw8 \\
Theory Object Id: & 651077708696fee3d23e186d6ab9c1805fc9c46eb287174c7c7726c14df5cd25 \\
Theory Object Address: & TMNNG5ehc1kjbSr79hs1JoXieVRroM54amr
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp13:gech}
\end{equation}
\begin{verbatim}
In_rec_iii_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfjgjgjgpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_iii}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_iii}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5f0574ebbeaebb60edd0cf70b9e3649d00e8391b36dc79f8abc40b36f0236f5d \\
Pure Prop Address: & TMLw55kNTBuMX9fEZ9ucafMGa8X9q9Vg5AS \\
Theory Prop Id: & a0709d7e1ee7e89fa5e406d74c01159f7bc4a43f2d6eb3aecf054a5c987acced \\
Theory Prop Address: & TMe1LiqcZFAP9bdmQLTeizcNBRHbFYkJKz8
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_iio}\label{feahdhjgmgpgogcffgdgpfjgjgpg}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}})}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfjgjgpg}
$\mname{In\_rec\_iio}$ is the opaque object of type ${{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8465061e06db87ff5ec9bf4bd2245a29d557f6b265478036bee39419282a5e28 \\
Pure Object Address: & TMKaaHZBwQLEGRN8PYDKcEfwZubgSevskVz \\
Theory Object Id: & ebf7a42862e5ae14b0b042ad0dd80452de3ad1c5e8e168f4b1ab3d2fb945f61e \\
Theory Object Address: & TMLjGqbKQQthLSzLhyZ5N8iPmocUeVoLr3N
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp14:gech}
\end{equation}
\begin{verbatim}
In_rec_iio_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfjgjgpgpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_iio}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_iio}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6bb8bb1ff02720df380edef1d6e1599715ed907c141a8134c85b26a0a245f9b \\
Pure Prop Address: & TMG9Ak4owSMXtiyYkh2BpkesWY7gR3RoFCu \\
Theory Prop Id: & bff321513dbb1d418dd4c5d50b267215cb2c98cc7e1db5de1c7148e57ce1044d \\
Theory Prop Address: & TMZyTR9yto8MPdDZTwmCg5y3krsPUWxxW6u
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_Vo1}\label{feahdhjgmgpgogcffgdgpfgfpgbd}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{Vo}~{1}}})}\unicdbdjdcd{{Vo}~{1}}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfgfpgbd}
$\mname{In\_rec\_Vo1}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{Vo}~{1}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e9c5f22f769cd18d0d29090a943f66f6006f0d132fafe90f542ee2ee8a3f7b59 \\
Pure Object Address: & TMF7xrRrqMjz5Lk6579gDvuGzGVm7S7Xbm3 \\
Theory Object Id: & b1f6ea77e17286f0717ab97435a1b23d6c4cd8a5a8d1718c6bbe022c543fe9b5 \\
Theory Object Address: & TMRg5yF9XnKxQKRqe5XeJ2UENC7Gurp2pax
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{{Vo}~{1}}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp15:gech}
\end{equation}
\begin{verbatim}
In_rec_Vo1_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfgfpgbdpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_Vo1}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_Vo1}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fa315696609285c33f1dd6bb13f004c898139dd9c5a7f4d65239606647d55821 \\
Pure Prop Address: & TMKzEyM3ak62ud6SUpQnDC1eNXkY9NiztW3 \\
Theory Prop Id: & 69f9607db0c116ec22508e0bbe3620d5741374de361719968ce5a7a509dfca8c \\
Theory Prop Address: & TMUP4D2yi5VENpkASUcnEs47UeEw4yGYhCw
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_Vo2}\label{feahdhjgmgpgogcffgdgpfgfpgcd}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{Vo}~{2}}})}\unicdbdjdcd{{Vo}~{2}}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfgfpgcd}
$\mname{In\_rec\_Vo2}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{Vo}~{2}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8bc8d37461c7653ced731399d140c0d164fb9231e77b2824088e534889c31596 \\
Pure Object Address: & TMJV2odr76mGWeyBRTv7gyjmWSSMGzGy4vj \\
Theory Object Id: & b67f4be4f70efe3a08c8984e82e3f0ace6bc31b42132285fbf626d533ad4a46e \\
Theory Object Address: & TMMQWnTTmxXXX8n9NmHW2iCY3E2PWon4Gh3
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{{Vo}~{2}}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp16:gech}
\end{equation}
\begin{verbatim}
In_rec_Vo2_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogpfchfgdgpfgfpgcdpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_Vo2}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_Vo2}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1386f49a7aeb74994677ac4425fbfe5622be81d9fd2ba5678dc74f1e60cbc108 \\
Pure Prop Address: & TMZt6xCkE5e2YHuk9kBiQSM7r1AC1Cp8HNJ \\
Theory Prop Id: & 573f9327980a8c0f52e474888757973c754fdd9f151a1b366673a160168ba0cb \\
Theory Prop Address: & TMGqV65crtJCaDQBUgBqHQbtxYEWxrkKgh3
\end{tabular}
\end{center}

\end{theorem}
