\chapter{Rings II}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfdgbgchchjgfgch}
We define $\mname{CRing\_with\_id\_carrier}$ to be ${\uniddcgcg Rs .  {{Rs}~{0}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f0bb69e74123475b6ecce64430b539b64548b0b148267ea6c512e65545a391a1 \\
Pure Object Address: & TMY8sbcPiVs9VL311KPHpbm67U6sLM9JvF7 \\
Theory Object Id: & 9211e41eaf81bb8c152618cbe35230be60d736fcd5684c0b7bdc5ccc1ff70181 \\
Theory Object Address: & TMZQE6tPrFvJMaBcLrcMn85ZgscSeFbm4pT
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfahmgfhdh}
We define $\mname{CRing\_with\_id\_plus}$ to be ${\uniddcgcg Rs .  {{\mname{decode\_b}}~{({{Rs}~{1}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6968cd9ba47369f21e6e4d576648c6317ed74b303c8a2ac9e3d5e8bc91a68d9d \\
Pure Object Address: & TMYTM1QQGqgVyRM9unR8CLL2scwRHYvV3c3 \\
Theory Object Id: & ed06aa34b4112f8507370b46c1c5c7de7f2f9af4f24b831d45893ad3066e994e \\
Theory Object Address: & TMRiY7KU6BpU28KD19iwgBDLsQ5XyfpcbYL
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfngfhmgeh}
We define $\mname{CRing\_with\_id\_mult}$ to be ${\uniddcgcg Rs .  {{\mname{decode\_b}}~{({{Rs}~{2}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4b4b94d59128dfa2798a2e72c886a5edf4dbd4d9b9693c1c6dea5a401c53aec4 \\
Pure Object Address: & TMQSTL5b71ddbjnkjnGXfRZ61uXWmMGwJHD \\
Theory Object Id: & 7eb39ed695c795e4451a9252d011d377d0f4bdf0bfe6193f7a31ceb58f687a40 \\
Theory Object Address: & TMaJmzoi8UnDNTAXrAvZxYbTeEdKV3viygg
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfkhfgchpg}
We define $\mname{CRing\_with\_id\_zero}$ to be ${\uniddcgcg Rs .  {{Rs}~{3}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 61f7303354950fd70e647b19c486634dc22d7df65a28d1d6893007701d7b3df4 \\
Pure Object Address: & TMJzMmYjL1HdXDWMSRf7c775tmGDc6osaRL \\
Theory Object Id: & b74fb66a398c6c647d135ea9283353963f66d301d2c1ee126b203679f2071094 \\
Theory Object Address: & TMHQo21kvxiD8yab3ek4ATBz2PBfwvqsmaJ
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfpgogfg}
We define $\mname{CRing\_with\_id\_one}$ to be ${\uniddcgcg Rs .  {{Rs}~{4}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 57e734ae32adddc1f13e75e7bab22241e5d2c12955ae233ee90f53818028312a \\
Pure Object Address: & TMV8UDBZRqv4jocV6zt17aP89PcYugzQkoU \\
Theory Object Id: & b2fa78f7f58b95f4bc4f46ac268c3a959090897e56338c64bd84a73bc5fc2551 \\
Theory Object Address: & TMWFb9uZk2JEesS9quTe9a6Ww4ND9VcbBJA
\end{tabular}
\end{center}

\end{definition}
\section{CRing\_with\_id}\label{decfjgoghgpfhhjgehigpfjgeg}Let $ Rs : {\iota}$ be given.
Assume the following.
\begin{equation}
{{\mname{CRing\_with\_id}}~{Rs}}\label{hyp40:iecfdh}
\end{equation}
Let $R : {\iota}$ be ${{\mname{CRing\_with\_id\_carrier}}~{Rs}}$.
Let $zero : {\iota}$ be ${{\mname{CRing\_with\_id\_zero}}~{Rs}}$.
Let $one : {\iota}$ be ${{\mname{CRing\_with\_id\_one}}~{Rs}}$.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${{\mname{CRing\_with\_id\_plus}}~{Rs}}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${{\mname{CRing\_with\_id\_mult}}~{Rs}}$.
\begin{verbatim}
CRing_with_id_eta
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpffgehbg} 
$$
\begin{array}{c}
{{{{Rs}}={{{{{{{{{{{{\mname{{pack\_b\_b\_e\_e}}}}~{{R}}}}~{{({{{{\mname{{CRing\_with\_id\_plus}}}}~{{Rs}}}})}}}}~{{({{{{\mname{{CRing\_with\_id\_mult}}}}~{{Rs}}}})}}}}~{{zero}}}}~{{one}}}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 19895bd57673dd78940963d6fcc41b374e3914364fcfea397ea66c6fbf664993 \\
Pure Prop Address: & TMGYeUaTmA7FDSErSMoGpiYWt7ZcZFFdt71 \\
Theory Prop Id: & d44bbbcb20f869f08519c1b4ae75e3aa5154362f4fff11b557d1e7203da89831 \\
Theory Prop Address: & TMJMAQYbxKT8R2VWNpVMaASpWXQHbY8dnP7
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_explicit_CRing_with_id
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpffgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgeg} 
$$
\begin{array}{c}
{{{{{{{{{{{{\mname{{explicit\_CRing\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{({{{{\mname{{CRing\_with\_id\_plus}}}}~{{Rs}}}})}}}}~{{({{{{\mname{{CRing\_with\_id\_mult}}}}~{{Rs}}}})}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a3ff783737e4d8958b2aa7415fe17473670a67c35da28139dff7bae3f4e94735 \\
Pure Prop Address: & TMVhXNKTXiit8PdcpXCyihn8b4FTsC3k2ej \\
Theory Prop Id: & 56ddec707e12204d0adbd96c68e0500a77d81ad8852f7ce843d1a89f076bed97 \\
Theory Prop Address: & TMEtWQ6ajg8K49oJHzYUKgUUcZG8mV9k9CD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_zero_In
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfjeog} ${{zero} \in {R}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d1c133446d084c259b4e26e8455730b6db88c0480b50cfe8c1548ebaac397411 \\
Pure Prop Address: & TMUd78nxJNekmpXHWS1gxBmHFVqBbVXqURF \\
Theory Prop Id: & 42b83047b5470f202412a31f5819c2bcfd6ce9af636f261d3171012400a8362c \\
Theory Prop Address: & TMHL6R5QUphtzjmu3bzsfeJdq6c3Yemfgg6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_one_In
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgogfgpfjeog} ${{one} \in {R}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2fa10721fd9208ab1e1eda4402ab18280e5076b055a04f23501ee00c86ae3bd6 \\
Pure Prop Address: & TMSn9V5PkmSZNhoiJE1BXRDWi4AyqGo5tEs \\
Theory Prop Id: & a53700e2c16d4d39a135c22a89b655a707721c850f4b02f791f7b5962324450e \\
Theory Prop Address: & TMHiL2AUU8VvaHXP7gKgkrGeZd2daCDT76Y
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_plus_clos
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgmgpgdh} ${\unicdcdadad x y \in {R} .  {{{x}+{y}} \in {R}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 66b3347c3b4cc8181cb587a10e6fdddaf8f1db0dfaedebf691206c43b5454f81 \\
Pure Prop Address: & TMaPdKX5KfZy52M1fsgS698CBznuSXjAAQq \\
Theory Prop Id: & d2fae7d02aba4468a0d3e7ae865a7175216a2064cc2a83eac8524bf761ae8665 \\
Theory Prop Address: & TMSuXgDfq9vWRJXbJvdfjSGgSqjU13XUvKZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_mult_clos
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfngfhmgehpfdgmgpgdh} ${\unicdcdadad x y \in {R} .  {{{x}*{y}} \in {R}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ef950216b478ee5ac786dcd5b26724cf2b7cca1507f263cf09aa4d17c6a4cfdc \\
Pure Prop Address: & TMRK1cL4HUwW4gVfA7fWYbzoNAqvrXFqkd6 \\
Theory Prop Id: & 81665379575211b266779e952c3b4b18fd01a04f7da8eee59fb234fffb1db011 \\
Theory Prop Address: & TMbGpmv6AAcSZfaNEN3rm5PX6sRS59HttJi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_plus_assoc
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfbgdhdhpgdg} ${\unicdcdadad x y z \in {R} .  {{{x}+{({{y}+{z}})}}={{({{x}+{y}})}+{z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 454cc66248a33dc6e34bc2d7c3406f6ea1034419dd0abe5e4915b38af1bdd1da \\
Pure Prop Address: & TMQjX1emD1dnLgUKfE941oVUGCfDQyMUpXT \\
Theory Prop Id: & f2fe8f25a1fc149692ba6c28a8f4d1838e62305907ba78cf398ef5c4730d85f2 \\
Theory Prop Address: & TMca3P6Uj8MFLwDfmKJw24JLqCBdBiTo2ge
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_plus_com
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgpgng} ${\unicdcdadad x y \in {R} .  {{{x}+{y}}={{y}+{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e1ec1adb066b85b12e0506e4fc204093d7e6ada60496967a6728d34eff569554 \\
Pure Prop Address: & TMPUNCr5oiXd8PKxvprAqJ3n8qdBby2zkwy \\
Theory Prop Id: & 6b52cfd60b1677666cfc2a418ff72124083d95553587c923415f05e9d2660cfc \\
Theory Prop Address: & TMYoTWDw5hq6S5t6qWKJAQSbseTkUH3rGXK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_zero_L
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfme} ${\unicdcdadad x \in {R} .  {{{zero}+{x}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f35d5e2cb4c5f2f6924a8a216db8a83b2419462902ed4931aafb8448de773de7 \\
Pure Prop Address: & TMMv4dCHoLPd63XLsyBEpxxQatyYjuAN6Zd \\
Theory Prop Id: & f987b8eb4b1d1c03ffa91d2acf41d423fbb463f0f6ff54054d915245384b9664 \\
Theory Prop Address: & TMZiPp7aZHNZCiWPSvz3S9vEUNYuY1ef5Ce
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_plus_inv
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfjgoggh} ${\unicdcdadad x \in {R} .  {\unicdcdaddd y \in {R} .  {{{x}+{y}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 39fc1073cf2b1717e43d5e37e722ec6dc5e2762de4efea8b60fcd83168259e8b \\
Pure Prop Address: & TMJppCMEt4Wjhgfzc6osCgs8pyrPW7A2t3q \\
Theory Prop Id: & 8dbe3e89f0ed03c869c48edbd9729c9e9e07f83c48e1fc41cf4ce63726a55703 \\
Theory Prop Address: & TMGEihSCgFbz19W1WMiKWFqirbHZRxBnwEk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_mult_assoc
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfngfhmgehpfbgdhdhpgdg} ${\unicdcdadad x y z \in {R} .  {{{x}*{({{y}*{z}})}}={{({{x}*{y}})}*{z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fa25d807da6b86aa2872ac8f4b6ce9af0dde8c126b739a180e2292a5ad0b7dc0 \\
Pure Prop Address: & TMTGLRHnb5NytZEW9BtTjmjgzSoYUdX3Lq4 \\
Theory Prop Id: & 09949174d310e1abf6b516643ecbf69fb2cf7e3fb36f2b3cc266eaffaa5cca61 \\
Theory Prop Address: & TMUmkRGj1nHwhjroNxwFzc3LpQcb2T4SgJr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_mult_com
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfngfhmgehpfdgpgng} ${\unicdcdadad x y \in {R} .  {{{x}*{y}}={{y}*{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8fc88e1ed947c8d1d020e3f1b2c9ae9d85ce481324a851dcaf7ac3e82d522fb3 \\
Pure Prop Address: & TMUSB3uan5mCMRByLcZb9Vf6XGJLEqvGAx2 \\
Theory Prop Id: & 993072235b78d59978f6d2d7cf20206ad064f19386577afc365ea4ffde99e012 \\
Theory Prop Address: & TMbZ4NWw66ZTcKKd4JXSjKenmXtKidd92WT
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_one_neq_zero
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgogfgpfogfgbhpfkhfgchpg} ${{one}\unicdcdgdad{zero}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cedcbebb970be20c670e00da3c0b87ab77a367e70926a4ed9f074b2be9008982 \\
Pure Prop Address: & TMEvCCzeCPquYLSEU7q1oMEzpWzipFajv3Q \\
Theory Prop Id: & ec7109346aee40725228c175e17b9274815d864e0391c1d1a02806855544bd46 \\
Theory Prop Address: & TMX7e8dpinoTbP3eGKDcZggchnnnzddqYNo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_one_L
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgogfgpfme} ${\unicdcdadad x \in {R} .  {{{one}*{x}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a7a0f95242895f6eb543a18d764276740cde1e7c97815da94792785f6d715289 \\
Pure Prop Address: & TMMDR8jBbmxxtSxnqMkUtFxddjJTP4p9AoR \\
Theory Prop Id: & 47ab0ad2e91b36e068e15b85e2ae4556a99d2d2131d1a80be5fbc3485fcd84a8 \\
Theory Prop Address: & TMZnbveBuCsuGB8UqSdxmfU8pxPepufVw7K
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_distr_L
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfegjgdhehchpfme} ${\unicdcdadad x y z \in {R} .  {{{x}*{({{y}+{z}})}}={{{x}*{y}}+{{x}*{z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3c94070ae4c81515b83396b01a1abf18f8fb887ede6f676ce628a4dd5c373902 \\
Pure Prop Address: & TMRDgjKhiZf81J84szN54xfkhAS79YaDiGY \\
Theory Prop Id: & aca955a68afb3f852001bc0ad5cef20f02c96080f226c19c097a0acaeca82731 \\
Theory Prop Address: & TMYojyDz1DaZZMWZU9guJSxD1TDFN4qyKXy
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpfpgngfghgbgpffgihah}
We define $\mname{CRing\_with\_id\_omega\_exp}$ to be $${\uniddcgcg x .  {{{\mname{nat\_primrec}}~{one}}~{({\uniddcgcg k r .  {{x}*{r}}})}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b079d3c235188503c60077e08e7cb89a17aa1444006788a8377caf62b43ea1ea \\
Pure Object Address: & TMQDSzK4zGei1WaFxwYxfp5T1fYD9frJ1iE \\
Theory Object Id: & 5d35489a6173669c2175e151eba6c7c0d9bd86c956b8a3cbee0b8aa433d69a7a \\
Theory Object Address: & TMQgksRuPWDCMf6N4hRujxQQ6p1EcFejvED
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}}
We use superscripts as notation corresponding to applying term ${\mname{CRing\_with\_id\_omega\_exp}}$.
\begin{verbatim}
CRing_with_id_omega_exp_0
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgngfghgbgpffgihahpfad} ${\unicdcdadad x .  {{{x}^{0}}={one}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8b9c8bf0cedf602ad64ec9fda9404cd08eaea17ebf9730500f9d73a231c12db0 \\
Pure Prop Address: & TMKBtqa6CgMy36XtRCUkiY5qZML3T3omNvz \\
Theory Prop Id: & 64d60c82466552e43c260e08ac60fa038064ba97a7b299601bb5ac348d15e92d \\
Theory Prop Address: & TMU64mwxKSqZr95cwqeqp8gLtWdfbUdGauU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_omega_exp_S
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgngfghgbgpffgihahpfdf} ${\unicdcdadad x .  {\unicdcdadad n \in {\mname{omega}} .  {{{x}^{({{\mname{ordsucc}}~{n}})}}={{x}*{{x}^{n}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 14d493dd404e3f9509a3156f2272e3c51abbd469b9e5a348093995321cdc02c7 \\
Pure Prop Address: & TMaPKnDcmp98SwqmHGsP6Upmm4LVc7HBYeY \\
Theory Prop Id: & b501f7792ce7723a2549037b7664ccee4a1f7319ecbe7ec95d81d30ee5d64db7 \\
Theory Prop Address: & TMWJS21wHv8n2fKeHv1VWF6sSsyo6xbsLgo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_omega_exp_1
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgngfghgbgpffgihahpfbd} ${\unicdcdadad x \in {R} .  {{{x}^{1}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 730a1c203f7c249e3caf69aa7f389915ff525f30f92b1343d270b5df775e11ff \\
Pure Prop Address: & TMWRcHBBm5BHyxkidxbDUj99jsLbDdcXpMk \\
Theory Prop Id: & d2a867dea7b48e2f9e3089f5db74c3d8470de6f670f9209a78e953d06761fa8e \\
Theory Prop Address: & TMZwVw12XXo388yfUGycKftBC8osJcNPCHv
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
CRing_with_id_omega_exp_clos
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfpgngfghgbgpffgihahpfdgmgpgdh} ${\unicdcdadad x \in {R} .  {\unicdcdadad n \in {\mname{omega}} .  {{{x}^{n}} \in {R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9a2b5725819918b6748494bfa537f50d0ca70b39d8c1e8ac3ac748fbeccec3f9 \\
Pure Prop Address: & TMXNCAZsnHcpmBbcTyxVYrdZgESRVaFBJ13 \\
Theory Prop Id: & a996c7c3b925951b4e2d7bbb01fcc9986e58880420715d9c42b7d108ffc16761 \\
Theory Prop Address: & TMc79AxZxe6P15NYTfHWGFMuKcAwNRAnJsW
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgegpffgghbgmgpfahpgmgjh}
We define $\mname{CRing\_with\_id\_eval\_poly}$ to be $${\uniddcgcg n cs x .  {{{{\mname{nat\_primrec}}~{zero}}~{({\uniddcgcg m r .  {{{{cs}~{m}}*{{x}^{m}}}+{r}}})}}~{n}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b84ca72faca3a10b9b75c38d406768819f79488fbad8d9bee8b765c45e35823c \\
Pure Object Address: & TMUwUn45GuDKgSXWDvDMPcovuhY4uP1dZdG \\
Theory Object Id: & 808af0dde5838cc9e9caab3e4c3a545899005ebfaec703c548a438c00a522768 \\
Theory Object Address: & TMTHaSMuk9FXH4zmYumMT1hCMdrHTXWYL3V
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
CRing_with_id_eval_poly_clos
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpffgghbgmgpfahpgmgjhpfdgmgpgdh} 
$$
\begin{array}{c}
{\unicdcdadad n \in }{{{\mname{{omega}}}}}{ .  }{\unicdcdadad cs \in }{{{{{R}}^{{n}}}}}{ .  }{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{{{{{\mname{{CRing\_with\_id\_eval\_poly}}}}~{{n}}}}~{{cs}}}}~{{x}}}} \in {{R}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e579be29fc0b739e1e606a16df30fd76865f842f7859988a490019039a140bfb \\
Pure Prop Address: & TMSCLopfevPZB8YYCtqzjREB3sftpBvTih7 \\
Theory Prop Id: & b40a29975dbc63c22e581f918f9362b2bd0b03c27af7e307e9ac129426d92073 \\
Theory Prop Address: & TMZXvJWRJta8nKp7RX1mQcytfayt5Sk89bB
\end{tabular}
\end{center}

\end{theorem}
