\chapter{Natural Numbers I}

\begin{definition}\label{def:pgchegdhfhdgdg}
$\mname{ordsucc}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 65d8837d7b0172ae830bed36c8407fcd41b7d875033d2284eb2df245b42295a6 \\
Pure Object Address: & TMavRsMUqs8nxad2sig41TibDMTMy1H1mNn \\
Theory Object Id: & 1452f7d6b185ccc8dd0cf665789667547457cc1e37f37eeb4542ea13bb0f3b7c \\
Theory Object Address: & TMKDT5PUJNLA2gdidecqgknUTRNKvDTHhkr
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:pgchegdhfhdgdgjebd} ${\unicdcdadad x : {\iota} .  {{x} \subseteq {{\mname{ordsucc}}~{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5a2f15e1e0256bce0e0a36c10194ffcbfe641dbb51c699626b909df04caf5bc8 \\
Pure Prop Address: & TMPc16mnjiUyzqEV7bqCxpSd6RmykST31RK \\
Theory Prop Id: & 367d807338b46735c105597b4d7b718fc7262d8a19b606bca8b2fcba8f5b1e15 \\
Theory Prop Address: & TMPyyF13kHh14HmE9nFU4oA64FKkfCootMK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegdhfhdgdgjecd} ${\unicdcdadad x : {\iota} .  {{x} \in {{\mname{ordsucc}}~{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2f6efdd09ddf2d88f93f929612974d444c064325e7c941dfb1462b672c87b2af \\
Pure Prop Address: & TMVqzvRwWJ3SEK7WcdSkCGWDSdUaejyiBbZ \\
Theory Prop Id: & 2be6be024332289d2aa440c03da38fb1d593f63adf8e2fd3e60d61ed384710cb \\
Theory Prop Address: & TMMZ4GfqtzWS5jhaGuWH9wJJD8HBcxQMpbD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegdhfhdgdgfe} ${\unicdcdadad x y : {\iota} .  {{{y} \in {{\mname{ordsucc}}~{x}}}\unicdbdjdcd{{{y} \in {x}}\unicdcdcdid{{y}={x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 01c4eee053a9b09e095c4f3572245e6c0eab90795b95854b85d38a0087607c4c \\
Pure Prop Address: & TMUfsQNiuSFqHup4XjacKRWBsfxf8BGBqRc \\
Theory Prop Id: & 3849f5cb870c46683ed2e33b5b86c0c8d2d347b9f9ef20b2d6c3591e603a785b \\
Theory Prop Address: & TMHz6H3wiAaYh9iPsBhq4bonjGvMxx7bRgr
\end{tabular}
\end{center}

\end{theorem}

{\bf{Notation.}} We now use natural numbers $0,1,2,\ldots$ as terms where $0$ means ${\mname{Empty}}$ and $n+1$ means ${\mname{ordsucc}}~n$.

\begin{theorem}\label{thm:ogfgbhpfadpfpgchegdhfhdgdg} ${\unicdcdadad a : {\iota} .  {{0}\unicdcdgdad{{\mname{ordsucc}}~{a}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1b20cba417f676cb6dbc9672ee2b03ded8ab6cfed86cd29335c5ffc3734e019f \\
Pure Prop Address: & TMQj2ULKJiSRkfDiw5djhEYAiKFnD8V8ChY \\
Theory Prop Id: & 04c4104e681b528cc961597d733a565b395e183dad8c992b88138202d9471b6c \\
Theory Prop Address: & TMSZGeeBC5QqAdFny2AFc64sYMBqNSG7WsX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfpgchegdhfhdgdgpfad} ${\unicdcdadad a : {\iota} .  {{{\mname{ordsucc}}~{a}}\unicdcdgdad{0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9b391ea2bb9a775053e83e0216e5088a30439bc1052e445f7e2b049a5e87f59e \\
Pure Prop Address: & TMHpzvw5s6p11s2PhBAUH5tA63dzykXSMV4 \\
Theory Prop Id: & 346ee0e70829c6afd0125feef2af949dbac67cd5e69584a5150bc6084f37e8e7 \\
Theory Prop Address: & TMG4GdZg9J7SSN69pwxvT4GRe1Qx3Dvxqof
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegdhfhdgdgpfjgogkg} ${\unicdcdadad a b : {\iota} .  {{{{\mname{ordsucc}}~{a}}={{\mname{ordsucc}}~{b}}}\unicdbdjdcd{{a}={b}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 40cad67f9c954d4e382390b2aba8222e29db73bba21874edcdab5f1e65bcae9e \\
Pure Prop Address: & TMJhxcvNP3aGv2vSzykSRZBpaD8KiY3FWPU \\
Theory Prop Id: & 4869a11c62e30e2d41c7f4524c576be90f3c64f919fc7dfe1442add6e7c4b685 \\
Theory Prop Address: & TMNg9uVctRmhnFUUaeZ81Gj1Y7kuPbhrwyc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegdhfhdgdgpfjgogkgpfdgpgogehchbg} ${\unicdcdadad a b : {\iota} .  {{{a}\unicdcdgdad{b}}\unicdbdjdcd{{{\mname{ordsucc}}~{a}}\unicdcdgdad{{\mname{ordsucc}}~{b}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 79130458153e5721466856a630c586b16f2738bbfc6e0259d8313cb5ade1bfa0 \\
Pure Prop Address: & TMa7r3NCaBWkq3wxWzUgF3xxk3pTHF1U4qs \\
Theory Prop Id: & 66f4df16ff59481c9056308d94b75bc6bc55adb8b8e510c166184cb6cc83d26c \\
Theory Prop Address: & TMKVLdh2rykBFF1YXiKx1pwSwX7cpuoEp9t
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfbd} ${{0} \in {1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e984b0b4b8bd4560157f8d6d3577f303bcbfad9f5202acbc6aafe41c46f5a1e2 \\
Pure Prop Address: & TMSTYDAFnhcsxKw7rE1h1KyMkzowN5nMHPH \\
Theory Prop Id: & 3be80a55870dc121ca054e5dacdfa1de52caa7939a81bb69beaf6bdbc1246eaf \\
Theory Prop Address: & TMQTUaJ1s8JSg8LytU2CzSFNeMJJfqKmUPn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfcd} ${{0} \in {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 56dc2cbeb7b04a87557e31dd8850f675eda2fcb01d7fe2d95714032d7726ec34 \\
Pure Prop Address: & TMXDJP7PuoXtQw49z9dst2KviKHpUhQEeng \\
Theory Prop Id: & 5a202e3c8e0f6cac6103c72106cd4d8b5fafa891dddb8c40e68ea9b5e1e4d088 \\
Theory Prop Address: & TMVCcMZv24dUjhcz1MQJEf7nxq1pjQVJLEk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfcd} ${{1} \in {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8704b3e5f3972c8160904d3c95ef653a8d86fd991a0e3e89d6c4ba3a0989cffa \\
Pure Prop Address: & TMcojLEL6YY4Y3YxV2dkpKy8Vbt3vCHJed1 \\
Theory Prop Id: & 431e9e50b33a518fbfbcb0617273d0749a4068ee4d20068f34f568c8ca0ca98d \\
Theory Prop Address: & TMPAkzgdLgKfuKVB27MKBPmY5KQWhbL2dWE
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ogbgehpfah}
We define $\mname{nat\_p}$ to be ${\uniddcgcg n : {\iota} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{({\unicdcdadad x : {\iota} .  {{{p}~{x}}\unicdbdjdcd{{p}~{({{\mname{ordsucc}}~{x}})}}}})}\unicdbdjdcd{{p}~{n}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 458be3a74fef41541068991d6ed4034dc3b5e637179369954ba21f6dff4448e4 \\
Pure Object Address: & TMdNqBmjo7vJ5wFYe6UamcKdgnn9WXg7rEJ \\
Theory Object Id: & cfd8eb3ef07509602aa3910d783c30847ee19a1fa94457706e8bcc91da1a0685 \\
Theory Object Address: & TMQwsyTWGfzEce8GjWygs11T1pzxgCk15vk
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:ogbgehpfad} ${{\mname{nat\_p}}~{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1617bca54b26e5228d76be996df23b2acf38a1e8ccb04bf94ec2a951660e6a42 \\
Pure Prop Address: & TMUBAZcQKUGLBQhSYCTVsFgkCVP66bx3XMG \\
Theory Prop Id: & 457a72a6740767a11460a92c05bf74c2f85ec3d9d68b112eda7a6ccb7585d72a \\
Theory Prop Address: & TMMYbseVvbEE5mCqsfJbV6FkYHcx1cF2uL8
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfpgchegdhfhdgdg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{\mname{nat\_p}}~{({{\mname{ordsucc}}~{n}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 87f001f9ea63dd0ca64b98fb5d48ee465b362dbdb42cd8a8108ac9dde660ade1 \\
Pure Prop Address: & TMaWAUtmodzvGsvp6q6xHpk4Yuham8jZXcm \\
Theory Prop Id: & 57e940f024fda91a7159ab98b6fcc0219d72fb6e7bb86ae7f0b6c4d781dfd58c \\
Theory Prop Address: & TMKZQMyAvFRX9iJG3iXqmXhhgXw3WPru1ww
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfbd} ${{\mname{nat\_p}}~{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2f83faeb354b73c788d02a2f05af45d694cfea901b6a7b10dfa230c853b96453 \\
Pure Prop Address: & TMKVKW3snRuquEuPq79vsPPwjabNMfZWF9F \\
Theory Prop Id: & 672d0d5e7bbed7f2c3c492dd058d40c6f76f54880250fc30060ac1efe4135adc \\
Theory Prop Address: & TMUjC2bRLBWtBtHMGwSpPZY777xJhfnQBRo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfcd} ${{\mname{nat\_p}}~{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a8be1568ff355447f7db7c89da6ae23d1686bd32ec45719d79659417af6f447d \\
Pure Prop Address: & TMWqNeynfSDURZP8Wzc3iZasb4wYMvcrwSj \\
Theory Prop Id: & 9112e975c2b7883a953c49c1d03e3a50209fee33f81345ec21f36647283d3373 \\
Theory Prop Address: & TMTTG4UrkKbYb6ukW8afwvToLqvgXuokzbh
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfdd} ${{\mname{nat\_p}}~{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c0849ff3f73eb686bb761cb6944a4784c9c2d96f7206b9a8024656f2b406317d \\
Pure Prop Address: & TMNxJRiy5Z5ySkwD4bVtViWKE7vD4jrAD15 \\
Theory Prop Id: & 133bb750b1d962e5d82a3fae62787479ad909ed8e960846d440b4c68d71ae6da \\
Theory Prop Address: & TMQXcPujARi3ryfse2NkWbvZ4uGumLKcEWS
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfed} ${{\mname{nat\_p}}~{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2c8e1aae548c1357c58dde606cc0aec5ffac22c5e66251a8ce0805caf0f28922 \\
Pure Prop Address: & TMH3HZH2XtjuKpCAF7SNvq8oWwWq1gMGf9g \\
Theory Prop Id: & 69ffc33641fda2b620e65b8c7a42ab36d1575ef4f6cdffca4419166392954387 \\
Theory Prop Address: & TMcTTobfSQSnJ7AbXsvRGCQ7y3HaQnEeeFs
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpffd} ${{\mname{nat\_p}}~{5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1a2477a480bd21b24c7f26877221e1b8a5a0977ebc3409b63d8b81adc052b208 \\
Pure Prop Address: & TMaLjbE49i38tGGYWFzVVSxUtcuU82qvhmk \\
Theory Prop Id: & b84b25e58b844e2ddd85bea48fe48f329f13a25c4c0456681e28158f15b3a5df \\
Theory Prop Address: & TMFj5aVyECSdNXwpDgCbbGDuCSC7gTYNSn4
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfgd} ${{\mname{nat\_p}}~{6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 25de88744534dcfb82c0d0379635001cdffce949810f8ad348a12948d32b0af7 \\
Pure Prop Address: & TMS5YEXhfPvtcWyPkWtRChML7geomnrXHCd \\
Theory Prop Id: & b4ec6745b4fa46eb645b20d7578dbd15a3c3bd98922e7daf874d00b8ec50fb0c \\
Theory Prop Address: & TMStihyrXSQ2eoCRa882VokNRU7nbYWQD8F
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfadpfjgogpfpgchegdhfhdgdg} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{0} \in {{\mname{ordsucc}}~{n}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9b50b9ff20796d5e40a96b518b4c6306f3f1fbcdac11d2c3f6be7a95ea734347 \\
Pure Prop Address: & TMNGcWtDYoP2Bidne3KeT6KVqrriDbdzHjr \\
Theory Prop Id: & 251f3d891ace960a597b3f004c9759fedf5c6738929d3028dba9a61a95fbf120 \\
Theory Prop Address: & TMHA18C6v8mXaGqFjk7jf2v9egdfvKKqWuW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfpgchegdhfhdgdgpfjgogpfpgchegdhfhdgdg} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m \in {n} .  {{{\mname{ordsucc}}~{m}} \in {{\mname{ordsucc}}~{n}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 819399e48921ef23f6b1409081964e191ac9faf077bcea0b877deb52ebc19088 \\
Pure Prop Address: & TMRPbaUhLFQA5eMs4qgHq2eHkAum5RDSzqx \\
Theory Prop Id: & 4c2c9521cdcb93eeae5ab0b3bddd72a6ac20699773fda70d1c40ad8369603f79 \\
Theory Prop Address: & TMWSu4yCbzbJPdvkEV8EErMS2USSHmDvFoQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfjgogeg} ${\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{({\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{p}~{n}}\unicdbdjdcd{{p}~{({{\mname{ordsucc}}~{n}})}}}}})}\unicdbdjdcd{\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{p}~{n}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d06f5ffa757285d834b9b984ab55693e9c64caee1e15c187462d6b08a91cfb6 \\
Pure Prop Address: & TMHLu8uvpDa5T7p3FX9tm1QcSzRDu8EgeoS \\
Theory Prop Id: & ecdce8bd5bb09bae03975edfeb1c1d944e5b0fb2eace3d673428b70400e410f2 \\
Theory Prop Address: & TMLKPWPGi2sVCW27Hu2rRaW71Je8eYbfMK9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfjgoggh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{n}={0}}\unicdcdcdid{\unicdcdaddd x .  {{{\mname{nat\_p}}~{x}}\unicdcdcdhd{{n}={{\mname{ordsucc}}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d4296fccf80fc82c53e9d0330ce9f3d5e1106daedee7d4d25d13d7d4b63ba57 \\
Pure Prop Address: & TMa76r1GZgLGs96CTRuUt7foxrtZPG4axsF \\
Theory Prop Id: & 4f4167d99f52765043e392f09f9c226ca035e3f1640818079090d6f7ab744d14 \\
Theory Prop Address: & TMR4i7cHgevq2znVdMhJMiqjT6wu9k8kJN8
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfdgpgngahmgfgehfgpfjgogeg} ${\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{({\unicdcdadad m \in {n} .  {{p}~{m}}})}\unicdbdjdcd{{p}~{n}}}}})}\unicdbdjdcd{\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{p}~{n}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d32e5b24fa29af5ae41e8ad1bdabc16e354331cd6f147252b6051abcd45747b4 \\
Pure Prop Address: & TMSAj2j7jwL81oXRAhtY9BFvgyXQUt34jN9 \\
Theory Prop Id: & 1e16087110e02042e56a9e5c1063925cc2f7ec418bc4e813ba1663102359d49f \\
Theory Prop Address: & TMSj9PFLh5Qr9YAvzYmFtQ9ahr3yMf1DzhX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahpfehchbgogdh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m \in {n} .  {{\mname{nat\_p}}~{m}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e884494b492bcc0edee39dcf5b1043dc2f35d009618bfad2e00c24a9c042215a \\
Pure Prop Address: & TMHs2RYjZjBVk1upHj4ggqMDExPU6aYRTU5 \\
Theory Prop Id: & 03b874ce14b10c68c8b003d5521fedd9dbde8f272d9947fada3cf5bee55416fc \\
Theory Prop Address: & TMMK6MMXkYaSfwkm9GkAhh9Lo4bkVBtYWdV
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfehchbgogdh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m \in {n} .  {{m} \subseteq {n}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6bc6e12c22a5d14f7294be0cdc44e66abf13bd33013e1c985c60b88343f6a7e9 \\
Pure Prop Address: & TMFwnmbaMpakWwrrmKjohDndW8KqnGgrE2R \\
Theory Prop Id: & cad6fe1daa30ce548334ddc0217dd046070f343d4279370eed3639bb6552015e \\
Theory Prop Address: & TMQmjjPV3zeSxpELyxYbuTXa9bAc7s9QGaw
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfpgchegdhfhdgdgpfehchbgogdh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m \in {{\mname{ordsucc}}~{n}} .  {{m} \subseteq {n}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e42e581777e9b184d838738cd0f2e42b37dbddeaedc030fc6bcbb1017c2c4acf \\
Pure Prop Address: & TMWNTUPr5UHTy5qBphSAPE6eNxNxTmDMM3c \\
Theory Prop Id: & bc868dd13fb819f4f89016d584069c5811ebf3ca5efcc8c1c4d079e962cf85db \\
Theory Prop Address: & TMV35265NGTDZcH9QrCs5zZVseRcm6nuMzu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogpfpgchegdhfhdgdgpffgbh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{\mname{Union}}~{({{\mname{ordsucc}}~{n}})}}={n}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 87308c20573b24369c99ff4fe9bc8822508ac2939b6f6d5756b6098dda4b527f \\
Pure Prop Address: & TMHVBTxQoQ4YadqkTHbe8MXRCPm3xY51g35 \\
Theory Prop Id: & e8cdeba740894b73be89b96729f0c00cde7781b068388e485ec8a7ef82de11cf \\
Theory Prop Address: & TMWEc3LBttyZMJdbQThEZMNmW5T1bNLMb8k
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfdd} ${{0} \in {3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d5d5f868b630108f6d0ef72c022b1a1fdcb3bba9e9ac36ffa44fbd60e4334ae \\
Pure Prop Address: & TMYMGQ2bVW21zWN5CbbTLaasyax3hxdLvqK \\
Theory Prop Id: & 313d97e81a38fa191ac39cd36a8d7be9e4da2ad48aa4710d01a9a001638e022b \\
Theory Prop Address: & TMU4Cdfau2fRjQ3n9SbuJ1p1TcVEvxWfhqp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfdd} ${{1} \in {3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 85201c4239d9221474ddfc6342817247634f124875f424ae9f7175ce6df17f51 \\
Pure Prop Address: & TMGfU5npaRR11H1ymdoVZKTfX7BrhZKDwjf \\
Theory Prop Id: & 8f3cec3de25f5229ffbd8a9526581652ba38c8b4ace6f65a6c6b0c34e257b18d \\
Theory Prop Address: & TMZAip8oPziRqgUtYsjaNbkMfq6G8pgm3NH
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfdd} ${{2} \in {3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4d67cef397f17c6f96d94a96fb406d790704d539c9dcd26f464a7ede52fd09ea \\
Pure Prop Address: & TMPo1MLQ944guurv3GfbEq47E776WbpEpzr \\
Theory Prop Id: & ebdb5d69cf555fc8c7f6126302fc59f1945db62dc77e65788bb147ab62800823 \\
Theory Prop Address: & TMFx1bn63w8vypVgVbQs3uqihXU9xXDRXcb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfed} ${{0} \in {4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0a2665a34864dd30cb973fd074b11e77208b4a6c95f91a17bc48472090308db8 \\
Pure Prop Address: & TMbWh6fxUCtxFfTwjF1FBTop3nZpchLnWC7 \\
Theory Prop Id: & 2d4164fa05829f0fb01d9e4ae31ab49773fd9055499b85021468859ab970f821 \\
Theory Prop Address: & TMG6uSmoWvJMEa12QT4E89xXUiPGnfsLvJb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfed} ${{1} \in {4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5cabbbcb5f4d3c4366e68c4306207f64e478077557ddbd21b737a9ed99b1bde8 \\
Pure Prop Address: & TMFSB8wCuJCgms892RboQ8XaFFohyZ5VoXi \\
Theory Prop Id: & 1e2d5bc32b050352877615a028897b5966602f62b83077de259c38244906a955 \\
Theory Prop Address: & TMb5w175AXMmikqn3jnFTEuWyxRWW1q9VR1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfed} ${{2} \in {4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 33c2ff88221f741e21ca67de81295fbf2c5a50f85469edc4c578006445422047 \\
Pure Prop Address: & TMSmCUEe8UeCDsTpkgeVsJafexbUrbDtBJT \\
Theory Prop Id: & 2cbb94cec93497c80bc1c990383ab0d819918ebba46428b8d07b50c2a8dd3873 \\
Theory Prop Address: & TMZ4rUSfGohxvov39V3nn9XfgUBuVUnDP81
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpfed} ${{3} \in {4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f25e446ff25ccb26c9eaf5000bbb167cdc2eee3efcb7a6c5d97b91ed9f586259 \\
Pure Prop Address: & TMHhdWYgy6pNRNN33esNvfW6grxMUZbxmQy \\
Theory Prop Id: & 22a0af713d24716cae60d0f24b75fa2f7a4806d9e04268f23e037d5bfda1d9ab \\
Theory Prop Address: & TMY5nCeLnTtDAbqPEDMuJXoU1synsTZUbX2
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpffd} ${{0} \in {5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d496b37c7578aa3dd3d6688724973b63a69ab8843dcdd9a9cbf404cee4a9e756 \\
Pure Prop Address: & TMWXaxNKNEtuRGm8q1B3GYkjFHYAnyqhofA \\
Theory Prop Id: & 965bc2aab360b39c6dcd958d77ad07534cbbe30f14358d204ad4e6b7b7b46d6c \\
Theory Prop Address: & TMK6cfwkMoqpWBimhTSkWz16DVZMkJZvErn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpffd} ${{1} \in {5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & be96a32ec1836ba1630ad994edab9d7936fc2693d7809d868797766ea4190943 \\
Pure Prop Address: & TMXHZTLBSjY6b6uscunc7vkkgtZToJhnJx3 \\
Theory Prop Id: & 34c02d4ab3de796ce3192599f046a83544b80ab964c752f5812cab439ef73dac \\
Theory Prop Address: & TMJSvdJuHEbLX569a7rARyuiAc4TBR5z7jq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpffd} ${{2} \in {5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ec68b2a5af6caf3d108a9db5a8c18bdba7461c7ae67c3f170c1567638841250e \\
Pure Prop Address: & TMcknqzryhsoUsEHJDCubHX54MtQJ7bamVZ \\
Theory Prop Id: & 7ed8e4dcf1f9fa87265224b605b86bd3741e69943d43b50b1e1184851339bc69 \\
Theory Prop Address: & TMKyPhdwyzSyueTwxxHt94eVxfRmv1aYr8Z
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpffd} ${{3} \in {5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & eddd369a108e071365a07eeb0102084ea704a8d55dd011c4fa3a11984c9d03a6 \\
Pure Prop Address: & TMFAtiv8XgWv9eW46mFVpYtzxFPKr6Zdm9r \\
Theory Prop Id: & df92fe69df5632294637d1b16ca10e692f827160f76ad0dea688f1cb47248e6d \\
Theory Prop Address: & TMEsH4FBsT68Y7qAu35cdgeMxfncBpZDQGB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfedpffd} ${{4} \in {5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e72ad7d7edf5bc6c656af02486d73733da6dab698e0c8324a4ef1729c1350b9c \\
Pure Prop Address: & TMM44jRqVsjAWBEjN5MPxHU2crXNCqdxJt9 \\
Theory Prop Id: & 03b9ff65b44d816e3599756cc6e5dc3b6b50ca8f07749f7adfd9e48f19469c45 \\
Theory Prop Address: & TMbtsFeGDXqrFQb2Xe3LnUKy3TXKV8WPAoQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfgd} ${{0} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4b3417730a51ee94caf04c6f4de510c62f9f4925400122c58b21177776e3b787 \\
Pure Prop Address: & TMLu5nuHNV3AzNorNqbEsf2hWrAxPF519QM \\
Theory Prop Id: & 9f78a575d1b7281fbcfa8c95d8e8c97c9bff83b15cc425c99c1cebf91540f0c5 \\
Theory Prop Address: & TMVHzfqGiL4fJjTzThd6tjGntRMTKW4S98D
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfgd} ${{1} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4c8428c2d2820e6ddd02f33412f82a456fbb92337a7c24bd2949838775230efa \\
Pure Prop Address: & TMc8kjaqr7JWG5gtEKyEAZGMhS9xsyCNsQu \\
Theory Prop Id: & 327244a71fe9738bca8eeac7c0c9b9ec3a4bb249e97ea6275ba6ab2dfd446afe \\
Theory Prop Address: & TMRoR6jxpANVwezSACwWKEdCd4NxVcABGsa
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfgd} ${{2} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a8317784c20b4dc83403cf330adc750c702b00a3cd65c663bc5c901a0367573d \\
Pure Prop Address: & TMXd4ThRkPLZAiyGBMqRWy2aiMvbxmyP3bv \\
Theory Prop Id: & a8f5a1b9820e7d62e90597d5e69f41e69bad70f2d1c754a0ca922ddeed9a53f7 \\
Theory Prop Address: & TMGReynZEJe34xYHBotustobc5dLWKRgJyQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpfgd} ${{3} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a261e5ada36e036a105a0af5df2c1a6bf280d14dceadb5fb843b1c5b93e6eca9 \\
Pure Prop Address: & TMGXG2p1QMD6aexgGew972chtNsckboghZa \\
Theory Prop Id: & 9f4635e903ae4d1ec8343f5c6b3c43eb6b2f022214d0c7c82673da42ba715ac7 \\
Theory Prop Address: & TMPdrRy79F8aNf9CVxzNbnL4JAAP286vxFk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfedpfgd} ${{4} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1b41da8a9246684b8db369a60d5fe5356821065ca71fb292dcb7f664a7828e8c \\
Pure Prop Address: & TMMLyZwuwf8JFrgJFBNjioGMCZyYvyzDqAn \\
Theory Prop Id: & 5d38f6e045507f4a93cad11fae8c1540a1eae90b3f52dbbefdcc9ed45b1d3c8e \\
Theory Prop Address: & TMLPcbeA4bjw9wrq33aFxyRQLGSz8g4hz1u
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpffdpfgd} ${{5} \in {6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2b492691b7ed3865b84636fa15db3d5054a753686f97633cc4ede78f686ef8d1 \\
Pure Prop Address: & TMPEvT5ScMWzFTfTs4L9HbhU3MydujRMzZs \\
Theory Prop Id: & 6d1dd13e78e58b97900513a8b85b88143e8f8b02809c1190db86c9dd2790e39f \\
Theory Prop Address: & TMW8GXcL8fcN4SrFvpTeB4P4JkZjrbQxnBM
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfbd} ${\unicdcdadad i \in {1} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{p}~{i}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7066058004d5c0b851f77ebf2a55649c2a748e523d3f217177dfd9510fd577ca \\
Pure Prop Address: & TMModSu1YSRUz9bXeP9MgEyHwZQ9newZ6CC \\
Theory Prop Id: & c6f0c0649935f65fab6b1d1d427a6aac062e1ba5d1610667c31ecaa47cb0c54e \\
Theory Prop Address: & TMcp6xnjxks7qVeybXpyew3hEbkn2Y1Yov6
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfcd} ${\unicdcdadad i \in {2} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{p}~{i}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4693b27abb85322341f1944c565b525391a1ae698d8535be845fd1293fbc3624 \\
Pure Prop Address: & TMKetHxomnrco2Vqg88PFWW5AconfvozyEs \\
Theory Prop Id: & 74563af5af19787ebf01165e4b1ceb3b061086f68c594ad4c780e78738af0c68 \\
Theory Prop Address: & TMZquspohj8HSbBs2iZWfi9rM4tD9PXhYCf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfdd} ${\unicdcdadad i \in {3} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{p}~{i}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2a0ca2e4c94eb26ab5c19412a6da10600e180d42150f6e6127f0717ef3a8c112 \\
Pure Prop Address: & TMUXV8fVuZa8oY4GuQa6GtAfrazqQgpJXZJ \\
Theory Prop Id: & 1a8a209d9754777b2d79de7e41a0d52b1cb29112b497f6494c04278866122964 \\
Theory Prop Address: & TMJNiwboDvoErEPCNUWNtB2URCDsvp59127
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfed} ${\unicdcdadad i \in {4} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{p}~{i}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d983698cedfbfb0d50150666cddd3b822dedfadb18caeb579770c029f207cd45 \\
Pure Prop Address: & TMa3a2ZsjVQYDT6yBAp8gzu9pDMZmvxMhFX \\
Theory Prop Id: & 58ec175e1fd7d83946fa2cbdc271e4619d08449b2fd4b9aa206d25c5c0250722 \\
Theory Prop Address: & TMSUJZnbtQsbxnZdQiLbj8KeXys9eLdtKmD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpffd} ${\unicdcdadad i \in {5} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{{p}~{4}}\unicdbdjdcd{{p}~{i}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f09c249f31e8eeee27f856932cdd5b636b782b2b3b2e32f82647235920772138 \\
Pure Prop Address: & TMaNUYXuGQLR3vViJceHm29PgX2B1DvZRQi \\
Theory Prop Id: & f380534e00e1acdd7956770233333b4d2c419506f8ed1664966fbd5a79325ea4 \\
Theory Prop Address: & TMbKWQtmy4GP7grvnKR87i4GqU3qf8y7RHj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfgd} ${\unicdcdadad i \in {6} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{{p}~{4}}\unicdbdjdcd{{{p}~{5}}\unicdbdjdcd{{p}~{i}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4dc95970bb9227a3f22f3850c0b8ae6a1fd851594d05dbd5ea64f678a4c05b04 \\
Pure Prop Address: & TMTngRfM6nYyAGMJnk3QjkHDpxpz3pM2qJM \\
Theory Prop Id: & ed34a795973972d067788ff2e988cafe8a031b1f5916062b65c812cd42b40e21 \\
Theory Prop Address: & TMJ5Xh7NbKFHd1vwDJmsHKLnMiEE6Lffx2L
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfadpfbd} ${{0}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9630fda1b35eebeb16a6330ac81eba7219b48d89e756733cef5f05db380572c9 \\
Pure Prop Address: & TMby1mMrnJnG3eebgn4AYd1GyHbrhqpL1fH \\
Theory Prop Id: & 74867a84ff3fe03d477cec3700c3c0504745b30ba4082bcf6867d3bfce7e06fd \\
Theory Prop Address: & TMW8jqbkDUF7dxtE4b7h7yVNVnwFchv7r4T
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfadpfcd} ${{0}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 05558045c651b5291665c412a39d06de2be8367ab59466b82289dd5533d9320e \\
Pure Prop Address: & TMZu44mT4xzQgx5223eLUCX58xAjU5Jf5QA \\
Theory Prop Id: & 9c9a3f601515a2d7da3b8b00ab6b88f05b63c5fb44c173cd5e868be872f2892a \\
Theory Prop Address: & TMYNJEaA1HL5UDfSf43JCRXZeNbHuYw2YXp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfbdpfcd} ${{1}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1d088a05070bdb1abb11db258e0e1a91308bf33b4bfd90fac2b4027e776ab0d7 \\
Pure Prop Address: & TMGhpsGUJvMfvoyyDMhyLQnsaoSjoUHHex1 \\
Theory Prop Id: & e5542eddbbedca6158ac40fec1d023b24b164c16667074aa41d1e2aa21991e23 \\
Theory Prop Address: & TMWMpuvExT7y6Sv9W8iFya7qZnGC8mnKqbz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfbdpfad} ${{1}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3a047842d8ee288fb6cf5794c28a9d57967ac47fed1474610f3d9471590139d4 \\
Pure Prop Address: & TMMwBjpCmpUHnTqc64ZdF7on5Eq6WCgDoy8 \\
Theory Prop Id: & 952fed722f255a691a61f7c092a9f63980b2e4e12b60313b9cdac6dbfd0d38d4 \\
Theory Prop Address: & TMVVgmiuwcrrYrrRVLykRqhZy2oz2EkZq5W
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfcdpfad} ${{2}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4d54d80a48e261479b57582099a83eaa414e72e5021d582b40a631d6440dcbd7 \\
Pure Prop Address: & TMSj4zVM1S7jpaZ1AVkAMacHh7z2a7w1mih \\
Theory Prop Id: & 00b357093a27461d60280a55739ba21a89b42f257242ae1a9fb792ab4984b5be \\
Theory Prop Address: & TMSyCWK4mwhWDmvJL9T59TwDeVDzmo5GCZW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfcdpfbd} ${{2}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6dd4c5f69b6b5a30c50cc8870ff9c94a49eb2257fc738c81c43eebd10b0b7fc8 \\
Pure Prop Address: & TMHNLPWx722xRdb6Lf4hip5kXBPKr3JD1kp \\
Theory Prop Id: & 2949ced3d070583d25d9e92478b3bb34672bfefe1c3018361515b55a230cbf19 \\
Theory Prop Address: & TMJ4wBoghYfjCp1GwwmbywTP6TCGue5eUGD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfddpfad} ${{3}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f27effee2c2c94b3616a5e05a191639ff0e04b481a37195eb4c6a1044f82ac79 \\
Pure Prop Address: & TMP1HRK27b3SUVqnCvdZEHQAsyFfrJj3ZFT \\
Theory Prop Id: & 799b0593a2ee6a2b5ac8d4d9a2bc8d8251c90a17927eb218b54fa15559ab2a26 \\
Theory Prop Address: & TMHR2rge7NMrthvfUFGcDrapFUGSLd3GMoR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfddpfbd} ${{3}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7fa352ff4f2f05596173373889b1ff9973ab441dd35cbebda9739720ebb7f5be \\
Pure Prop Address: & TMVVi7vv3wSKb2C8z3cEZ4a9C551bwwE95s \\
Theory Prop Id: & 8e4c7a0b39ad3b859373543800077739eb387a05d6213b9129540303af3968aa \\
Theory Prop Address: & TMdwMoiJi93xr8T9C61J9zFJibuUWHxu1oa
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfddpfcd} ${{3}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 90afb7a36efe45370d8283989fbac866a0e120e2b883d38ea2fe6fad1e2bbb4f \\
Pure Prop Address: & TMRJB22T27bFhKS9ThQj3eqAGQXbT11BEvn \\
Theory Prop Id: & 4672768d6a3c4e4a1c04351ed841430bbf66bed9a742ca18ddb5c4ccfef3f93b \\
Theory Prop Address: & TMG3u3ZqBrijhNAwNj1kYTN99h2HYB63pTL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfedpfad} ${{4}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9bd122b0da951d1af4b4d4c32e237bc4422ce033e491090ee9806587dc9cafb3 \\
Pure Prop Address: & TMKZ8uqsY7szUTPxqEmAn695ZoVVu1V891e \\
Theory Prop Id: & dbfe9c5bd8206b487aa4c1e0b115d0543cf6674122a0517ff19c410ec0cd3a44 \\
Theory Prop Address: & TMJvPDtd46ULWYjgiP8gUuZNywq5ExcmHBc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfedpfbd} ${{4}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 021d04962f43e9033ed2121c6eeb4e5d5e7ebd24e7e42ee06cfef6191229d177 \\
Pure Prop Address: & TMQffDs5XzPDL8shLUBqNhq3buem1wiUybw \\
Theory Prop Id: & bbd62921beb6f45383aa837f460867836347d2cde92052a3b2f54987f227e5e8 \\
Theory Prop Address: & TMHipYaxxuowEA9gh3W7Mg9siWtCc1uwmCj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfedpfcd} ${{4}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7a3354868dab1b0643c846ebb21f339ebbb411d9da95783a5cd4b5d559f44204 \\
Pure Prop Address: & TMRxE4YdWypoUuxdDA1hJAxrZPPnK1xbzyA \\
Theory Prop Id: & 0a09eff12034956f5d3fb29bf25815b76d297d68220b9f03eeb417bd726f5609 \\
Theory Prop Address: & TMJcWeMVmo9TXWzmFKFkPMhtzFbGJGJ6b8o
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfedpfdd} ${{4}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fdb8798e8cacfe9c22e7a5300ab6ad312c527880e2d6114e93ee6909092b939e \\
Pure Prop Address: & TMWoPuE96Hes4hFCCiWYiKQFfnv8kusTH4Q \\
Theory Prop Id: & 2a56945cd215c22b3db025b3a1115bea3f8be9f8cf7e86f135c9d62fe1b0d0ee \\
Theory Prop Address: & TMTJo37vnbVGCAZzhJgVrDjVt3X2aricxbz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpffdpfad} ${{5}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bf9251e9bb7b6c3fcadb2f0da4a63d6b36fd8576e49f09a3abe2d7b832c72c36 \\
Pure Prop Address: & TMEqk6oZYNwmG5wB1ZGKrZ4T3yWfbqHjRqV \\
Theory Prop Id: & 29ce2701ae30ad2dbf565d3b4a8bf0d77c130da112d208cdb3edf1b1daf72161 \\
Theory Prop Address: & TMFJq3wfqDg8x2vPXgbwmSzud3MUPwdSgcc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpffdpfbd} ${{5}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f97fb195b34610dd92dc1c9a46a8fe29d0b99faddd0ee0cb789d7ff153041aa4 \\
Pure Prop Address: & TMLhHuF4WrVXhN5KWBBaWXPp9K7YsCP7XNf \\
Theory Prop Id: & cdb672d8c8dfd8a0236d3cfb650c10ae9a5ce01b958ebc60d0bba75bcd57ab5d \\
Theory Prop Address: & TMahxTsu3gQAQUaNifvwRtxDuvarKz9wQP3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpffdpfcd} ${{5}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 25bd00866c407af3c2b8f45d94058aae95d0bd9f06352dd9963408e6745e7f2a \\
Pure Prop Address: & TMLxeQNww6bks2wbWReMUo5Q5HCFEpkctEq \\
Theory Prop Id: & 72066ec74ade8ba81c3aefe23451a21df4aca05a08491cc0af4ff4b1131a38f3 \\
Theory Prop Address: & TMLSxacJKrd3N21R6mQxy5fSfYVEUaG9E8y
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpffdpfdd} ${{5}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3372df01e49c94e55fd317e47ba515344be9ed24947b63ae3b7f4648de435eda \\
Pure Prop Address: & TMPpVH6dFjx3FEaJ9sSmDs9wSvDKLg7DmMq \\
Theory Prop Id: & c26bb5b01832d8111735852c7f606f729b39acf9552a1df641404300808a241c \\
Theory Prop Address: & TML4qfcmrd4raBqNGGB7QyhUxV5XtrDK1Q4
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpffdpfed} ${{5}\unicdcdgdad{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 909c7c9d7cea9bcfbcb09a16340b2474d31cd36261d27ffef43b7102b4a4eb71 \\
Pure Prop Address: & TMJHtW82A2WHP7ViQ391KAdZ1w1wRKs8HYL \\
Theory Prop Id: & 20c3f2d381518f33179709cb5e92c3242267b3069264b9539368291bdf5c269b \\
Theory Prop Address: & TMX5VEFqEbmZM1jXnm6B1dHJJ3UZE1gT5QR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfdgmgpgdhfgegpfje} ${\unicdcdadad U .  {{{\mname{Union\_closed}}~{U}}\unicdbdjdcd{{{\mname{Power\_closed}}~{U}}\unicdbdjdcd{{{\mname{Repl\_closed}}~{U}}\unicdbdjdcd{{\mname{ZF\_closed}}~{U}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f643b48ed401d2a1c3f6e0b2127cb23b125acf15c4cb21f77a1c45bb01c85847 \\
Pure Prop Address: & TMJPXWCGGsgp2RauzJmcXDkupZ2Bwq8zM8g \\
Theory Prop Id: & 6d69881b387db1470aab7b9513ee8d85714e5e34821b8dcdfbe77a49b4958281 \\
Theory Prop Address: & TMbg2Nr5QH7Ui64ri9oF1hQu8esX9wKCtSG
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfdgmgpgdhfgegpffe} 
$$
\begin{array}{c}
\unicdcdadad U .  {{\mname{ZF\_closed}}~{U}}\unicdbdjdcd \unicdcdadad p : {o} .\\
 {{({{{\mname{Union\_closed}}~{U}}\unicdbdjdcd{{{\mname{Power\_closed}}~{U}}\unicdbdjdcd{{{\mname{Repl\_closed}}~{U}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d795d416d63c658dd17353b60159cec522fd5799091016c00532a86a98184a9c \\
Pure Prop Address: & TMFJaZKQXV2BpbnNf3V5PpeaeGyXeZd9p8t \\
Theory Prop Id: & c78c790145214f0f70a0200b6fba47786c8f97e50408def3352d6b836a599b37 \\
Theory Prop Address: & TMZSTib6nnUwYgZqRxuRTmGJX2JoBnPeAGv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfffogjgpgogpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad X \in {U} .  {{{\mname{Union}}~{X}} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a7cdf13e39c8049cf56acd30a1e889d54edc18ff38a1bbc2e1ed347d9682a5ad \\
Pure Prop Address: & TMUofvcpBARSdnFetm8dQrjhiWg4kWAGFB4 \\
Theory Prop Id: & 250496cf2e1875d7ec9219017e8d4508f9ca7718cbfd9c968c7bade397f00ea9 \\
Theory Prop Address: & TMcGjahmQUapH4bqbAdGBQ6EgJgQDSjPLwm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfafpghhfgchpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad X \in {U} .  {{{\mname{Power}}~{X}} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d781fd8e7019faff9a70275545ea6d69a0eb9adbe24e83a2e06143bffd06746 \\
Pure Prop Address: & TMHz75Wp3yULtSkKHqZV4euzQkSQyKevgdT \\
Theory Prop Id: & 7411dd8f49dfca8e20b3d4524ebb50b5fb3351ca8588eb34afde921cd3727004 \\
Theory Prop Address: & TMFeLtgqxJCBDZ3U5JYcbg9M6iiuFekPu6M
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfcffgahmgpfdgmgpgdhfgeg}
$$\begin{array}{c}
\unicdcdadad U .  {{\mname{ZF\_closed}}~{U}}\unicdbdjdcd\unicdcdadad X \in {U} .  \unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} . \\ {{({\unicdcdadad x \in {X} .  {{{F}~{x}} \in {U}}})}\unicdbdjdcd{{\{{{F}~{x}}|x \in {X}\}} \in {U}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 312268feb1dd5835c81ed94141bfe83ca9dda2b26ecf8263cee15af85f88b8b2 \\
Pure Prop Address: & TMPP71S8C6hLepoQ5MX4wJnJZ5iqRp8wjHj \\
Theory Prop Id: & 18f8acc434076d8590e9958a09b3287e80e677748bfa68846c9246019587ec5c \\
Theory Prop Address: & TMQuAnjb2usoLHA9bv3uUoCs1dSHiL1SFdi
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfffafbgjgchpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad x y \in {U} .  {{\{{x},{y}\}} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 54256a260e0aeb219ec7b9c1f5470e1c879e31656131aab6f98d5191437dc819 \\
Pure Prop Address: & TMJ8PnAXtGvJBQ2w7xRg2sQuiEx27bk436v \\
Theory Prop Id: & ef42d3cc50e9cba4432b33a79bbd1192bd239f4d284470ad502781b5fb35ca8e \\
Theory Prop Address: & TMcjrdqKzeo7g2gDjiEsVum3CAuDTSFiFuB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfdfjgoghgpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad x \in {U} .  {{\{{x}\}} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d8a834f1cf303ccfa19193124cf05f94ba5eadb60ba9505bc698fae5beefe9f \\
Pure Prop Address: & TMRHMv7QRuD1cNMZ1DKFBfgHLajcAvhMXXa \\
Theory Prop Id: & d02d66f005b189993512ef90ced927d55db86cbffc2242c0a868958712bdead1 \\
Theory Prop Address: & TMQJBe5GNPMz6xkyZp1New6CprvjNNWbVQB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfcgjgogfhogjgpgogpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad X Y \in {U} .  {{({{X}\unicdcdcdbg{Y}})} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8a62402878aa34b70e4993833d0aac7cf60d7b31747f91d9f6bbb966b91e20e1 \\
Pure Prop Address: & TMEqKpBN15S7iTeSq7zbuWutkNifE2ingyu \\
Theory Prop Id: & 1bacfdb236f4aeb5ec63cb4b7c4d4bb0744883de7265fff6b8b706d8b410cece \\
Theory Prop Address: & TMdzxaBW52KHaW3S2NvEVtisq8WoKg6MZvp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:kfgepfpgchegdhfhdgdgpfdgmgpgdhfgeg} ${\unicdcdadad U .  {{{\mname{ZF\_closed}}~{U}}\unicdbdjdcd{\unicdcdadad x \in {U} .  {{{\mname{ordsucc}}~{x}} \in {U}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 68a6ba11b0ad56c445b6e8bc81041f5c2cb0db9142f6b147cfcfa7ef1d2f27f3 \\
Pure Prop Address: & TMH2dwKRQudFN9m3qx3RNdaBLvqypKizZv5 \\
Theory Prop Id: & 946e6124c0e8be96a15baa61fedb45d36338fafc05a2f31ce54a95174700bf8f \\
Theory Prop Address: & TMPqDp5W4hUggbHVsbPDuU2ytBMzDWrbM2M
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahpfffogjgghpeggpffengahehjh} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{n} \in {{\mname{UnivOf}}~{\mname{Empty}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c885b475dae13164eaf466c05904664c48aa5e96b6499036d6bbd7ab2b3b01e3 \\
Pure Prop Address: & TMTM67QGgM77h8RbmGoR4QhuHU14bxuur8y \\
Theory Prop Id: & 645aee297f02d0a7caa06a5efea238cec06af7df69b2643d2adc7c5d9b418911 \\
Theory Prop Address: & TMZEUzvGsZE4EoguW8R1ovkAWzhDE4znAr3
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:pgngfghgbg}
$\mname{omega}$ is the opaque object of type ${\iota}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6fc30ac8f2153537e397b9ff2d9c981f80c151a73f96cf9d56ae2ee27dfd1eb2 \\
Pure Object Address: & TMb4KgMPXEQBvZWN5yMtrjHJCTxAvdStvip \\
Theory Object Id: & ad9ad81c42d92fd52433645cf2466f4f0179ab10ee124be71bb12991deb2ddf0 \\
Theory Object Address: & TMNkXuKe4mYMmqP6e4nkiPeWyEzHKwZy2zC
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:pgngfghgbgpfogbgehpfah} ${\unicdcdadad n \in {\mname{omega}} .  {{\mname{nat\_p}}~{n}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f44a309f3fadd69adfefbc11bb8cd5a0e2d204f0f0ccde446b0cf927293e46dd \\
Pure Prop Address: & TMQLBjRkNsbEFRVrBkuh1bmZQqCeUscTWR1 \\
Theory Prop Id: & c2c61b35088d7afd198e0d398dabb21f1be9e52d6c73d798f0fa57761801eaa0 \\
Theory Prop Address: & TMcBbUsnDN99QLS1dM6hhdDj1W8pvPaMBBH
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahpfpgngfghgbg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{n} \in {\mname{omega}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6a1b445f977fd3fae4e1e1cc46011455e1f0531f1a15c5c25278556928dcee83 \\
Pure Prop Address: & TMd8YkcuN2F2evUjAbU6Ts5vNLwKCBES7rW \\
Theory Prop Id: & d5080f911ac6cf73280f9bbcf0edc2218ca24806bdc57695210e6115b9406c38 \\
Theory Prop Address: & TMWv1SjyTw4FBL65LJ4Dydky2jqrjzFo4WF
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgngfghgbgpfpgchegdhfhdgdg} ${\unicdcdadad n \in {\mname{omega}} .  {{{\mname{ordsucc}}~{n}} \in {\mname{omega}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 246d636d93c78b4e3365422a679abe57556849f5546b6f8e8fbaeeab0e834905 \\
Pure Prop Address: & TMYTp6SmJ6Xb74ZB58T5drE74MrfSMJ56Xd \\
Theory Prop Id: & 17fb646a22b11762cb7ae21fb49306beac81729c7c3e89992f09e10eff2d8f9e \\
Theory Prop Address: & TMcKRUvCqbX8WtX4XYQZ7VoDqsewDsQmCWB
\end{tabular}
\end{center}

\end{theorem}
