\chapter{Groups}
\section{AssocComm}\label{bedhdhpgdgdepgngng}Let $ R : {\iota}$ be given.
Let $ plus : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
\begin{theorem}\label{thm:bedhdhpgdgdepgngngpfjgegfgogehjgehjgfgdh} ${{({\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{\unicdcdadad p : {o} .  {{({{({\unicdcdadad x y z \in {R} .  {{{x}+{{y}+{z}}}={{y}+{{x}+{z}}}}})}\unicdbdjdcd{{({\unicdcdadad x y z \in {R} .  {{{x}+{{y}+{z}}}={{z}+{{x}+{y}}}}})}\unicdbdjdcd{{({\unicdcdadad x y z w \in {R} .  {{{({{x}+{y}})}+{({{z}+{w}})}}={{({{x}+{z}})}+{({{y}+{w}})}}}})}\unicdbdjdcd{{({\unicdcdadad x y z w \in {R} .  {{{x}+{{y}+{{z}+{w}}}}={{w}+{{x}+{{y}+{z}}}}}})}\unicdbdjdcd{{({\unicdcdadad x y z w \in {R} .  {{{x}+{{y}+{{z}+{w}}}}={{z}+{{w}+{{x}+{y}}}}}})}\unicdbdjdcd{p}}}}}})}\unicdbdjdcd{p}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c45653e3c80cd999509820d81f22ae3c47b5cd44421738f32eda320ba570c87e \\
Pure Prop Address: & TMGvdvL6fepmXewTz9sJwhigZicrLoSXLZZ \\
Theory Prop Id: & 40e443867ab4b8a14aafd8ab67f7ac4ae69383ab44ea2a4da6420b281d0d0628 \\
Theory Prop Address: & TMQfH9YcUAFRqr7yeAgZh2h8mk1nc3GYCto
\end{tabular}
\end{center}

\end{theorem}
\section{Group1}\label{hechpgfhahbd}Let $ G : {\iota}$ be given.
\subsection{Group1Explicit}\label{hechpgfhahbdfeihahmgjgdgjgeh}Let $ op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfhechpgfhah}
We define $\mname{explicit\_Group}$ to be ${{{({\unicdcdadad a b \in {G} .  {{{a}*{b}} \in {G}}})}\unicdcdcdhd{({\unicdcdadad a b c \in {G} .  {{{a}*{({{b}*{c}})}}={{({{a}*{b}})}*{c}}}})}}\unicdcdcdhd{\unicdcdaddd e \in {G} .  {{({\unicdcdadad a \in {G} .  {{{{e}*{a}}={a}}\unicdcdcdhd{{{a}*{e}}={a}}}})}\unicdcdcdhd{({\unicdcdadad a \in {G} .  {\unicdcdaddd b \in {G} .  {{{{a}*{b}}={e}}\unicdcdcdhd{{{b}*{a}}={e}}}}})}}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 0edee4fe5294a35d7bf6f4b196df80681be9c05fa6bb1037edb8959fae208cea \\
Pure Object Address: & TMKHXb8sJYXkkV8waqUHeCymoBGxrmp2eJ7 \\
Theory Object Id: & a0d4c8bd9f788ef787589b54b2745f33864b9386aad8d7b99e0c747d5cd502b8 \\
Theory Object Address: & TMNeD6sRqkAPQrbpVxeWHbWkWuomaavLf35
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpffhogjgbhfhfg} ${\unicdcdadad e e' \in {G} .  {{({\unicdcdadad a \in {G} .  {{{e}*{a}}={a}}})}\unicdbdjdcd{{({\unicdcdadad a \in {G} .  {{{a}*{e'}}={a}}})}\unicdbdjdcd{{e}={e'}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fe12d74789aa4b30c5b553f9b583cc7dac65508fc7b435345c330c9c50b7bda4 \\
Pure Prop Address: & TMX43i28gCdiXowFyXeB4bgH5QZTmM6g1nh \\
Theory Prop Id: & 4b4d44f80512969adc0813a098b3d4bc6f42912746d2cd4de30c9b4dc1fd8c1d \\
Theory Prop Address: & TMcvB6UWPmzCrw9QT1edWJq9i5gU4ihPnYh
\end{tabular}
\end{center}

\end{theorem}
Assume the following.
\begin{equation}
{\mname{explicit\_Group}}\label{hyp:iehe}
\end{equation}
\begin{definition}\label{def:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjh}
We define $\mname{explicit\_Group\_identity}$ to be ${{\mname{Eps\_i}}~{({\uniddcgcg e .  {{{e} \in {G}}\unicdcdcdhd{({{({\unicdcdadad a \in {G} .  {{{{e}*{a}}={a}}\unicdcdcdhd{{{a}*{e}}={a}}}})}\unicdcdcdhd{\unicdcdadad a \in {G} .  {\unicdcdaddd b \in {G} .  {{{{a}*{b}}={e}}\unicdcdcdhd{{{b}*{a}}={e}}}}}})}}})}}$ of type ${\iota}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8a818c489559985bbe78176e9e201d0d162b3dd17ee57c97b44a0af6b009d53b \\
Pure Object Address: & TMMh2NL7Q85JJXCFBeNsaMqMcMPaFhqKbfP \\
Theory Object Id: & 84a58742704bbb5cd7767ccb82e978851abf4fb9bc5ab7c27851fdc99d2cd664 \\
Theory Object Address: & TMdVb1nKZjH4P19ib11PFY6Cka8NUiF79Re
\end{tabular}
\end{center}

\end{definition}
Let $e$ be ${\mname{explicit\_Group\_identity}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfg}
We define $\mname{explicit\_Group\_inverse}$ to be ${\uniddcgcg a .  {{\mname{Eps\_i}}~{({\uniddcgcg b .  {{{b} \in {G}}\unicdcdcdhd{({{{{a}*{b}}={e}}\unicdcdcdhd{{{b}*{a}}={e}}})}}})}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e8cf29495c4bd3a540c463797fd27db8e2dfcc7e9bd1302dad04b40c11ce4bab \\
Pure Object Address: & TMHFMiwrvo9LoSX8Wi5EZvS4ccFWXeWxrgx \\
Theory Object Id: & a89687cfcbd45caa52b5cdf460d31291544f843439c0fb0cac9bd218223d0a98 \\
Theory Object Address: & TMJDvZFoNydRtF58jVXVmTRo5GVfkFbJTHb
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\postnc{-}$ as a postfix operator  corresponding to applying term ${\mname{explicit\_Group\_inverse}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfahchpgah} ${{{e} \in {G}}\unicdcdcdhd{({{({\unicdcdadad a \in {G} .  {{{{e}*{a}}={a}}\unicdcdcdhd{{{a}*{e}}={a}}}})}\unicdcdcdhd{\unicdcdadad a \in {G} .  {\unicdcdaddd b \in {G} .  {{{{a}*{b}}={e}}\unicdcdcdhd{{{b}*{a}}={e}}}}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 068ffab150dc76c7de09d187943d2888faceaba1fbdc6449b322c8d4ef63ac4c \\
Pure Prop Address: & TMM9Eh1qhaiVeZj5Wgcxuvug9QQBNRfsEoz \\
Theory Prop Id: & c36841621d7b57d11c84af6cd0ed9c8fba75205040141ec30f15c1792884c83e \\
Theory Prop Address: & TMWKjEwmnVGHJzPZq7tPzu7AEs2mtZfK8zJ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfjgog} ${{e} \in {G}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 696ec40c6c7d83676b8638c42bd7832dd823bca9c973ae6f9c4f06cfa23bfc08 \\
Pure Prop Address: & TMSoutuNF8eeWkkhpwkABkzngwXxdhPEeii \\
Theory Prop Id: & 8cf78c6448b0a5a1eafb0e5c957793ae6ea2c4988a86e53cde584dd0291d61f3 \\
Theory Prop Address: & TMHmwXi5SHMeK3Us86CEgisvDGA9xNi341B
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfmgjgeg} ${\unicdcdadad a \in {G} .  {{{e}*{a}}={a}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0a8b96c11b2713c863850c5c7d4857de37aa4fca73f7c304457b56e2f95e16e3 \\
Pure Prop Address: & TMbD19oggdaE7cVLwcWS7ssWyd1V2HcUnDW \\
Theory Prop Id: & c412492ac795885c6900db2fe22e1dd552814f2557d6d79041f6191b3689beed \\
Theory Prop Address: & TMPTJy8uG71biAxCkf8AvzGecNsAuAUaKnK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfchjgeg} ${\unicdcdadad a \in {G} .  {{{a}*{e}}={a}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f6f5808dcc0c330452a517b4ebf8456cd5238d7b46e8111ab177813e331aa8b8 \\
Pure Prop Address: & TMVgRDZiCVC1sCRnAp2nQ2asZP7Bjg3oe5e \\
Theory Prop Id: & ac30373bfbf244191de0c19f090210f9903310858129ab85808112737072b614 \\
Theory Prop Address: & TMLhbf6oyewQ17oxmbzXFC3ejnSF86C5A6t
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfjgogghfgih} ${\unicdcdadad a \in {G} .  {\unicdcdaddd b \in {G} .  {{{{a}*{b}}={e}}\unicdcdcdhd{{{b}*{a}}={e}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a48e2c7de86dcd94f3d0b7870a3a456284feaaf5d5c20e80a45b93114c6d50d5 \\
Pure Prop Address: & TMW4eSZUkr3refSrUsK582eNHJhJwavEYV6 \\
Theory Prop Id: & aee17204445b1eac60e7b66a3cdd8608a0182bd2a434fc82de1a92678591d2a3 \\
Theory Prop Address: & TMTWCgk93fRtERh1PSJNhibGca6EnEgcnfe
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfgpfahchpgah} ${\unicdcdadad a \in {G} .  {{{\postnc{{a}}} \in {G}}\unicdcdcdhd{({{{{a}*{\postnc{{a}}}}={e}}\unicdcdcdhd{{{\postnc{{a}}}*{a}}={e}}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f17df9988cfc01139158b40656a874d8f2118364e3b47b12b829509448c3c11 \\
Pure Prop Address: & TMNhTk43Kf2YzVaFqj6KragMTmudKkw3kGf \\
Theory Prop Id: & 6781d5952539e6702dfb38b38d848b596c60f3f0e775d5ca957f11e8938fcfe3 \\
Theory Prop Address: & TMMJ2fwNJJe1W18rM6iSWAfyEcKkyVumryi
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfgpfjgog} ${\unicdcdadad a \in {G} .  {{\postnc{{a}}} \in {G}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f9bac9fe458ed7636280b89adbff7d9c00215f5f4364d4666a09f2fed583992 \\
Pure Prop Address: & TMJm8VUj9hoafxu2Z8k99ys52dNjtstV9hY \\
Theory Prop Id: & c688e8369c999b2423047a981d3b5c198fb153c1d0f7e6dbee92f27ff38da254 \\
Theory Prop Address: & TMbVkHwsuxJFdmgosfxN8dJkV4edBZBQ8Xf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfgpfchjgoggh} ${\unicdcdadad a \in {G} .  {{{a}*{\postnc{{a}}}}={e}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5faedae00b2ff3112d18fc67a44cc32e8836e3aefdb6f82dd4e11df8648381dc \\
Pure Prop Address: & TMNsYoMt2v2YNvxeJ1MzMMweHHpoJi62UCS \\
Theory Prop Id: & 6522bcdcc934d3748a0dfcbd204413a2501816629e1eddf53c5b4d871f78ca57 \\
Theory Prop Address: & TMc4sqjSkyuS9R2hVFzNDY16nePbzE5g4h8
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfgpfmgjgoggh} ${\unicdcdadad a \in {G} .  {{{\postnc{{a}}}*{a}}={e}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 434e096992c877eb38298cea7cc6fcf3ec01d9afbbcbd3b0783a632c67f5deff \\
Pure Prop Address: & TMTD5RfGMs4wShS2nexxcTshjmbsydNaghn \\
Theory Prop Id: & 6b2fca7f46e1532922eaca0735e71402b9a2629f54eb3f3571f4ca378487902d \\
Theory Prop Address: & TMExrQ2X7HUbLBQZmQuMUtKf8RDh4mQWHWu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfmgdgbgogdgfgmg} ${\unicdcdadad a b c \in {G} .  {{{{a}*{b}}={{a}*{c}}}\unicdbdjdcd{{b}={c}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 33b1b149cdeee23d3bb33fc0a6188a68ffa7bd8e41332d8be527ae438267f3d4 \\
Pure Prop Address: & TMX6h7qhm3NenK6T4aPYQn1M9426HgYTMLw \\
Theory Prop Id: & 826b2e6618fa8fe5b8cff0da58e5a8f4627dcb7b4323cd9e55e91ce57f05280e \\
Theory Prop Address: & TMSLWhCZYGhVwR8odE7nnVNZCRLJR4iruFv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfchdgbgogdgfgmg} ${\unicdcdadad a b c \in {G} .  {{{{a}*{c}}={{b}*{c}}}\unicdbdjdcd{{a}={b}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ef05cefa790fecef7769c37f99ae58c2563aaa45db53a8bee86258c6b886132a \\
Pure Prop Address: & TMWrcUsJHruC5nYp5yAKHRzmwgkFPmSofTL \\
Theory Prop Id: & 953b77b05a77af06ccb9cc940e52712be361bd38ef21fd159599be906700fe65 \\
Theory Prop Address: & TMGiX5S1yoJfx8UWN5xD5FJqKeuhVYzgttD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfchjgogghpfchfggh} ${\unicdcdadad a b \in {G} .  {{{{a}*{b}}={e}}\unicdbdjdcd{{b}={\postnc{{a}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 891f7754b53564fca6f0343cad2dc494efc6e05e34c918bed88fcbddc533265f \\
Pure Prop Address: & TMGNPsYapqknYHxQsZ2F5XoqR6d9prQyeeR \\
Theory Prop Id: & a04aee87622e0b7dc5811e087ae8a1b75632125b99c1aa5cb6c6c3c9beceb1fc \\
Theory Prop Address: & TMSE4wKdLGWD9NZm2jRusJ5H4TwxUYDkdzK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghpfdgpgng} ${\unicdcdadad a b \in {G} .  {{{{a}*{b}}={e}}\unicdbdjdcd{{{b}*{a}}={e}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 663c8f6ce8987057ef1a016fc2d2eb826895e0f18480b99833b0f0990206672c \\
Pure Prop Address: & TMaSbuU5FwcNTsVwQ6PtZ6jLP8LYTgUxsUb \\
Theory Prop Id: & f1098fa01f9673e741bc27d240745fb3bfa00795281c4048f9003c7cc6b2f23d \\
Theory Prop Address: & TMYsR6YLMhEDxsZDgKWug5MYnBqnSoiNUZg
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghpfchfgghcd} ${\unicdcdadad a b \in {G} .  {{{{({{a}*{b}})}*{({{a}*{b}})}}={e}}\unicdbdjdcd{{{({{b}*{a}})}*{({{b}*{a}})}}={e}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 68dbad203c9e4e0b7716e921ed000127a9cf37e288fd5c525a1cdd3a75b5471f \\
Pure Prop Address: & TML3EFwc6aWd8wgzpvyuEJ5Ygy5et6QXvtZ \\
Theory Prop Id: & c5aeaedf7b6e943800ba4479c3f4fbb8514a2e20caea2699de720d8d40aec27b \\
Theory Prop Address: & TMRZWZ4JLKtefjP9iqT3BqVemyLiAo6X7VF
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfbgcgfgmgjgbgog}
We define $\mname{explicit\_abelian}$ to be ${\unicdcdadad a b \in {G} .  {{{a}*{b}}={{b}*{a}}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 05d54a9f11f12daa0639e1df1157577f57d8b0c6ede098282f5eca14026a360f \\
Pure Object Address: & TMSbRNehAadQ85Kiirs6CeWkovxtJVvZdLQ \\
Theory Object Id: & afb9d62b583f9c34b2932e79c800886506cf83a6d1957f0f38ea4b6120525bf5 \\
Theory Object Address: & TMWoaUJJFHkS4LvMBAUyKZxmsGTDk35A5mR
\end{tabular}
\end{center}

\end{definition}
\subsection{Group1Explicit2}\label{hechpgfhahbdfeihahmgjgdgjgehcd}Let $ op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
\subsubsection{Group1Explicit2RepIndep}\label{hechpgfhahbdfeihahmgjgdgjgehcdcffgahjeogegfgah}Let $ op' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${op'}$.
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {G} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp:iepgahpgahhc}
\end{equation}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfchfgahjgogegfgahpfjgngah} ${{{\mname{explicit\_Group}}~{op}}\unicdbdjdcd{{\mname{explicit\_Group}}~{op'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f5012ed8643556d71d97efacc96365a3e64c4075b67a87d5e41d6946ea117e15 \\
Pure Prop Address: & TMK2g6qJebDnBquMej7EVWnZiqivTV1697r \\
Theory Prop Id: & 9d8852ec071692482dd632725271f66464e62a8187bc25f252ba7aa90d3a2c38 \\
Theory Prop Address: & TMUCkaJVFQzcD3xM53V7UGDtKmLnoAfRCF8
\end{tabular}
\end{center}

\end{theorem}
Let $e$ be ${{\mname{explicit\_Group\_identity}}~{op}}$.
Let $e'$ be ${{\mname{explicit\_Group\_identity}}~{op'}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgegfgogehjgehjhpfchfgahjgogegfgah} ${{{\mname{explicit\_Group}}~{op}}\unicdbdjdcd{{e}={e'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 598ff1a23c1fe4126915975f010569b525215d6ff2b98a5ab546dd324cbccaf2 \\
Pure Prop Address: & TMcA9q6i8Vw98yFDFEvLQqJQQv6mxymW78w \\
Theory Prop Id: & bf4147f42cb6909b3123e55bbdd9abcd5e4500bf4c228aba6d90e85f3863fc07 \\
Theory Prop Address: & TMGGsZcTZdyUMrW4cjQ2TioN1uRYTKdww5G
\end{tabular}
\end{center}

\end{theorem}
Let $inv$ be ${{\mname{explicit\_Group\_inverse}}~{op}}$.
Let $inv'$ be ${{\mname{explicit\_Group\_inverse}}~{op'}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfjgogghfgchdhfgpfchfgahjgogegfgah} ${{{\mname{explicit\_Group}}~{op}}\unicdbdjdcd{\unicdcdadad a \in {G} .  {{{\mname{inv}}~{a}}={{inv'}~{a}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1b3e083dd9cf397ee3bc561cfa6db02990a3cf16bf8021b5b480a16f23aeb4b6 \\
Pure Prop Address: & TMGDnT1Aqj6HwvAs6czLDGM8YE7vWNHc8xc \\
Theory Prop Id: & bce8beb409ddbfeedc408e86bebac1a0f9ce7b545243ee799f091e40547b0865 \\
Theory Prop Address: & TMcrPmRNvDAbfSmF1GFzJbteMNNZLQJGYpX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfbgcgfgmgjgbgogpfchfgahjgogegfgahpfjgngah} ${{{\mname{explicit\_abelian}}~{op}}\unicdbdjdcd{{\mname{explicit\_abelian}}~{op'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ef5af4d7ebcdc54f16dcbd6735446df711e99129ddf89eacd2c278c216ee4783 \\
Pure Prop Address: & TMPnVDeP4gfRfuDBEtT7nJNFcLgKCXaRHWg \\
Theory Prop Id: & 6dc553047a706e22ba94296abf5b0db1652898d70d735cf338004f26e3e4c8b4 \\
Theory Prop Address: & TMQeZC612yR6Xczxn9AVL8mF3Ukm9V2F2bL
\end{tabular}
\end{center}

\end{theorem}
\subsection{Group1Explicit3RepIndep}\label{hechpgfhahbdfeihahmgjgdgjgehddcffgahjeogegfgah}Let $ op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
Let $ op' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${op'}$.
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {G} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp:iepgahpgahhc}
\end{equation}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfchfgahjgogegfgah} ${{{\mname{explicit\_Group}}~{op}}\unicdbdjded{{\mname{explicit\_Group}}~{op'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4c880a72b808ad924e81f56a1ed90dd384b42d8c05b5a34106946de015681f8b \\
Pure Prop Address: & TMYoUUzVknsDHuBdb4CTMFGTQJ8RavVXrEb \\
Theory Prop Id: & f0f9a2f129898373c5727edb2324561e41b4d2ee82534892365f8605e104fa10 \\
Theory Prop Address: & TMdA43jg23cA8VmWUWe6knaNXVhz835Psjq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfbgcgfgmgjgbgogpfchfgahjgogegfgah} ${{{\mname{explicit\_abelian}}~{op}}\unicdbdjded{{\mname{explicit\_abelian}}~{op'}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4bf05bb4c1ce5486164c944aa718fe7c76541eaa979f90733925e0df5da80b31 \\
Pure Prop Address: & TMK9RV3nDAmdTWLAZyJDHS6BozLokJ5gF8H \\
Theory Prop Id: & 9c96138929f1974912de1c755238da49ddca4b64627b220e7717c3142c9bffbb \\
Theory Prop Address: & TMJUpZdPq3Ps6CrXDg4pSuMXobz6F6aTgdA
\end{tabular}
\end{center}

\end{theorem}
\section{Groups Encoded as a Set} % Group1
\begin{definition}\label{def:hechpgfhah}
We define $\mname{Group}$ to be ${\uniddcgcg G .  {{{\mname{struct\_b}}~{G}}\unicdcdcdhd{{{\mname{unpack\_b\_o}}~{G}}~{\mname{explicit\_Group}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3bcfdf72871668bce2faf4af19b82f05b1ff30e94a64bbc83215c8462bc294ca \\
Pure Object Address: & TMPgSXfSPyvihsFWLDa9H7w9DDaHAAqfKWh \\
Theory Object Id: & 48ad758ca1725528973592bef2eca92dd3b4cc57fcc1cec0478a8f8e97376e86 \\
Theory Object Address: & TMVKTH5owDCXYfd1wFd2cm4yxGHnuLN5CXz
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:bgcgfgmgjgbgogpfhechpgfhah}
We define $\mname{abelian\_Group}$ to be ${\uniddcgcg G .  {{{\mname{Group}}~{G}}\unicdcdcdhd{{{\mname{unpack\_b\_o}}~{G}}~{\mname{explicit\_abelian}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & c9c27ca28ffd069e766ce309b49a17df75d70111ce5b2b8e9d836356fb30b20a \\
Pure Object Address: & TMZYJxov52ZDnfLrrgP436fnEtrVohjgYF3 \\
Theory Object Id: & 82b65a8b4d905ce66d83d96cd51c72493e71be4e889671636b43a03ef4993b11 \\
Theory Object Address: & TMKxwHVb8mydLee3wEkwZAbNhhw23ui2AP7
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:hechpgfhahpffhogahbgdglgpffgbh} ${\unicdcdadad G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{{\mname{unpack\_b\_o}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}~{\mname{explicit\_Group}}}={{{\mname{explicit\_Group}}~{G}}~{op}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aceab134c9adba80930143837f535ea11b55ad2ca8eaf42a51a35901b0783c35 \\
Pure Prop Address: & TMd7GQcSo21uLBQ7A49xYT78iKSY3PhWQFB \\
Theory Prop Id: & f34cbdd88f4d553a25bb8ac2222863ca028a51086ae3e0f2d11a1fe78e716303 \\
Theory Prop Address: & TMZ6K2cAEkL2uXg3fBxTcxoJSRUaJHicJmH
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:hechpgfhahje} ${\unicdcdadad G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{{\mname{explicit\_Group}}~{G}}~{op}}\unicdbdjdcd{{\mname{Group}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f59584e74c871bfb0a1036e424d097143949b1923d9616b3320eb90f399a91ed \\
Pure Prop Address: & TMQUiQQxmEfgMnDao2t2u2KdoezR3zraGZY \\
Theory Prop Id: & 7a80f33492e5b3d03f1841fd7ccbd5fb77c2faa6b30b5c242db4c0059fc6cdb9 \\
Theory Prop Address: & TMTYbJ6XVymYaZkodwF8XHTGRBpsABB8dxk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:hechpgfhahfe} ${\unicdcdadad G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{\mname{Group}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}\unicdbdjdcd{{{\mname{explicit\_Group}}~{G}}~{op}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f3f463245e1c5c9686fda5a34894e9f282a8f86a019ada8b14ef0e11b0976d07 \\
Pure Prop Address: & TMHNfqMd8twRy3pLuxLepizuzSei8dgrR2i \\
Theory Prop Id: & 2239355bbc80224799ae9be8d5818f67132ab3353e50b12be897026966f41a8f \\
Theory Prop Address: & TMUKjYUwFEKr2Brho6Mkc5ukMBKuMH2PP4M
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgcgfgmgjgbgogpfhechpgfhahpffhogahbgdglgpffgbh} ${\unicdcdadad G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{{\mname{unpack\_b\_o}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}~{\mname{explicit\_abelian}}}={{{\mname{explicit\_abelian}}~{G}}~{op}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2346855e53255b79e76009eda280acf374dad7dcc5e72ab74d2f42201d79140a \\
Pure Prop Address: & TMMHnLwWhH3nJZkk281hptKVfm4dKceyAwW \\
Theory Prop Id: & 6dfe13367c39b0c86ac8656ad108a540b7a3f5c3364369c3dea90e33b297a4a2 \\
Theory Prop Address: & TMWfTBZCZjhKbb8QKapfLpSa2pyTTfAE71m
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgcgfgmgjgbgogpfhechpgfhahpffe} ${\unicdcdadad G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{\mname{abelian\_Group}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}\unicdbdjdcd{{{\mname{Group}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}\unicdcdcdhd{{{\mname{explicit\_abelian}}~{G}}~{op}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0ddfdd60c899db663169e18602174fc26a195f4e543a49ea6ff9d85c51d1db1d \\
Pure Prop Address: & TMFf47YDuvj4E1VPha1jb6n3UhV7xC9VtyU \\
Theory Prop Id: & 6ec272a62e16860ef6fdf6e1827bf60d5f1da411baf1baa0a7b2319ae3c3300a \\
Theory Prop Address: & TMQz71B8ZwyWMJ8Y7PhfRsqJmZ5rqBNeqbW
\end{tabular}
\end{center}

\end{theorem}
\section{Group2}\label{hechpgfhahcd}Let $ G : {\iota}$ be given.
Let $ op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
{\bf{Notation.}} We use $\postnc{-}$ as a postfix operator  corresponding to applying term ${{{\mname{explicit\_Group\_inverse}}~{G}}~{op}}$.
Let $ H : {\iota}$ be given.
\begin{definition}\label{def:fgihahmgjgdgjgehpfdhfhcghgchpgfhah}
We define $\mname{explicit\_subgroup}$ to be ${{{\mname{Group}}~{({{{\mname{pack\_b}}~{H}}~{op}})}}\unicdcdcdhd{{H} \subseteq {G}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4f273e5c6c57dff24b2d1ca4088c333f4bbd2647ab77e6a03beedd08f8f17eb9 \\
Pure Object Address: & TMNFW3sUiRGF4QZDyZs4U1ZFwLXYNZndEUA \\
Theory Object Id: & a5189d9d38cb9e37388edfc6167f21fbbac2dae96c0d30a42796f7f45363ba49 \\
Theory Object Address: & TMUKd1esxsYP6brvBoQj3SzvUxCbvF2x7bC
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgihahmgjgdgjgehpfogpgchngbgmg}
We define $\mname{explicit\_normal}$ to be ${\unicdcdadad x \in {G} .  {{\{{{x}*{{a}*{\postnc{{x}}}}}|a \in {H}\}} \subseteq {H}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1cb8f85f222724bb5ee5926c5c1c0da8acd0066ba3fa91c035fe2fb8d511a035 \\
Pure Object Address: & TMUp97JhNka3EMtq317xqSLU7QwwU9Rv3di \\
Theory Object Id: & d7a9568bb9deb69b03d47d288813c29f08fcc8800ee11aed9df4f6a44df35147 \\
Theory Object Address: & TMdaRbf7U1umHdo2j1hDVsveTbdoBQj6QLo
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{{\mname{Group}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}\label{hyp:iehe}
\end{equation}
Let $e$ be ${{{\mname{explicit\_Group\_identity}}~{G}}~{op}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdhfhcghgchpgfhahpfehfgdheh} ${{{H} \subseteq {G}}\unicdbdjdcd{{{e} \in {H}}\unicdbdjdcd{{({\unicdcdadad a \in {H} .  {{\postnc{{a}}} \in {H}}})}\unicdbdjdcd{{({\unicdcdadad a b \in {H} .  {{{a}*{b}} \in {H}}})}\unicdbdjdcd{\mname{explicit\_subgroup}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a0764d61788853004917f998bf172f98ea252833c7ffffbd4cc8f9fc6d366640 \\
Pure Prop Address: & TMF72nFcvhbTi7RSPrKiVdQH7Zno6gqKNzX \\
Theory Prop Id: & febaefb669b389c2e7af77327b7c126d3c2296175d831b5152819092c60df749 \\
Theory Prop Address: & TMSe5XgyjkAZsLZRAWWesUNSkSR5BgeN71j
\end{tabular}
\end{center}

\end{theorem}
Assume the following.
\begin{equation}
{\mname{explicit\_subgroup}}\label{hyp:iedfhe}
\end{equation}
Let $e'$ be ${{{\mname{explicit\_Group\_identity}}~{H}}~{op}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdhfhcghgchpgfhahpfjgegfgogehjgehjhpffgbh} ${{e}={e'}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d608de6b443a17bb92b076f03900648de80c1688b0a9b18c0f6f2a87d48e9494 \\
Pure Prop Address: & TMMi9FM87WTYChZcDCYSiR1mUgcxriaPpTH \\
Theory Prop Id: & 29bcb214853a5b2b4c2ba9cd9171fe4cd7583e3c7526e1f14f5c9d35785657f7 \\
Theory Prop Address: & TMMErcjnubQrVeuBCzarecXxmRfNpUwDVWL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdhfhcghgchpgfhahpfjgogghpffgbh} ${\unicdcdadad a \in {H} .  {{{{{\mname{explicit\_Group\_inverse}}~{G}}~{op}}~{a}}={{{{\mname{explicit\_Group\_inverse}}~{H}}~{op}}~{a}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 23d0fd40782cc5d113a6f8abbffe684eabb63f361450d6781bee3a513762cc1c \\
Pure Prop Address: & TMSzo58obcQmEn5FMDAcyyCsxm1mW4emXNT \\
Theory Prop Id: & c0bd13173f3bd1ccdf37652d679abb58404d427bcf1cb4bb3209c92633bb1cb0 \\
Theory Prop Address: & TMMes5AgQed1v3SDwaTYoyxExk9LqUvpPHw
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfbgcgfgmgjgbgogpfogpgchngbgmg} ${{{{\mname{explicit\_abelian}}~{G}}~{op}}\unicdbdjdcd{\mname{explicit\_normal}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 07d5b2fc245834d75ec2a313ddb687a0a4ac1c4858adfb47fb56a2b4cdadfcbb \\
Pure Prop Address: & TMWykJghtnE3YAmhYszqL4L2WUWyWs8bESa \\
Theory Prop Id: & 142e7aa60e5da0bf6b3fb1a0a03445c8098ce5c7613ce5f3f698f2493d8311bb \\
Theory Prop Address: & TMPfm754BwmkjxHRPzWnL1tdpxUusE7tyXy
\end{tabular}
\end{center}

\end{theorem}
\section{Group3}\label{hechpgfhahdd}Let $ H G : {\iota}$ be given.
Let $ op op' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
{\bf{Notation.}} We use $\postnc{-}$ as a postfix operator  corresponding to applying term ${{{\mname{explicit\_Group\_inverse}}~{G}}~{op}}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${op'}$.
{\bf{Notation.}} We use $\postkdnckd{-}$ as a postfix operator  corresponding to applying term ${{{\mname{explicit\_Group\_inverse}}~{G}}~{op'}}$.
Assume the following.
\begin{equation}
{{{\mname{explicit\_Group}}~{G}}~{op}}\label{hyp:iehe}
\end{equation}
Assume the following.
\begin{equation}
{{H} \subseteq {G}}\label{hyp:ieiehe}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad a b \in {G} .  {{{a}*{b}}={{a}\unicdbgcdgg{b}}}}\label{hyp:iepgahpgahhc}
\end{equation}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfogpgchngbgmgpfchfgahjgogegfgahpfjgngah} ${{{{{\mname{explicit\_normal}}~{G}}~{op}}~{H}}\unicdbdjdcd{{{{\mname{explicit\_normal}}~{G}}~{op'}}~{H}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3085191447907ed870314c89a8d28cb2745242ad5fc8d8fac5e605f123406e41 \\
Pure Prop Address: & TMF9MV6sqG4RPotXsm4dDP2WeBrREMZMpDz \\
Theory Prop Id: & 9e1540196415c21f2eff94a4d69154a46a0a7f369764af1fe8c67431af6bab59 \\
Theory Prop Address: & TMFwHf4QsoVfQnoVRPxuR1DDrZAUtc9aPLc
\end{tabular}
\end{center}

\end{theorem}
\section{Subgroup as a Relation on Encoded Groups} % Group3
\begin{definition}\label{def:dhfhcghgchpgfhah}
We define $\mname{subgroup}$ to be ${\uniddcgcg H G .  {{{{\mname{struct\_b}}~{G}}\unicdcdcdhd{{\mname{struct\_b}}~{H}}}\unicdcdcdhd{{{\mname{unpack\_b\_o}}~{G}}~{({\uniddcgcg G' op .  {{{\mname{unpack\_b\_o}}~{H}}~{({\uniddcgcg H' \_ .  {{{{H}={{{\mname{pack\_b}}~{H'}}~{op}}}\unicdcdcdhd{{\mname{Group}}~{({{{\mname{pack\_b}}~{H'}}~{op}})}}}\unicdcdcdhd{{H'} \subseteq {G'}}}})}}})}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 994c6976ade70b6acb23366d7ac2e5d6cf47e35ce09a6d71154e38fd46406ad1 \\
Pure Object Address: & TMLRkyR7sy5G519JM6FKX7WCKVJc2Xnbd7n \\
Theory Object Id: & cb09cb23c96a2afb0a031b5795b5906505c2d764fd807be41d9c9ed8115f7b0e \\
Theory Object Address: & TMGMFfq46mwEhdYGyNc2EdYoj7nzTA8Jomq
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${\mname{subgroup}}$.
\begin{definition}\label{def:dhfhcghgchpgfhahpfjgogegfgih}
We define $\mname{subgroup\_index}$ to be ${\uniddcgcg H G .  {{{\mname{unpack\_b\_i}}~{G}}~{({\uniddcgcg G' op .  {\{n \in {\mname{omega}}|{\unicdcdaddd f \in {{G'}^{{{\mname{ordsucc}}~{n}}}} .  {\unicdcdadad i j \in {{\mname{ordsucc}}~{n}} .  {{{i}\unicdcdgdad{j}}\unicdbdjdcd{\unicdcdadad a b \in {{H}~{0}} .  {{{{op}~{({{f}~{i}})}}~{a}}\unicdcdgdad{{{op}~{({{f}~{j}})}}~{b}}}}}}}\}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1dd206bf7d1aea060662f06e19ec29564e628c990cb17f043a496e180cf094e8 \\
Pure Object Address: & TMPcqQwKgtAXH5j1TdcLe1pH8wNiDMvYyEf \\
Theory Object Id: & 7ebea62699ca1f7386cd7aa4aca981fd2c9635dc208c7d879649411943005d9d \\
Theory Object Address: & TMHQwMsB4gE9yRryzdXDQJVWgJ17RM6aMp4
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ogpgchngbgmgpfdhfhcghgchpgfhah}
We define $\mname{normal\_subgroup}$ to be ${\uniddcgcg H G .  {{{H}\unicdcdgded{G}}\unicdcdcdhd{{{\mname{unpack\_b\_o}}~{G}}~{({\uniddcgcg G' op .  {{{\mname{unpack\_b\_o}}~{H}}~{({\uniddcgcg H' \_ .  {{{{\mname{explicit\_normal}}~{G'}}~{op}}~{H'}}})}}})}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 071c71e291b8c50d10f9d7f5544da801035d99ff3a68c9e5386b4087d22b5db2 \\
Pure Object Address: & TMd7xWz8FWuB8j5DzNNXPoPYjwwcw9iGFfh \\
Theory Object Id: & e2b2818e909567261bb44f9241b012f127d9ff02c3dd0d03ad5c7d708a41ee32 \\
Theory Object Address: & TMUQxZTG9uZr52Krep3t5yfZUjXQwpCSMDD
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:ahbgdglgpfcgpfdhfhcghgchpgfhahpffe} ${\unicdcdadad H G : {\iota} .  {\unicdcdadad opH op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{{{\mname{pack\_b}}~{H}}~{opH}}\unicdcdgded{{{\mname{pack\_b}}~{G}}~{op}}}\unicdbdjdcd{{{{{\mname{pack\_b}}~{H}}~{opH}}={{{\mname{pack\_b}}~{H}}~{op}}}\unicdcdcdhd{{{{\mname{explicit\_subgroup}}~{G}}~{op}}~{H}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7125ffccb47b1cd6d83c70896cd0d77ebc0a5c375a659546c75d43ff0d142474 \\
Pure Prop Address: & TMUbUKT8Uymhwq1sqJm6JGztSHZZZywozop \\
Theory Prop Id: & 071cdd18db9355616c94b43f39efdd84fb6821f364314b2cb4f40e9bd1675033 \\
Theory Prop Address: & TMaQ7YHCEZFXsZgr3AL8pKTCzucZbFxr6jW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcghgchpgfhahpffe} ${\unicdcdadad H G .  {{{H}\unicdcdgded{G}}\unicdbdjdcd{\unicdcdadad q : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{({\unicdcdadad H G .  {\unicdcdadad op : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{({\unicdcdadad a b \in {G} .  {{{{op}~{a}}~{b}} \in {G}}})}\unicdbdjdcd{{{\mname{Group}}~{({{{\mname{pack\_b}}~{H}}~{op}})}}\unicdbdjdcd{{{H} \subseteq {G}}\unicdbdjdcd{{{q}~{({{{\mname{pack\_b}}~{H}}~{op}})}}~{({{{\mname{pack\_b}}~{G}}~{op}})}}}}}}})}\unicdbdjdcd{{{q}~{H}}~{G}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8d2e3a1f4dd63f83ee62c1339fd126e053185c4e48fc3cc95c24bf2ccac05098 \\
Pure Prop Address: & TMYiapjALEQg8YorewqjMBBDNZSfdKWuMUd \\
Theory Prop Id: & 664898a15a2a44476b34fcd20187cb6b36a7be22f8e5a6208da45360a43d39bf \\
Theory Prop Address: & TMR3yhY1JLi3dUUZzQR9GUXSZroHRWT43WE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgcgfgmgjgbgogpfhgchpgfhahpfogpgchngbgmgpfdhfhcghgchpgfhah} ${\unicdcdadad G .  {{{\mname{abelian\_Group}}~{G}}\unicdbdjdcd{\unicdcdadad H .  {{{H}\unicdcdgded{G}}\unicdbdjdcd{{{\mname{normal\_subgroup}}~{H}}~{G}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4382dad503528fbf8173cf9e47b154aca06b57bf02b22eb6830a50e23b94f865 \\
Pure Prop Address: & TMTKNLNxcPh9EVds4cHdQmAhf5w3KjMpXZk \\
Theory Prop Id: & 31f5b8608189f9d346c09a8ca7beb6a0955a20f1ee768bbad1c3a8d8c9eff610 \\
Theory Prop Address: & TMRsrDZNbLqAcJgVD7iy9CvAaGQiKeavic1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcghgchpgfhahpfehchbgogdhjgehjgghfg} ${\unicdcdadad K H G .  {{{K}\unicdcdgded{H}}\unicdbdjdcd{{{H}\unicdcdgded{G}}\unicdbdjdcd{{K}\unicdcdgded{G}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c84fb0f00761163c826038c45b5a080d551a4af82e13ecdbec4190f7d264c8c6 \\
Pure Prop Address: & TMRVsYwzXoyQoBSWcrLFgzK5m4LjCaiomjX \\
Theory Prop Id: & 026e9055ebb50e4182d43a6f9cdfa349ac1e29a7844be46cdc9b70e9aa507fce \\
Theory Prop Address: & TMQpoQCnMNzGQ5c655fPoRUpabq3NF9LuZs
\end{tabular}
\end{center}

\end{theorem}
\section{Group4}\label{hechpgfhahed}Let $ A : {\iota}$ be given.
Let $G$ be ${\{f \in {{A}^{{A}}}|{{{{\mname{bij}}~{A}}~{A}}~{({\uniddcgcg x .  {{f}~{x}}})}}\}}$.
Let $op$ be ${\uniddcgcg f g : {\iota} .  {\uniddcgcg x \in {A} .  {{g}~{({{f}~{x}})}}}}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${op}$.
Let $id$ be ${\uniddcgcg x \in {A} .  {x}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfdhjhnghgchpgfhah} ${{{\mname{explicit\_Group}}~{G}}~{op}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 75533e8a735e606e28b8daa28ccee75f6b02e88687f5737d356a9e287a3636e0 \\
Pure Prop Address: & TMKpf7yzXWNWoB7pTFZ9CSXQc1WgFWKDum8 \\
Theory Prop Id: & 2004dca00796c3260ddfc226ff73cd52a9ab5d9464afb109a5e9626139500ed8 \\
Theory Prop Address: & TMUjucvp4GP3FkV7CeMpFR5TdJdrvtmChGd
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfdhjhnghgchpgfhahpfjgegpffgbh} ${{{{\mname{explicit\_Group\_identity}}~{G}}~{op}}={id}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 21cf5cbe5a190e3996df417982f48894c7fcd25e942984729664b5b8bc6e0914 \\
Pure Prop Address: & TMZFox5vkuvToBeKHtjvAXUWRxd5zPHKZEF \\
Theory Prop Id: & fce19ddc04b4e28eca8656cf372366102a641140d6d39cdbbd0e47fd939dd647 \\
Theory Prop Address: & TMXkzvHQA9cxQakivoT7RYrtHpaUzWEVmaX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfhechpgfhahpfdhjhnghgchpgfhahpfjgogghpffgbh} ${\unicdcdadad f \in {G} .  {{{{{\mname{explicit\_Group\_inverse}}~{G}}~{op}}~{f}}={({\uniddcgcg x \in {A} .  {{{{\mname{inv}}~{A}}~{({\uniddcgcg x .  {{f}~{x}}})}}~{x}}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 569ca8a98ff593e668e81c3c75a51082eb69d41932f6f1b3eb2d602a460fcb77 \\
Pure Prop Address: & TMSEXyQTYWdXvSSZeGpr2AiQNQYfM8psrG6 \\
Theory Prop Id: & 9b2215cf55968e6869adb6aba2a45d58065e1806de069a6c1f8eba372d33e15e \\
Theory Prop Address: & TMKp3LXskT1sHdd7hevEZu5XUkBG1q5YCR9
\end{tabular}
\end{center}

\end{theorem}
Let $ B : {\iota}$ be given.
Let $H$ be ${\{f \in {{A}^{{A}}}|{{{{{\mname{bij}}~{A}}~{A}}~{({\uniddcgcg x .  {{f}~{x}}})}}\unicdcdcdhd{\unicdcdadad x \in {B} .  {{{f}~{x}}={x}}}}\}}$.
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfdhfhcghgchpgfhahpfdhjhnghgchpgfhahpfggjgihjgoghg} ${{{B} \subseteq {A}}\unicdbdjdcd{{{{\mname{explicit\_subgroup}}~{G}}~{op}}~{H}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bbacee9bc55d4bb9d8a095e058cf6c04648223d4da35a401d88ff34482c4bfa6 \\
Pure Prop Address: & TMWhKgrPUBPXmguhqdDXCXSxNBeVZqTWqt7 \\
Theory Prop Id: & 9bbf1dff7d86d24b11b8fc750a9c1358c88d26f302226f1a0f7af5c4b779e747 \\
Theory Prop Address: & TMQPazgEs2ZAxG7K58ru8aJWKhEasAJanUc
\end{tabular}
\end{center}

\end{theorem}
\section{Groups of Permutations} % Group4
\begin{definition}\label{def:dhjhnghgchpgfhah}
We define $\mname{symgroup}$ to be ${\uniddcgcg A .  {{{\mname{pack\_b}}~{\{f \in {{A}^{{A}}}|{{{{\mname{bij}}~{A}}~{A}}~{({\uniddcgcg x .  {{f}~{x}}})}}\}}}~{({\uniddcgcg f g .  {\uniddcgcg x \in {A} .  {{g}~{({{f}~{x}})}}}})}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b5e0e5eb78d27c7fd8102e3c6741350d4444905a165833aa81250cef01a1acea \\
Pure Object Address: & TMZELiVF4MBqaUvQtfAy3PdnvoJi11ixgrf \\
Theory Object Id: & 5a86a668a5aa4ec3f8070179712ef77612eb82d194a9d09eba866f04a67f1bb9 \\
Theory Object Address: & TMLr56c3xH1KtYDpD7smvX5TNYc9XxLWkp7
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhjhnghgchpgfhahpfggjgihjgoghg}
We define $\mname{symgroup\_fixing}$ to be ${\uniddcgcg A B .  {{{\mname{pack\_b}}~{\{f \in {{A}^{{A}}}|{{{{{\mname{bij}}~{A}}~{A}}~{({\uniddcgcg x .  {{f}~{x}}})}}\unicdcdcdhd{\unicdcdadad x \in {B} .  {{{f}~{x}}={x}}}}\}}}~{({\uniddcgcg f g .  {\uniddcgcg x \in {A} .  {{g}~{({{f}~{x}})}}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 683becb457be56391cd0ea1cefb5016e2185efebd92b7afd41cd7b3a4769ac57 \\
Pure Object Address: & TMVDj8UpCzz8NDMvJKFnUV46Ac7avCYjHaA \\
Theory Object Id: & 3ec65f6d528b1474770fc9b11779c3256c697e2ffcb88e012e04a72be7cb29e1 \\
Theory Object Address: & TMFNyn7aj1wSxx41MtoZKZ7b1VE1wtZVNQz
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:hechpgfhahpfdhjhnghgchpgfhah} ${\unicdcdadad A .  {{\mname{Group}}~{({{\mname{symgroup}}~{A}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 990875f1186a5c690222b6df93ca46ef542493573c3ec402b83ecaa74a396595 \\
Pure Prop Address: & TMUqQYsqDvdQsVAxhFJHuJf8qqVjQaX4xft \\
Theory Prop Id: & aa2f4e58437f0a2d91605cef8477180bffe4c75c9f5c4c510c1123991d31284d \\
Theory Prop Address: & TMQ1kebtip2R8A29YT8cryCxBqcSdnZRkFP
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:hechpgfhahpfdhjhnghgchpgfhahpfggjgihjgoghg} ${\unicdcdadad A B .  {{{B} \subseteq {A}}\unicdbdjdcd{{\mname{Group}}~{({{{\mname{symgroup\_fixing}}~{A}}~{B}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4c494d5b78b3e2f30e56cfecea27ca083d44f00a781f32acffbe38a3616a3bd0 \\
Pure Prop Address: & TMVs3oeD3WthGX2etWEzZB5jM5vfjmrzdv8 \\
Theory Prop Id: & 79320ab5a30ce81496e65d23083aa7bf3b2669673cf4d3f1da6f4cd56754af32 \\
Theory Prop Address: & TMJxYyCcFvZLw4yZZSr8PNBQfMkiujqpSn7
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcghgchpgfhahpfdhjhnghgchpgfhahpfggjgihjgoghg} ${\unicdcdadad A B .  {{{B} \subseteq {A}}\unicdbdjdcd{{{{\mname{symgroup\_fixing}}~{A}}~{B}}\unicdcdgded{{\mname{symgroup}}~{A}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ea4ea2cb60a4490fa7dd3a8d1121a24afe0c4f02b1e69057fa3ac1cbaa488ce1 \\
Pure Prop Address: & TMUgyamfautEr7neHo5s168PJsHpp3YAAxn \\
Theory Prop Id: & e7086b5067a4adfaef6ac76b57d03ca28dd628c134faaba9dd82bdbe075035ba \\
Theory Prop Address: & TMNMREeoQruvS2q4Z9DbBPztZroZJLfFJtw
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhfhcghgchpgfhahpfdhjhnghgchpgfhahpfggjgihjgoghgcd} ${\unicdcdadad A B C .  {{{C} \subseteq {B}}\unicdbdjdcd{{{B} \subseteq {A}}\unicdbdjdcd{{{{\mname{symgroup\_fixing}}~{A}}~{B}}\unicdcdgded{{{\mname{symgroup\_fixing}}~{A}}~{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5b06faf92f0eabd16f89b9270b775c6a00de6b3dbc7910aba9398f6587c745ba \\
Pure Prop Address: & TMFXcztsEWX26DZ48NuWwuvxCKRxMqxgYEw \\
Theory Prop Id: & 93e5e57f39b365e446a7903858b9899067c88e034d90efdc581b4175c2a760c5 \\
Theory Prop Address: & TMVocWTn2DD7Q6zJVrVcTrKtjJ566LnziCr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogpgogogpgchngbgmgpfdhfhcghgchpgfhah} ${\unicdcdaddd H G .  {{{{\mname{Group}}~{G}}\unicdcdcdhd{{H}\unicdcdgded{G}}}\unicdcdcdhd{\preoh{{{{\mname{normal\_subgroup}}~{H}}~{G}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4af1eff8f561099d5165fbd9166ec526c420d387fa5843d448689ae34c64a1fd \\
Pure Prop Address: & TMaJXbhnzpZH2dG2PZNn1vcD2Zrzy99NNUq \\
Theory Prop Id: & f4475069cf93e4f1ed33d4f2b63efb7114719af9f10d271d932e038b09e2f797 \\
Theory Prop Address: & TMK3fNtE5vExNjZ8gT49kLhgbW7s8Mujkhm
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ogpgchngbgmgpfdhfhcghgchpgfhahpffgbhfhjggh}
We define $\mname{normal\_subgroup\_equiv}$ to be ${\uniddcgcg G N a b .  {{{\mname{unpack\_b\_o}}~{G}}~{({\uniddcgcg G op .  {{{{a} \in {G}}\unicdcdcdhd{{b} \in {G}}}\unicdcdcdhd{{{{op}~{a}}~{({{{{\mname{explicit\_Group\_inverse}}~{G}}~{op}}~{b}})}} \in {{N}~{0}}}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8d6a0ebb123230b9386afac5f3888ea2c3009a7caabad13e57153f9a737c8d0b \\
Pure Object Address: & TMRASNP9xsTmfEHZVz86EScPbtm9LE7RB3s \\
Theory Object Id: & 6de522f05b2ef6abc7f410d16bdebf811c59bb4ef7f25e5a80615298e85ecef2 \\
Theory Object Address: & TMHp4buRe3CwdShZ32fRxcFLnxds4BLiMTy
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:bhfhpgehjgfgogehpfhechpgfhah}
We define $\mname{quotient\_Group}$ to be ${\uniddcgcg G N .  {{{\mname{unpack\_b\_i}}~{G}}~{({\uniddcgcg G' op .  {{{\mname{pack\_b}}~{\{a \in {G'}|{{{\mname{quotient}}~{({{{\mname{normal\_subgroup\_equiv}}~{G}}~{N}})}}~{a}}\}}}~{({\uniddcgcg a b .  {{{\mname{canonical\_elt}}~{({{{\mname{normal\_subgroup\_equiv}}~{G}}~{N}})}}~{({{{op}~{a}}~{b}})}}})}}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 971902aba30554ada3e97388da3b25c677413e2b4df617edba4112889c123612 \\
Pure Object Address: & TMRMVZTtqZEm7ZeJHfgYoXZDgFGDJRPPgV8 \\
Theory Object Id: & ef67eb20b92ec20f2b10d37a0da1f0c16b334205004d4b4bdc4b498bcd06a015 \\
Theory Object Address: & TMJprm3Y7UHzW78sFefvKVSjQLMnLJqyagm
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ehchjgghjgbgmgpfhechpgfhahpfah}
We define $\mname{trivial\_Group\_p}$ to be ${\uniddcgcg G .  {{{\mname{Group}}~{G}}\unicdcdcdhd{\unicdcdadad x y \in {{G}~{0}} .  {{x}={y}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 759fd51778137326dda8cf75ce644e3ec8608dfa7e59c54b364069dd6cf6dd0d \\
Pure Object Address: & TMXgRAihjx6p6LVB2gjGrWcrkQxxPLzMt3u \\
Theory Object Id: & 4a843e3be3a632d671082290bcb4335685122c8f5b5168ab2de4fffb849942c4 \\
Theory Object Address: & TMMyfsrQ9kVyrT23cGp37GGgZap9HT6THXK
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhpgmgghbgcgmgfgpfhechpgfhahpfah}
We define $\mname{solvable\_Group\_p}$ to be ${\uniddcgcg G .  {\unicdcdaddd n \in {\mname{omega}} .  {\unicdcdaddd Gseq .  {{{{{({\unicdcdadad i \in {{\mname{ordsucc}}~{n}} .  {{\mname{Group}}~{({{Gseq}~{i}})}}})}\unicdcdcdhd{({\unicdcdadad i \in {n} .  {{{\mname{normal\_subgroup}}~{({{Gseq}~{({{\mname{ordsucc}}~{i}})}})}}~{({{Gseq}~{i}})}}})}}\unicdcdcdhd{({\unicdcdadad i \in {n} .  {{\mname{abelian\_Group}}~{({{{\mname{quotient\_Group}}~{({{Gseq}~{i}})}}~{({{Gseq}~{({{\mname{ordsucc}}~{i}})}})}})}}})}}\unicdcdcdhd{{G}={{Gseq}~{0}}}}\unicdcdcdhd{{\mname{trivial\_Group\_p}}~{({{Gseq}~{n}})}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 49803500fa75d5030dddbb3d7a18d03eeebfdd720d57630629384cec6d8b3afc \\
Pure Object Address: & TMX5XpRdUwhyCYB1UE83KHG1aehAuoESN6w \\
Theory Object Id: & da0c1bb253cd8664d898fe71430bbdd8202b6943c0866c96597b014889d43008 \\
Theory Object Address: & TMNb2P5ANiNoTvE4HeSJnPNGJDNyZCjuTD5
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:hechpgfhahpfdgbgchchjgfgch}
We define $\mname{Group\_carrier}$ to be ${\uniddcgcg Gs .  {{Gs}~{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:hechpgfhahpfpgah}
We define $\mname{Group\_op}$ to be ${\uniddcgcg Gs .  {{\mname{decode\_b}}~{({{Gs}~{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}
\section{Group2}\label{hechpgfhahcd}Let $ Gs : {\iota}$ be given.
Let $ Gs' : {\iota}$ be given.
Let $G : {\iota}$ be ${{\mname{Group\_carrier}}~{Gs}}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${{\mname{Group\_op}}~{Gs}}$.
Let $G' : {\iota}$ be ${{\mname{Group\_carrier}}~{Gs'}}$.
{\bf{Notation.}} We use $\infkdkckd$ as a right associative infix operator  corresponding to applying term ${{\mname{Group\_op}}~{Gs'}}$.
\begin{definition}\label{def:hechpgfhahpfiepgng}
We define $\mname{Group\_Hom}$ to be ${\uniddcgcg g .  {{{{{\mname{Group}}~{Gs}}\unicdcdcdhd{{\mname{Group}}~{Gs'}}}\unicdcdcdhd{{g} \in {{G'}^{{G}}}}}\unicdcdcdhd{\unicdcdadad a b \in {G} .  {{{g}~{({{a}*{b}})}}={{{g}~{a}}\unicdbgcdgg{{g}~{b}}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 163d1cc9e169332d8257b89d93d961798c6847300b6756e818c4906f0e37c37f \\
Pure Object Address: & TMG33bGq8oXGhbwW9bdnHoQwrAnZGRnqbDo \\
Theory Object Id: & 04a4493700bf4496fc9785ab649cc965ed6f6509b5bedeb92b3cfd0295c6ab1d \\
Theory Object Address: & TMbt3jCCTS2GpiirQWPe7YD1PGZoafrvFeD
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:hechpgfhahpfjedhpg}
We define $\mname{Group\_Iso}$ to be ${\uniddcgcg g .  {{{\mname{Group\_Hom}}~{g}}\unicdcdcdhd{{{{\mname{bij}}~{G}}~{G'}}~{({\uniddcgcg x .  {{g}~{x}}})}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3bc46030cc63aa36608ba06b3b00b696e1a1eb1de5346ff216ca33108220fbda \\
Pure Object Address: & TMNoSwhDXv7bcUbtfNVM1cTexdvsoLbdLJQ \\
Theory Object Id: & 3578401f9ab8d370c4c75e61d9c1049d50026478ddeaef7cb2f37a857cf8c8cd \\
Theory Object Address: & TMLoxwKVttJ32tGGRhbrdMTf4SuCUFyYCkX
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:hechpgfhahpfjedhpgngpgchahigjgdg}
We define $\mname{Group\_Isomorphic}$ to be ${\unicdcdaddd g .  {{\mname{Group\_Iso}}~{g}}}$ of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 727fd1e7d5e38e7145387c0a329b4de2b25f2de5d67989f11e8921bc96f4b6bd \\
Pure Object Address: & TMPtRTKnaVTXR2dtDWrcvKMrZogxkw6v58N \\
Theory Object Id: & 8b3f77534efc12910b019fd5efaa573bd03c8fbe3aaf9677848757f8741adaf1 \\
Theory Object Address: & TMKSQinvAqsVekHU9Jcu1GLLV1RU4ESajgh
\end{tabular}
\end{center}

\end{definition}
