\chapter{Rings}
\section{explicit\_Ring}\label{fgihahmgjgdgjgehpfcfjgoghg}Let $ R : {\iota}$ be given.
Let $ zero : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfcfjgoghg}
$\mname{explicit\_Ring}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & aa9e02604aeaede16041c30137af87a14a6dd9733da1e227cc7d6b966907c706 \\
Pure Object Address: & TMKWfmiqi9982enMMW61SmX2e5KJYZZRvW1 \\
Theory Object Id: & 9c479e9dd34e64c77a730debb88d122fdd5adfceda11ca779159e45aed2bc6dc \\
Theory Object Address: & TMJC4zWDzgdV3bp53NDJM4PjrbuESuq67yR
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Ring_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfje} 
$$
\begin{array}{c}
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}}{\unicdbdjdcd}\\
{{{{{zero}} \in {{R}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{({{{{x}}+{{y}}}})}}*{{z}}}}={{{{{{x}}*{{z}}}}+{{{{y}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}{{\mname{{explicit\_Ring}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 22c5848914731e1acb3f2bdd3b5bea1e0b842aaaa63773bdad8403ec9062cf0b \\
Pure Prop Address: & TMbhVQoNomR8RucZMffmjCGsSENbsaFffzF \\
Theory Prop Id: & c833f7cffb3a99d6a671445f80dbc49660a3082bc66d24ff01289ad8615ffb3b \\
Theory Prop Address: & TMWeeT9b2ScxzB9LDbXgaQkiZTzmNTSjyAf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_Ring}}}}\unicdbdjdcd{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}\unicdbdjdcd{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{zero}} \in {{R}}}})}}\unicdbdjdcd{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{({{{{x}}+{{y}}}})}}*{{z}}}}={{{{{{x}}*{{z}}}}+{{{{y}}*{{z}}}}}}}}}})}}\unicdbdjdcd{{q}}}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_Ring}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 950aaf3139b76e70ba05068465d32a78e3f118d81f4d1e94b22cced92de5bfd0 \\
Pure Prop Address: & TMQfB6fMj33EVzRKYCyD87MzvedosSwVhJD \\
Theory Prop Id: & 4b8365d9c8e0b8b788552aff606ae36d533041b7da02b2cec22a70afcfbd1597 \\
Theory Prop Address: & TMJpTMc6Ws4ojK4kibHze5L8RFuTnDjA4Dk
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdh}
$\mname{explicit\_Ring\_minus}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 2f43ee814823893eab4673fb76636de742c4d49e63bd645d79baa4d423489f20 \\
Pure Object Address: & TMaKRKGs3HSLGHhE6tiRaiCAnrUSperUAZx \\
Theory Object Id: & 39f82b17ca020bfc8f422ff1f573e4b4d16cb568809ce43d0dd8180c479bac80 \\
Theory Object Address: & TMHJ1R7iBuvhhAf2k1Cz8ffCtedaaEHuKX8
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${\mname{explicit\_Ring\_minus}}$.
\begin{verbatim}
explicit_Ring_minus_prop
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdhpfahchpgah} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{\prenc{{x}}} \in {R}}\unicdcdcdhd{{{x}+{\prenc{{x}}}}={zero}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1505204a877b431f2568dc7ac6d12545244a55ed333849833f1c46b8183d336e \\
Pure Prop Address: & TMRsPoCLMDVwLK3rcKy5p43qryZKDLTiRyB \\
Theory Prop Id: & 611ba38f9c0f91f22d522aa1088c3a0d2e970bdac08517c046f57e9723dea677 \\
Theory Prop Address: & TMEt9CzbdZzeQX9Zc7KR9eWrwfT3fpbr79B
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_minus_clos
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdhpfdgmgpgdh} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{x}}} \in {R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f7fd70d2da1e992a18a6daffc8e53b6d72df3587a6d38db3c311d3d07eadeb34 \\
Pure Prop Address: & TMMXdMN1Ek9HzsMkM2k8YJ2yoC8vLSVSxaF \\
Theory Prop Id: & 407c5021d140befb145ee35be8f062958adbf49ed32321837f9bdfd8cbf8bbf3 \\
Theory Prop Address: & TMFPcMzjC3fh84y93frtUFrQHpvWkhBH7dU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_minus_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdhpfcf} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{x}+{\prenc{{x}}}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 50d8d21d95cbe4b19e35eceb1a27541f47149bceed25c6463ea708464904f821 \\
Pure Prop Address: & TMX1UUFqGBXBNndnGRpkvSGovMpgc9gU2DF \\
Theory Prop Id: & f36bcb516e35dbe4a659c52f22434f2db5232803762843e14d255d39ff7cfe6f \\
Theory Prop Address: & TMZLsVX3DiMMGuzxPY5SdVeZeJrSUrUPMu1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_minus_L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdhpfme} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{\prenc{{x}}}+{x}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f88f84d640e937f6b72601b5dab987366579483fa4d481bcdda23f4a4ccf24c \\
Pure Prop Address: & TMKnaY97FsvKqr4oNHqfkqDUzfWR5EDriF8 \\
Theory Prop Id: & 265b233b823a9b5403a7808c8d9fe40e67443a240aa436ac39880031c4b97c6b \\
Theory Prop Address: & TMJDyjNAiaJZm8otfnLTZeaKs3qBbk4a5En
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_plus_cancelL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfahmgfhdhpfdgbgogdgfgmgme} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x y z \in {R} .  {{{{x}+{y}}={{x}+{z}}}\unicdbdjdcd{{y}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d0971cc93610ddafc2ae881eca4b9cc1f517b4d2883cf319421aee337430896 \\
Pure Prop Address: & TMZdhjuSoUtSbh7ZariasMQr3GnYBuCj2DP \\
Theory Prop Id: & 29aba412161a15a184e51ae63d56496c3de978192ab699d167c460212c724412 \\
Theory Prop Address: & TMF4XmuUfy2u5jbYgngzAWNZqQjoXEqyx7T
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_plus_cancelR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfahmgfhdhpfdgbgogdgfgmgcf} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x y z \in {R} .  {{{{x}+{z}}={{y}+{z}}}\unicdbdjdcd{{x}={y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & faa841b125d630a9a1f491a07ed3a5d60de8dd20716db81e18b6f781bdc4684b \\
Pure Prop Address: & TMcgiwGBhdYyV5TGZfhy58toP2rsnQBF51d \\
Theory Prop Id: & db44c76a5e03e020f6aecd4b489349da20eea01ed3ccb5c1e7aba14d3b807824 \\
Theory Prop Address: & TMPsdV2xq6oy1c4yFNQy1vMJWTw1hohLykV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_minus_invol
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfngjgogfhdhpfjgogghpgmg} ${{\mname{explicit\_Ring}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{\prenc{{x}}}}}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d53c5c6286ff24824884d7e268b83ab80bc56b72e3ac4a5d7f66f254d781235c \\
Pure Prop Address: & TMRSgzKJYUXvGzJtkNSKyvXy2ejXYwUhA9g \\
Theory Prop Id: & ae91428e6764c3c11715f8090decf3cb92e118e24893f18575481d2e6e141b7f \\
Theory Prop Address: & TMb8n5HKH6hot5PBfq3FJxG7Uy6tzs4YLHa
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_Ring\_with\_id}\label{fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgeg}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgeg}
$\mname{explicit\_Ring\_with\_id}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 51b1b6cf343b691168d1f26c39212233b95f9ae7efa3be71d53540eaa3c849ab \\
Pure Object Address: & TMdaa5S4BKNjpqS1g4ZsN2vwScQyufyRHC2 \\
Theory Object Id: & 3383bfe28df5b99c25f43d596c0ef0217f346f7b4b9482bb0cbae34091149924 \\
Theory Object Address: & TMPc9cZFPkXaxhQPst97YbsFqjZe58N9wQs
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Ring_with_id_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfje} 
$$
\begin{array}{c}
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}}{\unicdbdjdcd}\\
{{{{{zero}} \in {{R}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{{{one}} \in {{R}}}})}}}{\unicdbdjdcd}{{{({{{{one}}\unicdcdgdad{{zero}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x \in {{R}} .  {{{{{{x}}*{{one}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{({{{{x}}+{{y}}}})}}*{{z}}}}={{{{{{x}}*{{z}}}}+{{{{y}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}{{\mname{{explicit\_Ring\_with\_id}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2811338562140c0cd2270de2c5b8b90a2220baae01b626fc5a2384dc56f6ee59 \\
Pure Prop Address: & TMJooYZ4CrgUzVo3Bzu48i5pHmBC9ifXNhY \\
Theory Prop Id: & 0109ea8d1cdf78b4c4198b9dc0579e38153af90331137e279dca9bb43be8a24b \\
Theory Prop Address: & TMZPzA5o83etUX2nE84DdwyKQ7dHD7hyBLA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_Ring\_with\_id}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{zero}} \in {{R}}}})}}\unicdbdjdcd{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{{{one}} \in {{R}}}})}}\unicdbdjdcd{{({{{{one}}\unicdcdgdad{{zero}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{{{{{x}}*{{one}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{({{{{x}}+{{y}}}})}}*{{z}}}}={{{{{{x}}*{{z}}}}+{{{{y}}*{{z}}}}}}}}}})}}\unicdbdjdcd{{q}}}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8ccd42001003ed1d73a68a98715061082c13cf9b4045c5ad0972d6d2a4abc865 \\
Pure Prop Address: & TMRhQLAyL1ePgWjSAjbaKVJM3aPA2Kad84X \\
Theory Prop Id: & 94e4966c9127d4ec26511ff21d9016555b1c64c09b5a25b9a0ff7b14ca157b51 \\
Theory Prop Address: & TML8qDN4dhpVpcJvnzRzd6pGv3x7VGoQ4ZE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_Ring
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfcfjgoghg} 
${{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{{{{{{{{{{\mname{{explicit\_Ring}}}}~{{R}}}}~{{zero}}}}~{{plus}}}}~{{mult}}}}$.
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & de7598000bb3e8d9d0c079d8c393c0647add3611485f554beb972cd63b0c3e18 \\
Pure Prop Address: & TMN4a8Jp21Suwa418T4HpRTPuYS9i9K2pG9 \\
Theory Prop Id: & 6333af3f823898e2e5ef5587ca605674e78e08fc142b015e8dde0012a1de2ec4 \\
Theory Prop Address: & TMc6f6BJAGYUkRp6vVLE5Qq4oekR9n7gJ85
\end{tabular}
\end{center}

\end{theorem}
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{{{{\mname{explicit\_Ring\_minus}}~{R}}~{zero}}~{plus}}~{mult}}$.
\begin{verbatim}
explicit_Ring_with_id_minus_clos
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfdgmgpgdh} ${{\mname{explicit\_Ring\_with\_id}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{x}}} \in {R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5a4877220e6d8a5f449750b45b954c43d7bb295e3e890da80fd7c2235434f467 \\
Pure Prop Address: & TMPQuSyrrDPcLZfuACKu4c53aSTWev3qgN5 \\
Theory Prop Id: & 3cfc7850da9c3580b1c5ea83a321bd1140e03b38529cd3d45e38826d00c9ef51 \\
Theory Prop Address: & TMWoZMxoSrCdixGNZ9VBKwUMqr5CAaYD96g
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{x}}+{{\prenc{{x}}}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f46952af2450086f002e85d2d6e0556f7f24acc2118735482f95a69d45fa52ab \\
Pure Prop Address: & TMHCSKcKw6w715v3zWTNQjH8owToUBSXdea \\
Theory Prop Id: & 8841ef802d29f2a91dcb38ac2f2ee8e696c5b4536b7328b1511b09500d2d0012 \\
Theory Prop Address: & TMWtKvbayU8SfroSFkejQVC6W6nbnfrvb1B
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{\prenc{{x}}}}+{{x}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e8d98642ee9931149e776bcdddbfcdf98466a43b2db827516266be45bd30d348 \\
Pure Prop Address: & TMb7CRWhEaMLL4W5WF5t5amnUDdRobFSVb9 \\
Theory Prop Id: & 165cdf21cd0f400b4f6c03be7116abc9566fabac1d816fc347de2a525694e3b9 \\
Theory Prop Address: & TMX35b4kkmEtvQXdySEQugbu9V37WDaikHr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_plus_cancelL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgbgogdgfgmgme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x y z \in }{{{R}}}{ .  }{{{{{{{x}}+{{y}}}}={{{{x}}+{{z}}}}}}}{\unicdbdjdcd}{{{{y}}={{z}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 71bef6786a50fbc6a6a273f4a9eff4374f26d88994c8365b72e0daa0e23143e3 \\
Pure Prop Address: & TMKJ2P9pdxXugWYcPhKAPqtjdx8qCYhWmMY \\
Theory Prop Id: & 85138e19f6a6723c0ea841496568c64f40c18e1db10b2723c6d77f8596e268df \\
Theory Prop Address: & TMVGif5zhTjdUyXp5anvQUtBGG5rfbX7ddZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_plus_cancelR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgbgogdgfgmgcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x y z \in }{{{R}}}{ .  }{{{{{{{x}}+{{z}}}}={{{{y}}+{{z}}}}}}}{\unicdbdjdcd}{{{{x}}={{y}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 187848b39ef969f3fde507982eafd051de7ab1e0f840087b77e121e96cd2c1fc \\
Pure Prop Address: & TMYzuoTxJr6MhTadsdKwqXhkYK3ur8MvhKJ \\
Theory Prop Id: & 302fc924e5436eb9d2e5f9b7edefcaf0847335356058020c631fbda9c01bc7b1 \\
Theory Prop Address: & TMGbuMdJUtXoPXDJ5sUq7cTdniqN9CM7pRd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_invol
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfjgogghpgmg} ${{\mname{explicit\_Ring\_with\_id}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{\prenc{{x}}}}}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7e2ce6a225ab10fc23adde10859d367f9dbabbf928990919a5bc29910205476e \\
Pure Prop Address: & TMQK76BB3wvByKH1DMd1mwhQ7mBUo3KzPwY \\
Theory Prop Id: & b433b46a9cbc815a0d2612acd26255f6df34bacc5c54530277b91926d351f631 \\
Theory Prop Address: & TMTzGdyieMSypyUHY9Q64TiWWdbBynCRuoF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_one_In
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfpgogfgpfjeog} ${{\mname{explicit\_Ring\_with\_id}}\unicdbdjdcd{{\prenc{{one}}} \in {R}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 85b0236407eef117b01e63557a6f6a217a4948757c19b01f2fb5174081d84eed \\
Pure Prop Address: & TMXLf2xnGebu3EyRH1esAtDb4r35PFjLqhZ \\
Theory Prop Id: & aed03cc170861db941e2cd313b3ec44f90bf47a77311cec49b28c6e3e4d48540 \\
Theory Prop Address: & TMGRtpEhwtc8eg1XWzU4Sk8czRAk24M35AH
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_zero_multR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfngfhmgehcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{x}}*{{zero}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4a62e9fcb1d64a183b6295fd4ed4aba9eb09b3e0d5f275fcd8cc12c94aa442d0 \\
Pure Prop Address: & TMcnjcPqg8wqwQFAz8NTDCL51KPVyypCAig \\
Theory Prop Id: & abe208295f59516f79837f5f471c2dda2bf8f33f4cf65bcfd158530eff7010c3 \\
Theory Prop Address: & TMbdUb6eVFEUNrJSreGzs2bAZr6eyyrhWfd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_zero_multL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfngfhmgehme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{zero}}*{{x}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 46fb0e1fe2518ba1e903c00b5d02eb550a82f2839ac2bc021f0537f349aec4cb \\
Pure Prop Address: & TMLkHw8gKwxRm3iSphg4bG4HnxhbaKjTqE4 \\
Theory Prop Id: & 8352e717b959e3341c61f0f05eabef91e77b66df445e9d75d2b708e96dd469f5 \\
Theory Prop Address: & TMW7Z4P7jE8uDrrpvsx73yL58TmGFqNpuwk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_mult
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfngfhmgeh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{\prenc{{x}}}}={{{{({{\prenc{{one}}}})}}*{{x}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9d127a8ccb192ce461b0057b3348e4222c87b1c14666f7af75a91213930b4bdd \\
Pure Prop Address: & TMdw33XLkkeMx1fCtBccHF6mmrg1MHhJCTk \\
Theory Prop Id: & a85fe0130867e7b63136e642b5d12bba6d678e84770dedb29cddcd2d54c237c1 \\
Theory Prop Address: & TMXjFmdfwUTe58v3XycBBnWLN3ecVdoynv2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_mult_minus
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngfhmgehpfngjgogfhdh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{\prenc{{x}}}}={{{{x}}*{{({{\prenc{{one}}}})}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8837bf363dd2a389c6264ecdd6145862e06c0d860307051430ec19cdd534d488 \\
Pure Prop Address: & TMakKZcgjKjCdtVgW3SZdCgaxwFVjQbR5Rr \\
Theory Prop Id: & c61eb6196305d87d5e1ff179d767abbaeb21b0e821b3a9aa65c5e08b2da13c70 \\
Theory Prop Address: & TMWyT8XGK3tNij3sgsKDRvCMa7UVxEV34Sd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_one_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfpgogfgpfdhbhfhbgchfg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{{{{{{({{\prenc{{one}}}})}}*{{({{\prenc{{one}}}})}}}}={{one}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f6b3aca4e35bed72696bb58194e762fe71df22af5aa2ba4a20eb3cb185e29174 \\
Pure Prop Address: & TMbKTvnVWYvy7JDi45TnZqMzLQeGTT488j7 \\
Theory Prop Id: & f15095975e8203242ccee867846db7d1ff22f185cd0eb5d42934be01a000ec8a \\
Theory Prop Address: & TMXsC4FvKMruMUkYRjfKG4VMBJC1cbu9rU9
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Ring_with_id_minus_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfdhbhfhbgchfg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Ring\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{({{\prenc{{x}}}})}}*{{({{\prenc{{x}}}})}}}}={{{{x}}*{{x}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cf6988a1ad6d9a8623c0b2b14f24faadb38aef31eae52d0060f2892b40f1403e \\
Pure Prop Address: & TMctyY5gHQHkN8MBCzjY1dQYHmXfR3DRMpt \\
Theory Prop Id: & 218d33fbe8087bda46c6ffc2373aac19b542cc5eca4aa7125ccf7b7701998f41 \\
Theory Prop Address: & TMWeA74hJJNZgWcZWB1H6PzQVHCow6mJYFu
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpffgihahpfogbgeh}
We define $\mname{explicit\_Ring\_with\_id\_exp\_nat}$ to be $${\uniddcgcg x n .  {{{{\mname{nat\_primrec}}~{one}}~{({\uniddcgcg \_ r .  {{x}*{r}}})}}~{n}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & da14f3f79323b9ad1fb102c951a6ba616694bc14e5602b46a53c3b0e4928a55e \\
Pure Object Address: & TMH1FdiM8AidR1Vbxis6wfjL483LJqfQGSF \\
Theory Object Id: & 8058d9275d3dce79f0324a94ee62abfb6077060a9ed0a22dff3624c09ede793f \\
Theory Object Address: & TMPvyvYkA2Szt3fWkneXYns8V2R3guxHXSK
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infof$ as a right associative infix operator  corresponding to applying term ${\mname{explicit\_Ring\_with\_id\_exp\_nat}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpffgghbgmgpfahpgmgjh}
We define $\mname{explicit\_Ring\_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: & 7e80cba90c488f36c81034790c30418111d63919ffb3a9b47a18fd1817ba628e \\
Pure Object Address: & TMJ6rFroSnnr3YyYokqB1fFwqTDMseMA9Pc \\
Theory Object Id: & a93ca6874dd0fc9d10e725ebdc680764de2c751fe2955a812a3550b87334ae51 \\
Theory Object Address: & TMMeQp2kjHK2x54q5VmuFKELPoVkugf6jb6
\end{tabular}
\end{center}

\end{definition}
\section{explicit\_Ring\_with\_id\_RepIndep2}\label{fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfcffgahjeogegfgahcd}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ plus', mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}+{b}}={{a}\uniadadcdcg{b}}}}\label{hyp36:ieahahhc}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp37:iengnghc}
\end{equation}
\begin{verbatim}
explicit_Ring_with_id_repindep
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcfjgoghgpfhhjgehigpfjgegpfchfgahjgogegfgah} 
$$
\begin{array}{c}
  {{{{{{{{{{{{\mname{{explicit\_Ring\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}\\
      \unicdbdjded{{{{{{{{{{{{\mname{{explicit\_Ring\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus'}}}}~{{mult'}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a5dfcc96cb00f2205c3d5f2ac6a23140d6df64432d0b8b0a6e7cbe9701a3a2b6 \\
Pure Prop Address: & TMM9oEeg2JCz3Bqz65W4NLj1nv1sKS8dasp \\
Theory Prop Id: & 67e2ce901a576edc313e31090eebfa992581693662f54b580c5d20f054153db7 \\
Theory Prop Address: & TMaNX5eBf7WxzhXPJWRFWthj8sKB2ruu2kf
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_CRing\_with\_id}\label{fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgeg}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgeg}
$\mname{explicit\_CRing\_with\_id}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 83e7eeb351d92427c0d3bb2bd24e83d0879191c3aa01e7be24fb68ffdbb9060c \\
Pure Object Address: & TMKfVuNP6dqFRwExvJ9WyXcYZ3NfhsZyNwK \\
Theory Object Id: & d75af9f3e353a0cff15b19ee5f3b63b1f8cb7ac51e67f0cc5138140b1f6e3fdd \\
Theory Object Address: & TMMxvjm7y4j3vySsRsh1Va6jygpFMDeRtdb
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_CRing_with_id_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfje} 
$$
\begin{array}{c}
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}}{\unicdbdjdcd}\\
{{{{{zero}} \in {{R}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}}={{{{y}}*{{x}}}}}}}})}}}{\unicdbdjdcd}{{{({{{{one}} \in {{R}}}})}}}{\unicdbdjdcd}{{{({{{{one}}\unicdcdgdad{{zero}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}\\
{{\mname{{explicit\_CRing\_with\_id}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 889096929a3004fb09e1dfb86cc3b031dce78b5ce5b2ab064f27905045936a27 \\
Pure Prop Address: & TMRNEU81o8JKA2Eh2gUrS2b8pFv5FoeCm3s \\
Theory Prop Id: & 679bfe2ab11592d4d80ec52820c46e5c80300e609e19aa4dc28ae56e77854229 \\
Theory Prop Address: & TMKhUWhmjdKqdspZLxVwpVyWxcqC5gtPAPX
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_CRing\_with\_id}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{zero}} \in {{R}}}})}}\unicdbdjdcd{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}}={{{{y}}*{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{one}} \in {{R}}}})}}\unicdbdjdcd{{({{{{one}}\unicdcdgdad{{zero}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}\unicdbdjdcd{{q}}}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & faabb6a45219704de2f0e3fef26389bffec0af08019c3749078473ced2cb3d11 \\
Pure Prop Address: & TMMxE19BawJennoso8H8tRbuhZucCddTgHK \\
Theory Prop Id: & efd3a525fb8c1361391f2c1f17911c282c72ed050492dba2ca64c199693f7866 \\
Theory Prop Address: & TMJJgUD4bReLi7AP1TsY9TnoFikcsgyuy3G
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_Ring_with_id
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfcfjgoghgpfhhjgehigpfjgeg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}\\
{{{{{{{{{{{{\mname{{explicit\_Ring\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fbe43396cb1d43136aff0d303b13abd85b1ea630689e55ec6a2b988778f24e48 \\
Pure Prop Address: & TMQFMJBWxHz51Y8fYrL48pNMGk7r3p4736r \\
Theory Prop Id: & 9be399985767fb38ca0d7d6e6d6b473480388de775deabbb47204f82989a81c7 \\
Theory Prop Address: & TMSCnJQ4PTpCxDB9v4DeaGQZuAAtWyEj5cy
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_Ring
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfcfjgoghg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{{{{{{{{{{\mname{{explicit\_Ring}}}}~{{R}}}}~{{zero}}}}~{{plus}}}}~{{mult}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0a1028f53dfffdb66a5bc8450b30b06f47584d5a8ebb7659caccc2431eab79cd \\
Pure Prop Address: & TMWR4HYXqHQbNAtCPpCW4WyX1g6sEgeqM81 \\
Theory Prop Id: & d4833d0cb5524bc30358a3bb532e4e71813c9a5770dc5a75251e671d49156b0c \\
Theory Prop Address: & TMW54V1xY2GACHQtTgGxeQnSjcgYE13QF5h
\end{tabular}
\end{center}

\end{theorem}
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${{{{{\mname{explicit\_Ring\_minus}}~{R}}~{zero}}~{plus}}~{mult}}$.
\begin{verbatim}
explicit_CRing_with_id_minus_clos
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfdgmgpgdh} ${{\mname{explicit\_CRing\_with\_id}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{x}}} \in {R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3ae85ff26a5f71ad4869ca5b097a67259c6de609119efeb4bdc60ed927184f6f \\
Pure Prop Address: & TMdwWexqPB1YB6dqTefAgb1hYBMdY5om5oU \\
Theory Prop Id: & 0765b182f4deb4a94a40f4675d75a50065d365c9670a0ab0f49e558d0f85993d \\
Theory Prop Address: & TMJ4pj8CmckG9Wt5bG8Q52MwrXF25dyk3kb
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{x}}+{{\prenc{{x}}}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bb27a98e4f753c9ce2de93efd3a6c3a66fcfa71c58a26ed9feff5958784d9524 \\
Pure Prop Address: & TMLxMqEk88QyHzY7bcXNWKPPvM2GmbJkpT8 \\
Theory Prop Id: & 60d4131fe989a7c001f81787ae3ed44b78153d1f852ce54a3d4141b279c5c457 \\
Theory Prop Address: & TML4H1hcc9CreDDS8GT4dGMNCmQRxHBJUkG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{\prenc{{x}}}}+{{x}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 50baa96d414935b78c8004fe8327833fdc95dbb21e677a91ab1cf2c6b0fe04ca \\
Pure Prop Address: & TMaiKT6dJBUA6GYD8CEipgDz31FuNhAsVPZ \\
Theory Prop Id: & f84540b0cdb980f22b39fce9eca7602a4d61e86a70a72452220292d78080cb9f \\
Theory Prop Address: & TMWLryjTxXP9PfTDUBQTJVrMoHtCqMf2Toq
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_plus_cancelL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgbgogdgfgmgme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x y z \in }{{{R}}}{ .  }{{{{{{{x}}+{{y}}}}={{{{x}}+{{z}}}}}}}{\unicdbdjdcd}{{{{y}}={{z}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6f6e462ce78421c4a368b9489c238c0a56b788c33381051bc30b2344cc6fc9dd \\
Pure Prop Address: & TMYtj8Hh526XhqURvJhj6jZ4hduf9SfkVLZ \\
Theory Prop Id: & 1efdbbbd0d4626f6ed562dd6cf586bde2ad4047d77bf071a55596278332fd212 \\
Theory Prop Address: & TMHKn5Uz9yj1C4oNmL951CdC7QTuio1h7e7
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_plus_cancelR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfahmgfhdhpfdgbgogdgfgmgcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x y z \in }{{{R}}}{ .  }{{{{{{{x}}+{{z}}}}={{{{y}}+{{z}}}}}}}{\unicdbdjdcd}{{{{x}}={{y}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f7bef7cef51fefac0a8a968cd48339390194bc43db609d321297622f290f854b \\
Pure Prop Address: & TMXr6FaGNVmrtogzEG7TRA9wchey2iGQPw1 \\
Theory Prop Id: & 251f9b25df85d0dc24f0e3a92c389f8e0d2abf089dabb0942376c7f836fada37 \\
Theory Prop Address: & TMNaQYvw47cG7Q58RrnEKj8rrfammDMrR62
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_invol
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfjgogghpgmg} ${{\mname{explicit\_CRing\_with\_id}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{\prenc{{x}}}}}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ee28f648bb60af4ab802e7550db486a9b5f33435a2ddcfad83e57e7aeb38b90c \\
Pure Prop Address: & TMPixMacvRwLbJEEYF3Tu3BXhGhgayHXYiq \\
Theory Prop Id: & 01d19d582f4cd5e2997e85901f8234fd2844833c0ea422c25b30fb4cb7dcfba6 \\
Theory Prop Address: & TMaM5mPayy7LFWdA8ncy5w63W2sh9AEjLdV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_one_In
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfpgogfgpfjeog} ${{\mname{explicit\_CRing\_with\_id}}\unicdbdjdcd{{\prenc{{one}}} \in {R}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7608d9188365499939cb1fe551eecd223870593a73f2f473c50fdf0812b607fe \\
Pure Prop Address: & TMbawiEWXmjkJn3cNvBUYBL28Cpc9LDQEGD \\
Theory Prop Id: & 954fe6bb57ae5b479c5d7182e7aa2ca52a9d14d7226f7296a1bc495ed1c16908 \\
Theory Prop Address: & TMXjU4EzqoWzujVJA3GSZFqn43jFuMhi3Sf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_zero_multR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfngfhmgehcf} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{x}}*{{zero}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9f49c5a1afdc52b7b5433d4d3367501e3b8caf0412846c4cf5f182b8c277de85 \\
Pure Prop Address: & TMG7cDqVVyiPU92qFsQzXosDNLq1NTSreqP \\
Theory Prop Id: & 0c4690feb0a694a7e1bb0c027da7c70d01be7f914b759b801e5e9fdb4cf100c9 \\
Theory Prop Address: & TMSRjqxP1jRu2t7GgGMpBgEXn8ivZQWM9um
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_zero_multL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfkhfgchpgpfngfhmgehme} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{zero}}*{{x}}}}={{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0a092c2a6dd656ce3cf2cbab1ff88bd05ddbfb27fe53be361696f86c4312822c \\
Pure Prop Address: & TMMgnbsVdPLJ3iwrHZPnZiErXzyVeTyZRU2 \\
Theory Prop Id: & 924526e9dfa6060f77cadce478465ee75ea541ecc409f563b2ffe02f103abfd9 \\
Theory Prop Address: & TMMFp4RVmjUKJA9f9cUetYE3usofxBj3uuC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_mult
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfngfhmgeh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{\prenc{{x}}}}={{{{({{\prenc{{one}}}})}}*{{x}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2f95e375de8d8d7d33d150a3a832a3f28d3f4736facce19ec50f7bf1278b5de7 \\
Pure Prop Address: & TMc3H8URNXwHnJda77991VAXe6HmNqtnjWB \\
Theory Prop Id: & fd44c89e251ce67e81ce86520a199d0039c96c2d1f0bcfba1e2da4ebecd8add4 \\
Theory Prop Address: & TMU9zhbrpi1cxTikjTTd5CSMd1G6Kst4j5w
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_mult_minus
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngfhmgehpfngjgogfhdh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{\prenc{{x}}}}={{{{x}}*{{({{\prenc{{one}}}})}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 960b3084b8e49beeea6746780f075296d84ba89bfe0c23064365d8255960dfa6 \\
Pure Prop Address: & TMT8SWemm7sAFAGRv6i8SpVrYKufCRcTNkj \\
Theory Prop Id: & 58dd34b96bd3da4dda59ac8f027f0144f9aa188ef626da02bf86692dc0f5a89c \\
Theory Prop Address: & TMXMyqEZX2K4g8LgCYyD3LRKSt3urgcv9Gt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_one_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfpgogfgpfdhbhfhbgchfg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{{{{{{({{\prenc{{one}}}})}}*{{({{\prenc{{one}}}})}}}}={{one}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9027680ad43bbdc05b9ac2585988bf9bca1f56435309fcf8330934d3a4e55242 \\
Pure Prop Address: & TMKHMtgM4RegJL7J6H3aDWWmZYyuG6dGt4F \\
Theory Prop Id: & 27e1d09ca5cd60ad129f6b679f7062bed626f17e6e37987c960df24c3b5ef58b \\
Theory Prop Address: & TMJQU82As7FBLwuBdVYR5vt1kuAL1jNF9cr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_CRing_with_id_minus_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfngjgogfhdhpfdhbhfhbgchfg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_CRing\_with\_id}}}}}{\unicdbdjdcd}{\unicdcdadad x \in }{{{R}}}{ .  }{{{{{{({{\prenc{{x}}}})}}*{{({{\prenc{{x}}}})}}}}={{{{x}}*{{x}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cc64ff002d9d1fee374c40859d2a8b13e6a2e01c0daf12ebb732af37740d2369 \\
Pure Prop Address: & TMNzA9VqA3PfzJZ7FjCXuhvJBqkuXeLycnt \\
Theory Prop Id: & cba06f4f773cf52216bcff465b0e35eeda22efd81812f03664505820cd4d217b \\
Theory Prop Address: & TMaX7AFX3UeZnZX4SBaoUAegDF4y8TjJD2i
\end{tabular}
\end{center}

\end{theorem}
\section{explicit\_CRing\_with\_id\_RepIndep2}\label{fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfcffgahjeogegfgahcd}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
Let $ plus', mult' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdlckd$ as a right associative infix operator  corresponding to applying term ${plus'}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${mult'}$.
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}+{b}}={{a}\uniadadcdcg{b}}}}\label{hyp38:ieahahhc}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {R} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp39:iengnghc}
\end{equation}
\begin{verbatim}
explicit_CRing_with_id_repindep
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdecfjgoghgpfhhjgehigpfjgegpfchfgahjgogegfgah} 
$$
\begin{array}{c}
  {{{{{{{{{{{{\mname{{explicit\_CRing\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}\\
      \unicdbdjded{{{{{{{{{{{{\mname{{explicit\_CRing\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus'}}}}~{{mult'}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ac2d59ca206daa22783237146a060cbb078337457a0a1298597e6fcae4da5f00 \\
Pure Prop Address: & TMJtWqjqttZHff5TE3g13Vjiu7BhtNnvzfB \\
Theory Prop Id: & 6531240d433090d437bf90709c4ea3cb3ed4e135a6c52863192d1c5d24238853 \\
Theory Prop Address: & TMYe8NzBzkkswszXrNbVN74ksiBLPimnNkq
\end{tabular}
\end{center}

\end{theorem}
\section{Packing two Binary Operations and a Constant into a Set} % explicit_CRing_with_id_RepIndep2
\begin{definition}\label{def:ahbgdglgpfcgpfcgpffg}
$\mname{pack\_b\_b\_e}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\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: & c9ca029e75ae9f47e0821539f84775cc07258db662e0b5ccf4a423c45a480766 \\
Pure Object Address: & TMcBhLLE6SjWU8YK3zBnZTiJ441rzSVQZ4f \\
Theory Object Id: & 21d4d088757e7386d904218652e603fec7ce704c78740c732cc6f2bc8d0f15b9 \\
Theory Object Address: & TMT1KQaS6hSV4qnwVuKuKkuNrS6Em96tqXN
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhehchfhdgehpfcgpfcgpffg}
$\mname{struct\_b\_b\_e}$ is the opaque object of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 755e4e2e4854b160b8c7e63bfc53bb4f4d968d82ce993ef8c5b5c176c4d14b33 \\
Pure Object Address: & TMVRzggDuRW6mHLPpsN6eZtf5G2DQ1nm6ug \\
Theory Object Id: & 3be2a81c29bbdf8205c87f99ef9048632fba2bced44a1e8c51e6c55f41781fad \\
Theory Object Address: & TMYHoLuYL7HNg4NL1sS21yHunHjH3Z1FY6X
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fhogahbgdglgpfcgpfcgpffgpfjg}
$\mname{unpack\_b\_b\_e\_i}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{({{\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: & 7004278ccd490dc5f231c346523a94ad983051f8775b8942916378630dd40008 \\
Pure Object Address: & TMQ74XmyoP47CnXDEBHKEFtMzk18jjqu6dt \\
Theory Object Id: & 52a106befe8ad370345a8e6ab30f464040cc96b3bd3f78b38dc7599fc5e7de99 \\
Theory Object Address: & TMPRW7TWzKwNSZnPUoDa8Aj3P5cvnhJZi47
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fhogahbgdglgpfcgpfcgpffgpfpg}
$\mname{unpack\_b\_b\_e\_o}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}})}\unicdbdjdcd{o}}}$$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b94d6880c1961cc8323e2d6df4491604a11b5f2bf723511a06e0ab22f677364d \\
Pure Object Address: & TMVcrr5WR2rjHynX8x5DLY3reHfggeDReXu \\
Theory Object Id: & 7b0871aa00521156ece9021408011d93cc22a3a3d8be2ffab32e46cde2c7017a \\
Theory Object Address: & TMRmp4Vwef25JwbPLckTqR8B8PxPtoyHXZ1
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:cfjgoghg}
  We define $\mname{Ring}$ to be
  $$
  \begin{array}{c}
    \uniddcgcg R .  {{\mname{struct\_b\_b\_e}}~{R}}\unicdcdcdhd\\{{{\mname{unpack\_b\_b\_e\_o}}~{R}}~{({\uniddcgcg R~plus~mult~zero .  {{{{{\mname{explicit\_Ring}}~{R}}~{zero}}~{plus}}~{mult}}})}}
  \end{array}
  $$
  of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 61bbe03b7930b5642e013fa138d7c8e2353bab0324349fce28b7cbce8edce56a \\
Pure Object Address: & TMVG5WKysVhbYYd6hg9dUY2aCKLj1h9qkSs \\
Theory Object Id: & ffaf640f43cef8fec01ec428ab080a16b7b8c9fe29fc01c79b9a62fc32f9e1ab \\
Theory Object Address: & TMVey7JB9XreF71vPMXWv4MfPYVqXDJNqi5
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:cfjgoghgpfngjgogfhdh}
We define $\mname{Ring\_minus}$ to be $${\uniddcgcg R x .  {{{\mname{unpack\_b\_b\_e\_i}}~{R}}~{({\uniddcgcg R~plus~mult~zero .  {{{{{{\mname{explicit\_Ring\_minus}}~{R}}~{zero}}~{plus}}~{mult}}~{x}}})}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e5405bc7309f2aa971bcab97aadae821ba1e89825a425c7bf10000998c5266c9 \\
Pure Object Address: & TMGB3zNFrM8bRch4GNc7TY8X7Y5CDFkWQMu \\
Theory Object Id: & c725983606b8ac83202398408bea35fe4ce0b6c34d2d5411b8a4d54f4b73256f \\
Theory Object Address: & TMGzuX373w32Vo8i8c1MYDeruu5iffk14jV
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ahbgdglgpfcgpfcgpffgpffg}
$\mname{pack\_b\_b\_e\_e}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{({{\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: & 6859fb13a44929ca6d7c0e598ffc6a6f82969c8cfe5edda33f1c1d81187b9d31 \\
Pure Object Address: & TMHt74X3xjgCgvDbTBeJDSgoSU6NBFqLo3t \\
Theory Object Id: & cf1c51f21701c7f90f031360baccab3d9f9cc6bcbb438ab90424d004540beecf \\
Theory Object Address: & TMY3Jeq6qFWZoiMV17oUBbd2wzL4nynScQo
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhehchfhdgehpfcgpfcgpffgpffg}
$\mname{struct\_b\_b\_e\_e}$ is the opaque object of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 7685bdf4f6436a90f8002790ede7ec64e03b146138f7d85bc11be7d287d3652b \\
Pure Object Address: & TMMq6LTJYr6FfwYvoFthxRCCWMJeJ3PPcbc \\
Theory Object Id: & 93fa62123840de71d70cd336cd76c191a66b2a255f74ff9d886c0ce7bd229764 \\
Theory Object Address: & TMKaRBHLAH7X2upT8ygEK87KwVQkCv88tVc
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fhogahbgdglgpfcgpfcgpffgpffgpfjg}
$\mname{unpack\_b\_b\_e\_e\_i}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\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: & 0708055ba3473c2f52dbd9ebd0f0042913b2ba689b64244d92acea4341472a1d \\
Pure Object Address: & TMPWkrRKKhARHw7yZVhmEDea2FrJHMb9vQ2 \\
Theory Object Id: & e7d717c6dc1d45afea7f0ffa393d0e0f9d8162bd1099d59986e7a90eae668a3d \\
Theory Object Address: & TMPQgdNg6eUMGGtvqYwfi9ZggR6mb3tYxPU
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fhogahbgdglgpfcgpfcgpffgpffgpfpg}
$\mname{unpack\_b\_b\_e\_e\_o}$ is the opaque object of type $${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}}})}\unicdbdjdcd{o}}}$$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1bcc21b2f13824c926a364c5b001d252d630f39a0ebe1f8af790facbe0f63a11 \\
Pure Object Address: & TMLUiT5tyYDHruUZiDx7gvU1hj4TEKsQReX \\
Theory Object Id: & 3325ddb79a400302ecc0a153bdd9c21b9425489ac6ae7b8d16a00c9f9386f079 \\
Theory Object Address: & TMUV6wYXdEfCF2Zrhg4Q7de7PEc2arc5QiC
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:cfjgoghgpfhhjgehigpfjgeg}
  We define $\mname{Ring\_with\_id}$ to be
  $$
  \begin{array}{c}
    \uniddcgcg R .  {{\mname{struct\_b\_b\_e\_e}}~{R}}\unicdcdcdhd\\
               {{\mname{unpack\_b\_b\_e\_e\_o}}~{R}}~\\{({\uniddcgcg R~plus~mult~zero~one .  {{{{{{\mname{explicit\_Ring\_with\_id}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}})}
  \end{array}
  $$
  of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e87205d21afb0774d1a02a5d882285c7554f7b824ee3d6ff0a0c0be48dac31d6 \\
Pure Object Address: & TMMXH8sbGq7TCys16vmazU94M6z99RUZJ4e \\
Theory Object Id: & 5b1d1fc429c4ad1b59f175a48a3a442a9707b676450c6ff34ff21d9e21b47f80 \\
Theory Object Address: & TMHpeNjPXgpyDcsaGcgo2ZDP3VuziQZ8U4x
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Ring_with_id_unpack_eq
\end{verbatim}
\begin{theorem}\label{thm:cfjgoghgpfhhjgehigpfjgegpffhogahbgdglgpffgbh} 
$$
\begin{array}{c}
{\unicdcdadad R .  }{\unicdcdadad plus~mult : }{{{{{\iota}}\unicdbdjdcd{{{{\iota}}\unicdbdjdcd{{\iota}}}}}}}{ .  }{\unicdcdadad zero~one .  }\\
{{{{\mname{{unpack\_b\_b\_e\_e\_o}}}}~{{({{{{{{{{{{{{\mname{{pack\_b\_b\_e\_e}}}}~{{R}}}}~{{plus}}}}~{{mult}}}}~{{zero}}}}~{{one}}}})}}}}~\\
{{({{\uniddcgcg R~plus~mult~zero~one .  {{{{{{{{{{{{\mname{{explicit\_Ring\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}}})}}\\
={{{{{{{{{{{{\mname{{explicit\_Ring\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e125aaa25b8e15f0cb5142f069cd1158c31c0a22e2ba188ed03651f2b50f7f69 \\
Pure Prop Address: & TMYhZgSfEnPXAcYrzYgAs5j3TvrmvSQUYwo \\
Theory Prop Id: & 6ff04cdbf65065a1048fb4ed5c01d06bc600971c026c0e88f07528dee5a7753b \\
Theory Prop Address: & TMHgUEdaJ2656FZdQffXPyg9M1r2869W3gG
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:decfjgoghgpfhhjgehigpfjgeg}
  We define $\mname{CRing\_with\_id}$ to be
  $$
  \begin{array}{c}
    \uniddcgcg R .  {{\mname{struct\_b\_b\_e\_e}}~{R}}\unicdcdcdhd\\
               {{\mname{unpack\_b\_b\_e\_e\_o}}~{R}}~\\
               {({\uniddcgcg R~plus~mult~zero~one .  {{{{{{\mname{explicit\_CRing\_with\_id}}~{R}}~{zero}}~{one}}~{plus}}~{mult}}})}
  \end{array}
  $$
  of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 38dd910342442210ba796f0e96ab9a7e6b36c17352f74ba8c9c2db4da2aebf0e \\
Pure Object Address: & TMQgd2PoDs8mxEHY4Lw1N9XM2MuPgtY8d9w \\
Theory Object Id: & a1021e16f50fc0f2bd0b04593e51a03b9457694823e7aa3bc57cf1efe615c1f7 \\
Theory Object Address: & TMbRJRM2RQRfp7E2CEx4AJhw2m5Gxt5HthV
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
CRing_with_id_unpack_eq
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpffhogahbgdglgpffgbh} 
$$
\begin{array}{c}
{\unicdcdadad R .  }{\unicdcdadad plus~mult : }{{{{{\iota}}\unicdbdjdcd{{{{\iota}}\unicdbdjdcd{{\iota}}}}}}}{ .  }{\unicdcdadad zero~one .  }\\
{{{{\mname{{unpack\_b\_b\_e\_e\_o}}}}~{{({{{{{{{{{{{{\mname{{pack\_b\_b\_e\_e}}}}~{{R}}}}~{{plus}}}}~{{mult}}}}~{{zero}}}}~{{one}}}})}}}}~\\
{{({{\uniddcgcg R~plus~mult~zero~one .  {{{{{{{{{{{{\mname{{explicit\_CRing\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}}})}}\\
={{{{{{{{{{{{\mname{{explicit\_CRing\_with\_id}}}}~{{R}}}}~{{zero}}}}~{{one}}}}~{{plus}}}}~{{mult}}}}.\\

\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 36ff594b81ff0f9289211e517dfadc9825f390bdb5273a1c1da1b64814838ac3 \\
Pure Prop Address: & TMGSuWhhM3Pypq6dXURWZnpYUJPYcx7vkJ2 \\
Theory Prop Id: & 7707613ab3233c231329185e9013759e858082c5e03f957f33f5a266d7c92331 \\
Theory Prop Address: & TMFpD2MTMvgWJJuwcM5sqPZKwuope6VFnQg
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:cfjgoghgpfpgggpfcfjgoghgpfhhjgehigpfjgeg}
  We define $\mname{Ring\_of\_Ring\_with\_id}$ to be
  $$
  \begin{array}{c}
    \uniddcgcg R .  {{\mname{unpack\_b\_b\_e\_e\_i}}~{R}}~{({\uniddcgcg R~plus~mult~zero~one .  {{{{{\mname{pack\_b\_b\_e}}~{R}}~{plus}}~{mult}}~{zero}}})}
  \end{array}
  $$
  of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9f7755a326e730a1c98395c05032d068f1d3a5762700ae73598c3c57a6bd51ea \\
Pure Object Address: & TMJ3Jckg9eHwYuoWNm91qRwiRDGjP1Wv1u3 \\
Theory Object Id: & 119ffb040b7ae9e440cde0cba75f90e17ecab1fe0ecf8a8ace0582b41a80ab5e \\
Theory Object Address: & TMSZtFuoH5AXFQXg4j9tyqGVoKFDW7ouQ8H
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
CRing_with_id_is_Ring_with_id
\end{verbatim}
\begin{theorem}\label{thm:decfjgoghgpfhhjgehigpfjgegpfjgdhpfcfjgoghgpfhhjgehigpfjgeg} ${\unicdcdadad R .  {{{\mname{CRing\_with\_id}}~{R}}\unicdbdjdcd{{\mname{Ring\_with\_id}}~{R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 815b955355c5b9a3a4bba1901f861f2e42a8aba0b2e264541eb5237d2b7defed \\
Pure Prop Address: & TMUZNUomruVanp8ziSGJjGo6mnjbL8FcKLU \\
Theory Prop Id: & e157b3b577d0c147bf7e94da6f8ae23dc7ce8e6040bdb6473b6afe038837f0b1 \\
Theory Prop Address: & TMPJAdDaLrQhhspajeStvBhg4f1PCFGYJTp
\end{tabular}
\end{center}

\end{theorem}
