\chapter{Explicit Number Structures}
\section{explicit\_Nats}\label{fgihahmgjgdgjgehpfoebgehdh}Let $ N : {\iota}$ be given.
Let $ base : {\iota}$ be given.
Let $ S : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdh}
$\mname{explicit\_Nats}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3fb62f75e778736947d086a36d35ebe45a5d60bf0a340a0761ba08a396d4123a \\
Pure Object Address: & TMVtLiLBPcSiAyimBNLrSsPPvNGxNnQTLgx \\
Theory Object Id: & 499c1253e694386778e3a86aec4d8d86e3e968012315d84ff3d8771c7ca33ca6 \\
Theory Object Address: & TMYM3xBCn91GR8gYvvjmLwhSW8eWQhQUR5V
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Nats_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfje} 
$$
\begin{array}{c}
{{{({{{{base}} \in {{N}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad m \in {{N}} .  {{{{{{S}}~{{m}}}} \in {{N}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad m \in {{N}} .  {{{{{{S}}~{{m}}}}\unicdcdgdad{{base}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad m n \in {{N}} .  {{{{{{{{S}}~{{m}}}}={{{{S}}~{{n}}}}}}\unicdbdjdcd{{{{m}}={{n}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad p : {{{{\iota}}\unicdbdjdcd{{o}}}} .  {{{{{{p}}~{{base}}}}\unicdbdjdcd{{{{({{\unicdcdadad m .  {{{{{{p}}~{{m}}}}\unicdbdjdcd{{{{p}}~{{({{{{S}}~{{m}}}})}}}}}}}})}}\unicdbdjdcd{{({{\unicdcdadad m \in {{N}} .  {{{{p}}~{{m}}}}}})}}}}}}}})}}}{\unicdbdjdcd}{{\mname{{explicit\_Nats}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1e6abb88cfbf0a3803f631d2180983c78469316b36f44986957690ca50046636 \\
Pure Prop Address: & TMS7xTLnefHd6AjUKGkQBpdVrdEKnFWi6GV \\
Theory Prop Id: & 1c1fb7a66f9f17cd55170faa1827e232bbd7515b8fbb9a57a4ccf3c34eaa501a \\
Theory Prop Address: & TMZjQDjppyHzU9Sm626Nv7EXMsNVVAqkaJT
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_Nats}}}}\unicdbdjdcd{{({{{{base}} \in {{N}}}})}}\unicdbdjdcd{{({{\unicdcdadad m \in {{N}} .  {{{{{{S}}~{{m}}}} \in {{N}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad m \in {{N}} .  {{{{{{S}}~{{m}}}}\unicdcdgdad{{base}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad m n \in {{N}} .  {{{{{{{{S}}~{{m}}}}={{{{S}}~{{n}}}}}}\unicdbdjdcd{{{{m}}={{n}}}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad p : {{{{\iota}}\unicdbdjdcd{{o}}}} .  {{{{{{p}}~{{base}}}}\unicdbdjdcd{{{{({{\unicdcdadad m .  {{{{{{p}}~{{m}}}}\unicdbdjdcd{{{{p}}~{{({{{{S}}~{{m}}}})}}}}}}}})}}\unicdbdjdcd{{({{\unicdcdadad m \in {{N}} .  {{{{p}}~{{m}}}}}})}}}}}}}})}}\unicdbdjdcd{{q}}}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_Nats}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5de31c779c105b713f97c938846c5369a751bf11d4d1c91131667de452b85d52 \\
Pure Prop Address: & TMN27YWUyKn3QBjt1t4WK1VcstkTSsWazb6 \\
Theory Prop Id: & 80e228811834277628e910ca46e86ac23fcdf98d3b95ab2ee85c1f1697c9842b \\
Theory Prop Address: & TMXQDL2aLuWPAFGh9xNGSkbkMuMSyVTuvG2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_ind
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfjgogeg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Nats}}}}}{\unicdbdjdcd}{\unicdcdadad p : }{{{{{\iota}}\unicdbdjdcd{{o}}}}}{ .  }{{{{{p}}~{{base}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad m \in {{N}} .  {{{{{{p}}~{{m}}}}\unicdbdjdcd{{{{p}}~{{({{{{S}}~{{m}}}})}}}}}}}})}}}{\unicdbdjdcd}{\unicdcdadad m \in }{{{N}}}{ .  }{{{{p}}~{{m}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 72f6cf6a8db779d851cead9db4030c8cf14cdb66b3dba2256273ea5c82f6cf75 \\
Pure Prop Address: & TMRCzQGX3LAr7ohapsy9xQiuobUsWPbHmfG \\
Theory Prop Id: & 3e626e6f6e97b94d761465a195a81a506097757289b1852c22484904835f624b \\
Theory Prop Address: & TMLtcGPvoYCa4mMihX67t4Lm78GzLsmB2B6
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfahchjgngchfgdg}
$\mname{explicit\_Nats\_primrec}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & a61e60c0704e01255992ecc776a771ad4ef672b2ed0f4edea9713442d02c0ba9 \\
Pure Object Address: & TMY3C6hyjHYFvPNDaQK728xpbMFkgTGPbUQ \\
Theory Object Id: & 02adae4d88dbb61570b0e9d5d5ea2d21abfb3e9a8408276329ddc4e3b1fc2a9a \\
Theory Object Address: & TMUhjTmqPCD758LckQJPJ6DHuAFTQeHLoqS
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Nats_primrec_base
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfahchjgngchfgdgpfcgbgdhfg} 
$$
\begin{array}{c}
{\unicdcdadad a .  }{\unicdcdadad f : }{{{{{\iota}}\unicdbdjdcd{{{{\iota}}\unicdbdjdcd{{\iota}}}}}}}{ .  }{{{\mname{{explicit\_Nats}}}}}{\unicdbdjdcd}\\
{{{{{{{{{{\mname{{explicit\_Nats\_primrec}}}}~{{a}}}}~{{f}}}}~{{base}}}}={{a}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ec9dac528f5b9d80aeb2b078f81657da0725083292683597b6ed0f6bcda0033c \\
Pure Prop Address: & TMJxuYA6EQJ2GxewDFKrBTK4gZX2qiFpNuM \\
Theory Prop Id: & 18887ff3f12d4f358090a38d2eecb57a5531dabfe6535ad15a910933b602f16c \\
Theory Prop Address: & TMGkBbmvyBif6wxjhQzqdSRLtTP5TBd5e9z
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_primrec_S
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfahchjgngchfgdgpfdf} 
$$
\begin{array}{c}
{\unicdcdadad a .  }{\unicdcdadad f : }{{{{{\iota}}\unicdbdjdcd{{{{\iota}}\unicdbdjdcd{{\iota}}}}}}}{ .  }{{{\mname{{explicit\_Nats}}}}}{\unicdbdjdcd}{\unicdcdadad n \in }{{{N}}}{ .  }\\
{{{{{{{{{{\mname{{explicit\_Nats\_primrec}}}}~{{a}}}}~{{f}}}}~{{({{{{S}}~{{n}}}})}}}}={{{{{{f}}~{{n}}}}~{{({{{{{{{{\mname{{explicit\_Nats\_primrec}}}}~{{a}}}}~{{f}}}}~{{n}}}})}}}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c79ce9883e3c0c86ed88d57e78ed6269f94c26749772f51c6ad325234a554663 \\
Pure Prop Address: & TMSv5jrFNLuwkARow9Y11SWFGFXBqcbUbLK \\
Theory Prop Id: & bf9939e2289e86288ccefbe010777a3faf16479bf896f3b41a2c5a5a73e561cb \\
Theory Prop Address: & TMUpUUqwaxvwAg3jgXfPz8RdqaXuW1kMAxx
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_primrec_P
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfahchjgngchfgdgpfaf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Nats}}}}}{\unicdbdjdcd}{\unicdcdadad P : }{{{{{\iota}}\unicdbdjdcd{{o}}}}}{ .  }{\unicdcdadad a .  }{{{{{P}}~{{a}}}}}{\unicdbdjdcd}{\unicdcdadad f : }{{{{{\iota}}\unicdbdjdcd{{{{\iota}}\unicdbdjdcd{{\iota}}}}}}}{ .  }\\
{{{({{\unicdcdadad n \in {{N}} .  {{\unicdcdadad b .  {{{{{{P}}~{{b}}}}\unicdbdjdcd{{{{P}}~{{({{{{{{f}}~{{n}}}}~{{b}}}})}}}}}}}}}})}}}{\unicdbdjdcd}{\unicdcdadad n \in }{{{N}}}{ .  }\\
{{{{P}}~{{({{{{{{{{\mname{{explicit\_Nats\_primrec}}}}~{{a}}}}~{{f}}}}~{{n}}}})}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7ffca5b3e4e2357fc59f35b26bcc159af8962fe6020bca14a2c9246bac7165e9 \\
Pure Prop Address: & TMPVTJWhZ2JZ6V3t3BHXTUQ7k318dSnYpfW \\
Theory Prop Id: & a23b352d53e7ed810c1716d20ebfd8cf9fd43007e863a3265aa1009d6883d822 \\
Theory Prop Address: & TMSyXZfNTKDx39oHHCRdmhL4WfJE3gghudc
\end{tabular}
\end{center}

\end{theorem}
\section{Omega gives Explicit Naturals} % explicit_Nats
\begin{verbatim}
explicit_Nats_omega
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgngfghgbg} ${{{{\mname{explicit\_Nats}}~{\mname{omega}}}~{0}}~{\mname{ordsucc}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a3ba10e61c3b75d16024bffd1f732e7b90427037533d34ee2e091771480c74a6 \\
Pure Prop Address: & TMdGdgcJArCKDPYXVndpbm1SU3AEVwyfoDy \\
Theory Prop Id: & 4d074b5527b3d4f670e267d1341927f6e1665b1b695a8fa1d7b296e3b59b616f \\
Theory Prop Address: & TMN5Yqfwk5yD9vYjacHHUZqkgRCThYxgE6u
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Nats\_zero}\label{fgihahmgjgdgjgehpfoebgehdhpfkhfgchpg}Let $ N : {\iota}$ be given.
Let $ zero : {\iota}$ be given.
Let $ S : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfahmgfhdh}
$\mname{explicit\_Nats\_zero\_plus}$ 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: & 9683ebbbd2610b6b9f8f9bb32a63d9d3cf8c376a919e6989444d6d995da2aceb \\
Pure Object Address: & TMEmJ2AUSSkSo3PgswMDx4FDuVNXWTFp2Xv \\
Theory Object Id: & a492e421e4fb131a6ece5ab66d32b1664ac5750c65f21c1ee016f0b281db4c68 \\
Theory Object Address: & TMZHNQrttsjehBJHhEo49zc8mrT3L85obE5
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Nats\_zero\_plus}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfngfhmgeh}
$\mname{explicit\_Nats\_zero\_mult}$ 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: & 7cf43a3b8ce0af790f9fc86020fd06ab45e597b29a7ff1dbbe8921910d68638b \\
Pure Object Address: & TMWE5mZjYWyApPQfEURTERyzUQDmzqxvrRZ \\
Theory Object Id: & 11a63fc4e4e266de185d7864c9ae0a5059a920dc1af5eb33480e4b6257a39712 \\
Theory Object Address: & TMa5dmS6AU8GbHfa7BizTDCqP4sRj1UmdGg
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Nats\_zero\_mult}}$.
Assume the following.
\begin{equation}
{{{{\mname{explicit\_Nats}}~{N}}~{zero}}~{S}}\label{hyp26:ieoe}
\end{equation}
\begin{verbatim}
explicit_Nats_zero_plus_N
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfahmgfhdhpfoe} ${\unicdcdadad n m \in {N} .  {{{n}+{m}} \in {N}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 56523af04adfa34d579665edd443f3c8c991a55c2e1d59fe86eb7cb534626054 \\
Pure Prop Address: & TMKvkMhHVgvBVAMZ58PR6NKqCWx4kMPZmfY \\
Theory Prop Id: & d3decda97e93dc588cf7d1be70d082fee93bb6edd68e6c451ca3e4e4685258a4 \\
Theory Prop Address: & TMXZCAYSxCqnbikDjS9v4JyUbJQi41N3Beg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_zero_plus_0L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfahmgfhdhpfadme} ${\unicdcdadad m \in {N} .  {{{zero}+{m}}={m}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & eda4ea107573c4741f17b9e4cfc4ad2c0fca35856cb39a9f9d0c7082eeef8edc \\
Pure Prop Address: & TMZFAJoCr87Twhz3ue2eaZWtjHZrDbriNS2 \\
Theory Prop Id: & 6cbaa15873e859402e00e7efd7313e6202c9580bb8dc07d3eaff7cb6dd528689 \\
Theory Prop Address: & TMXGbC3fvTNoibPqk8dSmxUYfFe6A2jTjVA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_zero_plus_SL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfahmgfhdhpfdfme} ${\unicdcdadad n m \in {N} .  {{{{S}~{n}}+{m}}={{S}~{({{n}+{m}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4b64cc27697767078865ed93f819202d8095e44f34703cacb427d0ff277b7772 \\
Pure Prop Address: & TMUB4sk69KXoqr9KeeXuQvkBtdzEy5uGSGY \\
Theory Prop Id: & 67b5266ae2b89bd4f290f8483d37fed2bec3392b27b55c35022e5621958309a4 \\
Theory Prop Address: & TMUxY6JJgbyA2wvfR5kWXPg76FJgumm8rc1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_zero_mult_N
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfngfhmgehpfoe} ${\unicdcdadad n m \in {N} .  {{{n}*{m}} \in {N}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 242c80020d9e0983d413a8726b0f8dd31a5d6ed1c4a614a9e372f46e71b811d7 \\
Pure Prop Address: & TMPyVVnedkqiLXtyLzYCYMHVttNM5sfuXaF \\
Theory Prop Id: & 4d99dbaf92926086a5db90b0b45da73422e998d71f9d9b53551ce90cc1bc2a97 \\
Theory Prop Address: & TMUjvpTR8zMFez8UREoFWmF1mfB2Ck1G9qd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_zero_mult_0L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfngfhmgehpfadme} ${\unicdcdadad m \in {N} .  {{{zero}*{m}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b80ff108406a373e38422d03ee6a993a3300f355e3972522d8834e8f32e727eb \\
Pure Prop Address: & TMdPBQEb6r1jazTfaSsAkVi4HU5BuA9SgCr \\
Theory Prop Id: & 8b905296c07181890992e4efb2371e7d4c2eacd4d79aa5f2ae5bee8d137d8e99 \\
Theory Prop Address: & TMFy6HpCwNacy45vXp7VgoS5A62a6koR3ib
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_zero_mult_SL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfkhfgchpgpfngfhmgehpfdfme} ${\unicdcdadad n m \in {N} .  {{{{S}~{n}}*{m}}={{m}+{{n}*{m}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ceea17fc60f9c29a157639cceb082002f336d7ada992c4bf24f10ec2107aaeef \\
Pure Prop Address: & TMN5mn9NySXen2SeWDjUyYFPcUTDr2zeAhC \\
Theory Prop Id: & 58cb3351db2fc2413401ac6beecc0c5aa8cb6e94862e9b0888a08fab43ce10ae \\
Theory Prop Address: & TMYNaqKknxFESuZan8Ztx9TK21bLv9z72UQ
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Nats\_one}\label{fgihahmgjgdgjgehpfoebgehdhpfpgogfg}Let $ N : {\iota}$ be given.
Let $ one : {\iota}$ be given.
Let $ S : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfahmgfhdh}
$\mname{explicit\_Nats\_one\_plus}$ 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: & c14dd5291f7204df5484a3c38ca94107f29d636a3cdfbd67faf1196b3bf192d6 \\
Pure Object Address: & TMVj1gkGc7wpNZ6S9o6JmxmKVGCvLP3HmTd \\
Theory Object Id: & a0dc24bec298fc49cdd175bfad0801c6dda7e88d2602021d5fc71cc01e269ee8 \\
Theory Object Address: & TMW7qLS9YPVnzwPSYkBdmmRwk5ZbPbLdnpL
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Nats\_one\_plus}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfngfhmgeh}
$\mname{explicit\_Nats\_one\_mult}$ 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: & ec4f9ffffa60d2015503172b35532a59cebea3390c398d0157fd3159e693eb97 \\
Pure Object Address: & TMJBfR7vUcShqA32xB1n6LKgJDcAtK2PWgY \\
Theory Object Id: & 7cbccf9874bf38cebb42cd5bbc730880796dbf9ee8b00e588914593a33f3616e \\
Theory Object Address: & TMdYg5kd19jjyivNeoE1Fq5Z77fpmPN4Ghy
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Nats\_one\_mult}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpffgihah}
$\mname{explicit\_Nats\_one\_exp}$ 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: & cbcee236e6cb4bea1cf64f58905668aa36807a85032ea58e6bb539f5721ff4c4 \\
Pure Object Address: & TMGRgxwxS6aYefXQew7xTarwkrNkekEv1vL \\
Theory Object Id: & f451e86804defa9f4c49ef8b31319235986f06a57cc47e224e0e616e81349e41 \\
Theory Object Address: & TMYMj3b1DyJ9Lbh2dkML476LtBBK6RhxAGa
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infof$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Nats\_one\_exp}}$.
Assume the following.
\begin{equation}
{{{{\mname{explicit\_Nats}}~{N}}~{one}}~{S}}\label{hyp27:ieoe}
\end{equation}
\begin{verbatim}
explicit_Nats_one_plus_N
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfahmgfhdhpfoe} ${\unicdcdadad n m \in {N} .  {{{n}+{m}} \in {N}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b870373860de2f7ad912a4078539010f085139c691292d7e7d3c34db1f0cdb6a \\
Pure Prop Address: & TMMGxvc17zs14pSXUk5XHB547EgcLE5Qj1X \\
Theory Prop Id: & 2031f14ef57b3e0a0f0bb3c5d4e8d7cc6c01908d84f8ae8a58422536a7ebd671 \\
Theory Prop Address: & TMKsochxf4GKDVGFjEfDV7zBLDZ3NZmTqN8
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_plus_1L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfahmgfhdhpfbdme} ${\unicdcdadad m \in {N} .  {{{one}+{m}}={{S}~{m}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e0ca47b5062d5ffc6896d07746c59aaca4bc4acc06788ddcfa7d606c68f00a95 \\
Pure Prop Address: & TMSjCGdV6bWn9b6ayvqYSEN5ezLiifHBvqP \\
Theory Prop Id: & b861add16dde10cbd273ebb51a08c3bde324096c7b892a0f54908292dbd67d14 \\
Theory Prop Address: & TMRmkTUjpfWnjUnbtZRbTeUiDDjnxz6PKXn
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_plus_SL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfahmgfhdhpfdfme} ${\unicdcdadad n m \in {N} .  {{{{S}~{n}}+{m}}={{S}~{({{n}+{m}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d527faf460c66eb2a605937d7bc284a505c5e71e11b5819b3ebe45aa5ae3df30 \\
Pure Prop Address: & TMZrvHTgr8uHgFqVfwzAjaHWjcyWUe9ku88 \\
Theory Prop Id: & 272ea646fea8c08826956116e3b06f06b4f1a29035d7099f3e17dbff9743db74 \\
Theory Prop Address: & TMdJyqAKqfUoMVXYdkRynaBe5Y4UCycBCSi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_mult_N
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfngfhmgehpfoe} ${\unicdcdadad n m \in {N} .  {{{n}*{m}} \in {N}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 71dc3009d99275dcb7507e7e7f7b53e10abcd721e2a9f4479dfb1d9626492798 \\
Pure Prop Address: & TMUF1CggpPWJLEjwmb369yXyFWWhKTPPS6u \\
Theory Prop Id: & 6cea9937d528c3ed3844899b07adc36352b53c024fca3a3fb796832b3cb817eb \\
Theory Prop Address: & TMLGNEexWqJMgReiwzYkhaf87Wi9rCre9U7
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_mult_1L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfngfhmgehpfbdme} ${\unicdcdadad m \in {N} .  {{{one}*{m}}={m}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 248ac634eb92e6d0725101234c0f2912ffe95ed5d81f7568c5ebace9788fe8c6 \\
Pure Prop Address: & TMTS3c1HETRVj5fANAi3ixWKrd9G35hxXTk \\
Theory Prop Id: & cf9d37fbd63485076deb649fa124b9d2400952c5423fe11ea9f085d236188b80 \\
Theory Prop Address: & TMTMa1DWHDPBUbN5Uh2GsHTp6jg2Ve8n4iF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_mult_SL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfngfhmgehpfdfme} ${\unicdcdadad n m \in {N} .  {{{{S}~{n}}*{m}}={{m}+{{n}*{m}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f260dfa960c7ea2ad1c80083a06eaed1460025b578976944e9d439072b54a833 \\
Pure Prop Address: & TMYCaevEfmMyUdnjxigfSRQFKL62bwDtseb \\
Theory Prop Id: & 84048a4e0ac742533042895099975cda2d4ce7777ccfe9a38dfebad9d348452b \\
Theory Prop Address: & TMT3bNHPRqWLxd5k165RfwDrLuFDDnTU4GR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_exp_N
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpffgihahpfoe} ${\unicdcdadad n m \in {N} .  {{{n}^{m}} \in {N}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e06153d7a791dd306b96ac5fa124b22a5e0e6f3c79dc892e8973612dbdbcf965 \\
Pure Prop Address: & TMbPBpFHKw4tdRPzKEnzY36NJm6Wo5NA1vq \\
Theory Prop Id: & dc83c194406168e2322b693e0db9e9c2935f9b5890252230aac13dbba5dd04f4 \\
Theory Prop Address: & TMXt3nAqYNYZHtj3LbChY5GKH6imEYDSJJA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_exp_1L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpffgihahpfbdme} ${\unicdcdadad n \in {N} .  {{{n}^{one}}={n}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3135e1cbd0675df0f6c911e6f05dd6ea73bc4c458266e5d736412045200aae78 \\
Pure Prop Address: & TMd59g2sbanMoRmaQmddMbB1kEpMZkGsjHd \\
Theory Prop Id: & 35371d46a876899103c3b0122a82b56515f75a0378f71012b5d765398f35d30b \\
Theory Prop Address: & TMKNGaufMJdNVayeapLn2aUCzuEgW63wrfh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Nats_one_exp_SL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpffgihahpfdfme} ${\unicdcdadad n m \in {N} .  {{{n}^{({{S}~{m}})}}={{n}*{{n}^{m}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7a9c28b365c7612ae00bcf5eae2460615c9a85f39e5734a2fe11b4129c6272d2 \\
Pure Prop Address: & TMbzoYWnxTt9ZksjQ6HvVxXro6tokwCYzCB \\
Theory Prop Id: & 61fbfd0911e934537afe54a0c8fd8369d881dbd3b94b5b74c40a418954a55d7d \\
Theory Prop Address: & TMJ3ASygyK5PDcYrS3MhKvqvt7Buzmpj1BC
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfmgeh}
We define $\mname{explicit\_Nats\_one\_lt}$ to be $${\uniddcgcg m n .  {{{{m} \in {N}}\unicdcdcdhd{{n} \in {N}}}\unicdcdcdhd{\unicdcdaddd k \in {N} .  {{{m}+{k}}={n}}}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & a887fc6dd84a5c55d822e4ceb932c68ead74c9292ff8f29b32a732a2ee261b73 \\
Pure Object Address: & TMaZtSJJReNwaSNEigaPZg3GCC7FWiry1eM \\
Theory Object Id: & d1d62283501ce0525b4885ac683b5f8872a63a79b85eaa1912e4259776dcde37 \\
Theory Object Address: & TMQmi5rw5Vmk7auDTyrnNtW84cLiTH49cT4
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgihahmgjgdgjgehpfoebgehdhpfpgogfgpfmgfg}
We define $\mname{explicit\_Nats\_one\_le}$ to be $${\uniddcgcg m n .  {{{{m} \in {N}}\unicdcdcdhd{{n} \in {N}}}\unicdcdcdhd{({{{m}={n}}\unicdcdcdid{\unicdcdaddd k \in {N} .  {{{m}+{k}}={n}}}})}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8d7cd4bd6b239e3dc559142aa4d11d731c7a888de9faa3b9eeec2e7d5651c3fb \\
Pure Object Address: & TMM32WFKaju25pJnuVLyA3borpF7YFkso2V \\
Theory Object Id: & 0165a966c5de8b542de020a29a4531b3e01f1d9ab3a4aa7fba893a0bf28f0580 \\
Theory Object Address: & TMMNCaFpJUV2w4YZrBepTz2BXoitsuYhDUE
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infmd$ as an infix operator  corresponding to applying term ${\mname{explicit\_Nats\_one\_lt}}$.
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${\mname{explicit\_Nats\_one\_le}}$.
\section{explicit\_Nats\_transfer}\label{fgihahmgjgdgjgehpfoebgehdhpfehchbgogdhggfgch}Let $ N : {\iota}$ be given.
Let $ base : {\iota}$ be given.
Let $ S : {{\iota}\unicdbdjdcd{\iota}}$ be given.
Let $ N' : {\iota}$ be given.
Let $ base' : {\iota}$ be given.
Let $ S' : {{\iota}\unicdbdjdcd{\iota}}$ be given.
Let $ f : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{verbatim}
explicit_Nats_transfer
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfehchbgogdhggfgch} 
$$
\begin{array}{c}
{{{{{{{{{\mname{{explicit\_Nats}}}}~{{N}}}}~{{base}}}}~{{S}}}}}{\unicdbdjdcd}{{{{{{{{{\mname{{bij}}}}~{{N}}}}~{{N'}}}}~{{f}}}}}{\unicdbdjdcd}{{{{{{{f}}~{{base}}}}={{base'}}}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad n \in {{N}} .  {{{{{{f}}~{{({{{{S}}~{{n}}}})}}}}={{{{S'}}~{{({{{{f}}~{{n}}}})}}}}}}}})}}}{\unicdbdjdcd}{{{{{{{{\mname{{explicit\_Nats}}}}~{{N'}}}}~{{base'}}}}~{{S'}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3a37116910f44ef4e3c8921b5dcaba3ab229f567fd494a0d9f6d3fd6ac9823f8 \\
Pure Prop Address: & TMGVh4mHULAwdH24Rh3RJUPVxrmkg1EWVue \\
Theory Prop Id: & 6c4761bc5fcc2f65480e8a6ac8bd7faf5d89a85926881bb7e4724dd397f0746d \\
Theory Prop Address: & TMbddV6bagEzzT8wfXKJuLdPeN4XyXPbp2U
\end{tabular}
\end{center}

\end{theorem}
