\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
 WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
 LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.

|#

; Requires defn-sk.

#|
The following article is about this event file.

@article{Yu89,
        author="Yuan Yu",
        title="Computer Proofs in Group Theory",
        journal="Journal of Automated Reasoning",
        volume="6",
	number="3",
        year=1990
}
|#



\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf thm} theory.

\addvspace{18pt}

 
\begin{verbatim}; First, several concepts on SET.

; Set L has no duplicate element.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{set-standard} \\  
\=\+{\rm{set-standard}}\,({\it{l\/}})\index{set-standard} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }({\rm{car}}\,({\it{l\/}}) $\not\in$ {\rm{cdr}}\,({\it{l\/}})) $\wedge$ {\rm{set-standard}}\,({\rm{cdr}}\,({\it{l\/}}))\index{set-standard} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; L1-L2.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{set-minus} \\  
\=\+{\rm{set-minus}}\,({\it{l1\/}}, {\it{l2\/}})\index{set-minus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l1\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{l1\/}}) $\in$ {\it{l2\/}}$\;\;${\bf then }{\rm{set-minus}}\,({\rm{cdr}}\,({\it{l1\/}}), {\it{l2\/}})\index{set-minus} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l1\/}}), {\rm{set-minus}}\,({\rm{cdr}}\,({\it{l1\/}}), {\it{l2\/}})\index{set-minus})$\;${\bf  endif}\- \\ 
{\bf else }{\it{l1\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; L1 and L2 are disjoint.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{set-disjoint} \\  
\=\+{\rm{set-disjoint}}\,({\it{l1\/}}, {\it{l2\/}})\index{set-disjoint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l1\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{l1\/}}) $\in$ {\it{l2\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{set-disjoint}}\,({\rm{cdr}}\,({\it{l1\/}}), {\it{l2\/}})\index{set-disjoint}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; remove the element x from L.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{delete} \\  
\=\+{\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{l\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{delete})$\;${\bf  endif}\- \\ 
{\bf else }{\it{l\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; L2 contains L1.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subset} \\  
\=\+{\rm{subset}}\,({\it{l1\/}}, {\it{l2\/}})\index{subset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l1\/}})$\;\;${\bf then }({\rm{car}}\,({\it{l1\/}}) $\in$ {\it{l2\/}}) $\wedge$ {\rm{subset}}\,({\rm{cdr}}\,({\it{l1\/}}), {\it{l2\/}})\index{subset} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; The number of elements in L.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cardinal} \\  
\=\+{\rm{cardinal}}\,({\it{l\/}})\index{cardinal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }$1\;+$ {\rm{cardinal}}\,({\rm{cdr}}\,({\it{l\/}}))\index{cardinal} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Lemmas based on the above concepts.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  set-standard-lemma \\ \index{set-standard-lemma}
{\rm{set-standard}}\,({\it{a\/}})\index{set-standard} $\rightarrow$ {\rm{set-standard}}\,({\rm{set-minus}}\,({\it{a\/}}, {\it{b\/}})\index{set-minus})\index{set-standard}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-minus-lemma1 \\ \index{set-minus-lemma1}
{\rm{count}}\,({\rm{set-minus}}\,({\it{s\/}}, {\it{s1\/}})\index{set-minus}) $\leq$ {\rm{count}}\,({\it{s\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-minus-lemma2 \\ \index{set-minus-lemma2}
({\it{c\/}} $\not\in$ {\it{a\/}}) $\rightarrow$ ({\rm{set-minus}}\,({\it{a\/}}, {\rm{cons}}\,({\it{c\/}}, {\it{b\/}}))\index{set-minus} $=$ {\rm{set-minus}}\,({\it{a\/}}, {\it{b\/}})\index{set-minus})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-minus-lemma3 \\ \index{set-minus-lemma3}
({\it{x\/}} $\in$ {\rm{set-minus}}\,({\it{s\/}}, {\it{s1\/}})\index{set-minus}) $=$ (({\it{x\/}} $\in$ {\it{s\/}}) $\wedge$ ({\it{x\/}} $\not\in$ {\it{s1\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-minus-lemma \\ \index{set-minus-lemma}
\=\+({\rm{listp}}\,({\it{s\/}}) $\wedge$ ({\it{x\/}} $\in$ {\it{s\/}}) $\wedge$ ({\it{x\/}} $\in$ {\it{s1\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count}}\,({\rm{set-minus}}\,({\it{s\/}}, {\it{s1\/}})\index{set-minus}) $<$ {\rm{count}}\,({\it{s\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-lemma1 \\ \index{delete-lemma1}
({\it{x\/}} $\in$ {\it{a\/}}) $\rightarrow$ ({\rm{cardinal}}\,({\it{a\/}})\index{cardinal} $=$ ($1\;+$ {\rm{cardinal}}\,({\rm{delete}}\,({\it{x\/}}, {\it{a\/}})\index{delete})\index{cardinal}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-lemma2 \\ \index{delete-lemma2}
(({\it{y\/}} $\in$ {\it{a\/}}) $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) $\rightarrow$ ({\it{y\/}} $\in$ {\rm{delete}}\,({\it{x\/}}, {\it{a\/}})\index{delete})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-lemma3 \\ \index{delete-lemma3}
(({\it{x\/}} $\in$ {\it{a\/}}) $\wedge$ ({\it{x\/}} $\not\in$ {\it{b\/}}) $\wedge$ {\rm{subset}}\,({\it{b\/}}, {\it{a\/}})\index{subset}) $\rightarrow$ {\rm{subset}}\,({\it{b\/}}, {\rm{delete}}\,({\it{x\/}}, {\it{a\/}})\index{delete})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-transitivity \\ \index{subset-transitivity}
({\rm{subset}}\,({\it{a\/}}, {\it{b\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{b\/}}, {\it{c\/}})\index{subset}) $\rightarrow$ {\rm{subset}}\,({\it{a\/}}, {\it{c\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-lemma0 \\ \index{subset-lemma0}
({\rm{subset}}\,({\it{s1\/}}, {\it{s\/}})\index{subset} $\wedge$ ({\it{x\/}} $\in$ {\it{s1\/}})) $\rightarrow$ ({\it{x\/}} $\in$ {\it{s\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-lemma1 \\ \index{subset-lemma1}
{\rm{subset}}\,({\it{a\/}}, {\it{b\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\it{a\/}}, {\rm{cons}}\,({\it{c\/}}, {\it{b\/}}))\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-lemma2 \\ \index{subset-lemma2}
{\rm{subset}}\,({\it{a\/}}, {\it{b\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\rm{set-minus}}\,({\it{a\/}}, {\it{c\/}})\index{set-minus}, {\it{b\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-reflexivity \\ \index{subset-reflexivity}
{\rm{subset}}\,({\it{a\/}}, {\it{a\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cardinal-lemma \\ \index{cardinal-lemma}
({\it{x\/}} $\in$ {\it{s\/}}) $\rightarrow$ ({\tt{1}} $\leq$ {\rm{cardinal}}\,({\it{s\/}})\index{cardinal})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cardinal-equality \\ \index{cardinal-equality}
\=\+({\rm{set-standard}}\,({\it{a\/}})\index{set-standard} $\wedge$ ({\it{c\/}} $\not\in$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\in$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cardinal}}\,({\rm{set-minus}}\,({\it{a\/}}, {\it{b\/}})\index{set-minus})\index{cardinal} $=$ ($1\;+$ {\rm{cardinal}}\,({\rm{set-minus}}\,({\it{a\/}}, {\rm{cons}}\,({\it{c\/}}, {\it{b\/}}))\index{set-minus})\index{cardinal}))\-
\end{tabbing}

\begin{verbatim}; Induction hint for CARDINAL-INEQUALITY-LEMMA
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cardinal-inequality-induct} \\  
\=\+{\rm{cardinal-inequality-induct}}\,({\it{b\/}}, {\it{a\/}})\index{cardinal-inequality-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{b\/}})$\;\;${\bf then }{\rm{cardinal-inequality-induct}}\,({\rm{cdr}}\,({\it{b\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{b\/}}), {\it{a\/}})\index{delete})\index{cardinal-inequality-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cardinal-inequality \\ \index{cardinal-inequality}
({\rm{set-standard}}\,({\it{b\/}})\index{set-standard} $\wedge$ {\rm{subset}}\,({\it{b\/}}, {\it{a\/}})\index{subset}) $\rightarrow$ ({\rm{cardinal}}\,({\it{b\/}})\index{cardinal} $\leq$ {\rm{cardinal}}\,({\it{a\/}})\index{cardinal})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cardinal-subset \\ \index{cardinal-subset}
\=\+({\rm{set-standard}}\,({\it{a\/}})\index{set-standard} $\wedge$ {\rm{set-standard}}\,({\it{b\/}})\index{set-standard} $\wedge$ {\rm{subset}}\,({\it{b\/}}, {\it{a\/}})\index{subset}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cardinal}}\,({\rm{set-minus}}\,({\it{a\/}}, {\it{b\/}})\index{set-minus})\index{cardinal} $=$ ({\rm{cardinal}}\,({\it{a\/}})\index{cardinal} $-$ {\rm{cardinal}}\,({\it{b\/}})\index{cardinal}))\-
\end{tabbing}

\begin{verbatim}; we will introduce the axioms for definition of group with operation OP.
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it op\index{op}\/} of 2 arguments.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{group-op} \\  
\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+$\forall\;${\it{x\/}}, {\it{y\/}}$\;$((({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}})) $\rightarrow$ ({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op} $\in$ {\it{g\/}}))\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{y\/}}, {\it{z\/}}$\;$(\=\+(({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\it{z\/}})\index{op} $=$ {\rm{op}}\,({\it{x\/}}, {\rm{op}}\,({\it{y\/}}, {\it{z\/}})\index{op})\index{op}))\-\index{forall} \\ 
$\wedge$$\;\;\;\;$$\exists\;${\it{id\/}}$\;$(\=\+({\it{id\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{x\/}}$\;$(\=\+({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{op}}\,({\it{id\/}}, {\it{x\/}})\index{op} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{id\/}})\index{op} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$$\exists\;${\it{inv\/}}$\;$(\=\+({\it{inv\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{op}}\,({\it{inv\/}}, {\it{x\/}})\index{op} \\ 
$=$$\;\;\;\;${\it{id\/}})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{op}}\,({\it{x\/}}, {\it{inv\/}})\index{op} \\ 
$=$$\;\;\;\;${\it{id\/}})\-)\-\index{exists})\-)\-\index{forall})\-\index{exists})\-\-
\end{tabbing}
                                                             
\begin{verbatim}; the group has the "closed" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op-closed \\ \index{group-op-closed}
({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}})) $\rightarrow$ ({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op} $\in$ {\it{g\/}})
\end{tabbing}
                      
\begin{verbatim}; the group has the "associativity" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op-associativity \\ \index{group-op-associativity}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\it{z\/}})\index{op} $=$ {\rm{op}}\,({\it{x\/}}, {\rm{op}}\,({\it{y\/}}, {\it{z\/}})\index{op})\index{op})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  group-op-associativity1 \\ \index{group-op-associativity1}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\rm{op}}\,({\it{y\/}}, {\it{z\/}})\index{op})\index{op} $=$ {\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\it{z\/}})\index{op})\-
\end{tabbing} 

\begin{verbatim}; the group has the "identity" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op-identity \\ \index{group-op-identity}
\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{id}}\,({\it{g\/}})\index{id} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $\in$ {\it{g\/}}) $\rightarrow$ (({\rm{op}}\,({\rm{id}}\,({\it{g\/}})\index{id}, {\it{x\/}})\index{op} $=$ {\it{x\/}}) $\wedge$ ({\rm{op}}\,({\it{x\/}}, {\rm{id}}\,({\it{g\/}})\index{id})\index{op} $=$ {\it{x\/}}))))\-\-
\end{tabbing}

\begin{verbatim}; the group has the "inverse" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op-inverse \\ \index{group-op-inverse}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv}, {\it{x\/}})\index{op} $=$ {\rm{id}}\,({\it{g\/}})\index{id}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\index{op} $=$ {\rm{id}}\,({\it{g\/}})\index{id}))\-\-
\end{tabbing}
                           
\begin{verbatim}; introduce the concept of coset.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{right-coset} \\  
\=\+{\rm{right-coset}}\,({\it{s\/}}, {\it{a\/}})\index{right-coset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{s\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{op}}\,({\rm{car}}\,({\it{s\/}}), {\it{a\/}})\index{op}, {\rm{right-coset}}\,({\rm{cdr}}\,({\it{s\/}}), {\it{a\/}})\index{right-coset}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-coset-cardinal \\ \index{right-coset-cardinal}
{\rm{cardinal}}\,({\rm{right-coset}}\,({\it{s\/}}, {\it{a\/}})\index{right-coset})\index{cardinal} $=$ {\rm{cardinal}}\,({\it{s\/}})\index{cardinal}
\end{tabbing}
                    
\begin{tabbing}{\sc Theorem}:  right-coset-nempty \\ \index{right-coset-nempty}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ ({\rm{id}}\,({\it{g\/}})\index{id} $\in$ {\it{s\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{right-coset}}\,({\it{s\/}}, {\it{x\/}})\index{right-coset})\-
\end{tabbing}

\begin{verbatim}; some simple equalities in group.
; EQUALITY1: x*a=y*b-->x=y*(b*(inv g a)).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op-equality1 \\ \index{op-equality1}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $=$ {\rm{op}}\,({\it{y\/}}, {\it{b\/}})\index{op}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $=$ {\rm{op}}\,({\it{y\/}}, {\rm{op}}\,({\it{b\/}}, {\rm{inv}}\,({\it{g\/}}, {\it{a\/}})\index{inv})\index{op})\index{op})\-
\end{tabbing}
                           
\begin{verbatim}; EQUALITY2: x*a=y*b-->a=((inv g x)*y)*b.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op-equality2 \\ \index{op-equality2}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $=$ {\rm{op}}\,({\it{y\/}}, {\it{b\/}})\index{op}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $=$ {\rm{op}}\,({\rm{op}}\,({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv}, {\it{y\/}})\index{op}, {\it{b\/}})\index{op})\-
\end{tabbing}

\begin{verbatim}; cancellation: xa=ya-->x=y.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  cancellation \\ \index{cancellation}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $=$ {\rm{op}}\,({\it{y\/}}, {\it{a\/}})\index{op}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $=$ {\it{y\/}})\-
\end{tabbing}

\begin{verbatim}; some further simple equalities.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op-equality3 \\ \index{op-equality3}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{g\/}}) $\wedge$ ({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $=$ {\rm{id}}\,({\it{g\/}})\index{id})) \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $=$ {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  op-equality4 \\ \index{op-equality4}
({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\rm{op}}\,({\it{x\/}}, {\it{x\/}})\index{op} $=$ {\it{x\/}})) $\rightarrow$ ({\it{x\/}} $=$ {\rm{id}}\,({\it{g\/}})\index{id})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{subgroup-op} \\  
{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $=$ ({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op}}\,({\it{h\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{h\/}}, {\it{g\/}})\index{subset})
\end{tabbing}

\begin{verbatim}; (id g)=(id h), if h is a subgroup of g.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op-identity-same \\ \index{op-identity-same}
{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\rightarrow$ ({\rm{id}}\,({\it{g\/}})\index{id} $=$ {\rm{id}}\,({\it{h\/}})\index{id})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  op-identity-in-subgroup \\ \index{op-identity-in-subgroup}
{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\rightarrow$ ({\rm{id}}\,({\it{g\/}})\index{id} $\in$ {\it{h\/}})
\end{tabbing}
              

\begin{verbatim}; (inv g x)=(inv h x), if h is a subgroup of g.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op-inverse-same \\ \index{op-inverse-same}
({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}})) $\rightarrow$ ({\rm{inv}}\,({\it{h\/}}, {\it{x\/}})\index{inv} $=$ {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  op-inverse-in-subgroup \\ \index{op-inverse-in-subgroup}
({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}})) $\rightarrow$ ({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv} $\in$ {\it{h\/}})
\end{tabbing}
              
\begin{tabbing}{\sc Theorem}:  group-op-order \\ \index{group-op-order}
{\rm{group-op}}\,({\it{g\/}})\index{group-op} $\rightarrow$ ({\tt{1}} $\leq$ {\rm{cardinal}}\,({\it{g\/}})\index{cardinal})
\end{tabbing}


\noindent{\sc Event}:   Disable group-op.

\addvspace{18pt}

\noindent{\sc Event}:   Disable group-op-associativity1.

\addvspace{18pt}
\begin{verbatim}; we will introduce the axioms for another group with operation OP1.
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it op1\index{op1}\/} of 2 arguments.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{group-op1} \\  
\=\+{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\leftrightarrow$$\;\;\;\;$(\=\+$\forall\;${\it{x\/}}, {\it{y\/}}$\;$((({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{h\/}})) $\rightarrow$ ({\rm{op1}}\,({\it{x\/}}, {\it{y\/}})\index{op1} $\in$ {\it{h\/}}))\index{forall} \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{y\/}}, {\it{z\/}}$\;$(\=\+(({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{h\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op1}}\,({\rm{op1}}\,({\it{x\/}}, {\it{y\/}})\index{op1}, {\it{z\/}})\index{op1} $=$ {\rm{op1}}\,({\it{x\/}}, {\rm{op1}}\,({\it{y\/}}, {\it{z\/}})\index{op1})\index{op1}))\-\index{forall} \\ 
$\wedge$$\;\;\;\;$$\exists\;${\it{id\/}}$\;$(\=\+({\it{id\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$$\forall\;${\it{x\/}}$\;$(\=\+({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{op1}}\,({\it{id\/}}, {\it{x\/}})\index{op1} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\it{id\/}})\index{op1} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$$\exists\;${\it{inv\/}}$\;$(\=\+({\it{inv\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{op1}}\,({\it{inv\/}}, {\it{x\/}})\index{op1} \\ 
$=$$\;\;\;\;${\it{id\/}})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{op1}}\,({\it{x\/}}, {\it{inv\/}})\index{op1} \\ 
$=$$\;\;\;\;${\it{id\/}})\-)\-\index{exists})\-)\-\index{forall})\-\index{exists})\-\-
\end{tabbing}
                                                             
\begin{verbatim}; the group has the "closed" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op1-closed \\ \index{group-op1-closed}
({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{h\/}})) $\rightarrow$ ({\rm{op1}}\,({\it{x\/}}, {\it{y\/}})\index{op1} $\in$ {\it{h\/}})
\end{tabbing}
                      
\begin{verbatim}; the group has the "associativity" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op1-associativity \\ \index{group-op1-associativity}
\=\+({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{h\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op1}}\,({\rm{op1}}\,({\it{x\/}}, {\it{y\/}})\index{op1}, {\it{z\/}})\index{op1} $=$ {\rm{op1}}\,({\it{x\/}}, {\rm{op1}}\,({\it{y\/}}, {\it{z\/}})\index{op1})\index{op1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  group-op1-associativity1 \\ \index{group-op1-associativity1}
\=\+({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{z\/}} $\in$ {\it{h\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\rm{op1}}\,({\it{y\/}}, {\it{z\/}})\index{op1})\index{op1} $=$ {\rm{op1}}\,({\rm{op1}}\,({\it{x\/}}, {\it{y\/}})\index{op1}, {\it{z\/}})\index{op1})\-
\end{tabbing}

\begin{verbatim}; the group has the "identity" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op1-identity \\ \index{group-op1-identity}
\=\+{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{id-1}}\,({\it{h\/}})\index{id-1} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{op1}}\,({\rm{id-1}}\,({\it{h\/}})\index{id-1}, {\it{x\/}})\index{op1} $=$ {\it{x\/}}) $\wedge$ ({\rm{op1}}\,({\it{x\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{op1} $=$ {\it{x\/}})))\-)\-\-
\end{tabbing}

\begin{verbatim}; the group has the "inverse" property.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  group-op1-inverse \\ \index{group-op1-inverse}
\=\+({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{inv-1}}\,({\it{h\/}}, {\it{x\/}})\index{inv-1} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\rm{inv-1}}\,({\it{h\/}}, {\it{x\/}})\index{inv-1}, {\it{x\/}})\index{op1} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\rm{inv-1}}\,({\it{h\/}}, {\it{x\/}})\index{inv-1})\index{op1} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1}))\-\-
\end{tabbing}

\begin{verbatim}; some simple equalities in group.
; OP1-EQUALITY1: x*a=y*b-->x=y*(b*(inv a)).
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op1-equality1 \\ \index{op1-equality1}
\=\+(\=\+{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\it{a\/}})\index{op1} $=$ {\rm{op1}}\,({\it{y\/}}, {\it{b\/}})\index{op1}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $=$ {\rm{op1}}\,({\it{y\/}}, {\rm{op1}}\,({\it{b\/}}, {\rm{inv-1}}\,({\it{h\/}}, {\it{a\/}})\index{inv-1})\index{op1})\index{op1})\-
\end{tabbing}
                           
\begin{verbatim}; EQUALITY2: x*a=y*b-->a=((inv x)*y)*b.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op1-equality2 \\ \index{op1-equality2}
\=\+(\=\+{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\it{a\/}})\index{op1} $=$ {\rm{op1}}\,({\it{y\/}}, {\it{b\/}})\index{op1}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $=$ {\rm{op1}}\,({\rm{op1}}\,({\rm{inv-1}}\,({\it{h\/}}, {\it{x\/}})\index{inv-1}, {\it{y\/}})\index{op1}, {\it{b\/}})\index{op1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  op1-equality3 \\ \index{op1-equality3}
\=\+({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{a\/}} $\in$ {\it{h\/}}) $\wedge$ ({\rm{op1}}\,({\it{x\/}}, {\it{a\/}})\index{op1} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1})) \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $=$ {\rm{inv-1}}\,({\it{h\/}}, {\it{x\/}})\index{inv-1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  op1-equality4 \\ \index{op1-equality4}
({\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ ({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\rm{op1}}\,({\it{x\/}}, {\it{x\/}})\index{op1} $=$ {\it{x\/}})) $\rightarrow$ ({\it{x\/}} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1})
\end{tabbing}

\begin{verbatim}; cancellation: xa=ya-->x=y.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  op1-cancellation \\ \index{op1-cancellation}
\=\+(\=\+{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op1}}\,({\it{x\/}}, {\it{a\/}})\index{op1} $=$ {\rm{op1}}\,({\it{y\/}}, {\it{a\/}})\index{op1}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{x\/}} $=$ {\it{y\/}})\-
\end{tabbing}

\begin{verbatim}; we start to prove the kernel of a group homomorphism is a normal subgroup.
; Introduce homomorphisms.
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it phi\index{phi}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{homo-phi} \\  
\=\+{\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{y\/}}$\;$(\=\+(({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{phi}}\,({\it{x\/}})\index{phi} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{phi}}\,({\it{y\/}})\index{phi} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{phi}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op})\index{phi} $=$ {\rm{op1}}\,({\rm{phi}}\,({\it{x\/}})\index{phi}, {\rm{phi}}\,({\it{y\/}})\index{phi})\index{op1}))\-)\-\index{forall}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  homomorphism-phi \\ \index{homomorphism-phi}
\=\+({\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{phi}}\,({\it{x\/}})\index{phi} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{phi}}\,({\it{y\/}})\index{phi} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{phi}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op})\index{phi} $=$ {\rm{op1}}\,({\rm{phi}}\,({\it{x\/}})\index{phi}, {\rm{phi}}\,({\it{y\/}})\index{phi})\index{op1}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{phi-inv} \\  
\=\+{\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{g\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{phi}}\,({\rm{car}}\,({\it{g\/}}))\index{phi} $=$ {\it{a\/}}$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{g\/}}), {\rm{phi-inv}}\,({\rm{cdr}}\,({\it{g\/}}), {\it{a\/}})\index{phi-inv}) \\ 
{\bf else }{\rm{phi-inv}}\,({\rm{cdr}}\,({\it{g\/}}), {\it{a\/}})\index{phi-inv}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  basic-mapping1 \\ \index{basic-mapping1}
(({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\rm{phi}}\,({\it{x\/}})\index{phi} $=$ {\it{a\/}})) $\rightarrow$ ({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  basic-mapping2 \\ \index{basic-mapping2}
({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv}) $\rightarrow$ ({\rm{phi}}\,({\it{x\/}})\index{phi} $=$ {\it{a\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  phi-inv-subset \\ \index{phi-inv-subset}
{\rm{subset}}\,({\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv}, {\it{g\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  id-to-id \\ \index{id-to-id}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{phi}}\,({\rm{id}}\,({\it{g\/}})\index{id})\index{phi} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  inv-to-inv \\ \index{inv-to-inv}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{phi}}\,({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\index{phi} $=$ {\rm{inv-1}}\,({\it{h\/}}, {\rm{phi}}\,({\it{x\/}})\index{phi})\index{inv-1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-closed \\ \index{ker-closed}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;${\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;${\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\-
\end{tabbing}
                   
\begin{tabbing}{\sc Theorem}:  ker-associativity \\ \index{ker-associativity}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv}) \\ 
$\wedge$$\;\;\;\;$({\it{z\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\it{a\/}})\index{phi-inv}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\it{z\/}})\index{op} $=$ {\rm{op}}\,({\it{x\/}}, {\rm{op}}\,({\it{y\/}}, {\it{z\/}})\index{op})\index{op})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-identity \\ \index{ker-identity}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{id}}\,({\it{g\/}})\index{id} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\-
\end{tabbing}
                           
 \begin{tabbing}{\sc Theorem}:  id-inv-id \\ \index{id-inv-id}
{\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\rightarrow$ ({\rm{inv-1}}\,({\it{h\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{inv-1} $=$ {\rm{id-1}}\,({\it{h\/}})\index{id-1})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-inverse \\ \index{ker-inverse}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;${\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;${\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-identity-inverse \\ \index{ker-identity-inverse}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{x\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{op}}\,({\rm{id}}\,({\it{g\/}})\index{id}, {\it{x\/}})\index{op} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\rm{id}}\,({\it{g\/}})\index{id})\index{op} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv}, {\it{x\/}})\index{op} $=$ {\rm{id}}\,({\it{g\/}})\index{id}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\index{op} $=$ {\rm{id}}\,({\it{g\/}})\index{id}))\-)\-\-
\end{tabbing}
                           
\begin{tabbing}{\sc Theorem}:  ker-subgroup \\ \index{ker-subgroup}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;${\rm{group-op}}\,({\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\index{group-op}\-
\end{tabbing}
                           
\begin{tabbing}{\sc Definition}:\index{op-normalp} \\  
\=\+{\rm{op-normalp}}\,({\it{g\/}}, {\it{n\/}})\index{op-normalp} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{y\/}}$\;$((({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{n\/}})) $\rightarrow$ ({\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\index{op} $\in$ {\it{n\/}}))\index{forall}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{normal-subgroup-op} \\  
\=\+{\rm{normal-subgroup-op}}\,({\it{g\/}}, {\it{n\/}})\index{normal-subgroup-op} \\ 
$=$$\;\;\;\;$({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op}}\,({\it{n\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{n\/}}, {\it{g\/}})\index{subset} $\wedge$ {\rm{op-normalp}}\,({\it{g\/}}, {\it{n\/}})\index{op-normalp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  normal-lemma \\ \index{normal-lemma}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;${\rm{group-op1}}\,({\it{h\/}})\index{group-op1} \\ 
$\wedge$$\;\;\;\;${\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op}, {\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv})\index{op} $\in$ {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-normal \\ \index{ker-normal}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;${\rm{op-normalp}}\,({\it{g\/}}, {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\index{op-normalp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  ker-normal-subgroup \\ \index{ker-normal-subgroup}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op1}}\,({\it{h\/}})\index{group-op1} $\wedge$ {\rm{homo-phi}}\,({\it{g\/}}, {\it{h\/}})\index{homo-phi}) \\ 
$\rightarrow$$\;\;\;\;${\rm{normal-subgroup-op}}\,({\it{g\/}}, {\rm{phi-inv}}\,({\it{g\/}}, {\rm{id-1}}\,({\it{h\/}})\index{id-1})\index{phi-inv})\index{normal-subgroup-op}\-
\end{tabbing}


\noindent{\sc Event}:   Enable group-op-associativity1.

\addvspace{18pt}

\begin{verbatim}; Now back to the proof of Lagrange Theorem.
; Every coset of s in a group is "set-standard".
\end{verbatim}\begin{tabbing}{\sc Theorem}:  right-coset-standard-1 \\ \index{right-coset-standard-1}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ ({\it{a\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{x\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{x\/}} $\not\in$ {\it{s\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $\not\in$ {\rm{right-coset}}\,({\it{s\/}}, {\it{a\/}})\index{right-coset})\-
\end{tabbing}
                           
\begin{tabbing}{\sc Theorem}:  right-coset-standard-2 \\ \index{right-coset-standard-2}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ {\rm{set-standard}}\,({\it{s\/}})\index{set-standard} $\wedge$ ({\it{a\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{set-standard}}\,({\rm{right-coset}}\,({\it{s\/}}, {\it{a\/}})\index{right-coset})\index{set-standard}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-coset-standard \\ \index{right-coset-standard}
\=\+({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ {\rm{set-standard}}\,({\it{h\/}})\index{set-standard} $\wedge$ ({\it{a\/}} $\in$ {\it{g\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{set-standard}}\,({\rm{right-coset}}\,({\it{h\/}}, {\it{a\/}})\index{right-coset})\index{set-standard}\-
\end{tabbing}

\begin{verbatim}; different cosets are disjoint.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  right-coset-disjoint-lemma \\ \index{right-coset-disjoint-lemma}
\=\+(\=\+{\rm{group-op}}\,({\it{g\/}})\index{group-op} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{op}}\,({\rm{inv}}\,({\it{g\/}}, {\it{x\/}})\index{inv}, {\it{y\/}})\index{op} $\in$ {\it{s\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{right-coset}}\,({\it{s\/}}, {\it{b\/}})\index{right-coset}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $\not=$ {\rm{op}}\,({\it{y\/}}, {\it{b\/}})\index{op})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-coset-disjoint-1 \\ \index{right-coset-disjoint-1}
\=\+(\=\+{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{s\/}}, {\it{h\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $\not\in$ {\rm{right-coset}}\,({\it{s\/}}, {\it{b\/}})\index{right-coset})\-
\end{tabbing}
             
\begin{tabbing}{\sc Theorem}:  right-coset-disjoint-2 \\ \index{right-coset-disjoint-2}
\=\+(\=\+{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\in$ {\it{h\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $\not\in$ {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-coset-disjoint-3 \\ \index{right-coset-disjoint-3}
\=\+(\=\+{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{s\/}}, {\it{h\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in$ {\it{g\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\not\in$ {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{set-disjoint}}\,({\rm{right-coset}}\,({\it{s\/}}, {\it{a\/}})\index{right-coset}, {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\index{set-disjoint}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  right-coset-disjoint \\ \index{right-coset-disjoint}
\=\+({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ ({\it{a\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{b\/}} $\in$ {\it{g\/}}) $\wedge$ ({\it{a\/}} $\not\in$ {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})) \\ 
$\rightarrow$$\;\;\;\;${\rm{set-disjoint}}\,({\rm{right-coset}}\,({\it{h\/}}, {\it{a\/}})\index{right-coset}, {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\index{set-disjoint}\-
\end{tabbing}

\begin{verbatim}; Now the Lagrange Theorem will be attacked.
; First, we still need some lemmas.
; first, disable GROUP.
\end{verbatim}
\noindent{\sc Event}:   Disable group-op.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{op-closed} \\  
\=\+{\rm{op-closed}}\,({\it{s1\/}}, {\it{s2\/}})\index{op-closed} \\ 
$\leftrightarrow$$\;\;\;\;$$\forall\;${\it{x\/}}, {\it{y\/}}$\;$((({\it{x\/}} $\in$ {\it{s1\/}}) $\wedge$ ({\it{y\/}} $\in$ {\it{s2\/}})) $\rightarrow$ ({\rm{op}}\,({\it{x\/}}, {\it{y\/}})\index{op} $\in$ {\it{s2\/}}))\index{forall}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  la-lemma1 \\ \index{la-lemma1}
\=\+(({\it{b\/}} $\in$ {\it{s\/}}) $\wedge$ {\rm{subset}}\,({\it{h1\/}}, {\it{h\/}})\index{subset} $\wedge$ {\rm{op-closed}}\,({\it{h\/}}, {\it{s\/}})\index{op-closed}) \\ 
$\rightarrow$$\;\;\;\;${\rm{subset}}\,({\rm{right-coset}}\,({\it{h1\/}}, {\it{b\/}})\index{right-coset}, {\it{s\/}})\index{subset}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  la-lemma2 \\ \index{la-lemma2}
\=\+({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ ({\it{b\/}} $\in$ {\it{g\/}}) $\wedge$ {\rm{op-closed}}\,({\it{h\/}}, {\it{s\/}})\index{op-closed}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{x\/}} $\in$ {\it{h\/}}) $\wedge$ ({\it{a\/}} $\in$ {\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\index{set-minus})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{op}}\,({\it{x\/}}, {\it{a\/}})\index{op} $\in$ {\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\index{set-minus}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  la-lemma3 \\ \index{la-lemma3}
\=\+({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ ({\it{b\/}} $\in$ {\it{g\/}}) $\wedge$ {\rm{op-closed}}\,({\it{h\/}}, {\it{s\/}})\index{op-closed}) \\ 
$\rightarrow$$\;\;\;\;${\rm{op-closed}}\,({\it{h\/}}, {\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\it{b\/}})\index{right-coset})\index{set-minus})\index{op-closed}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lagrange-induct-measure \\ \index{lagrange-induct-measure}
\=\+({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{group-op}}\,({\it{h\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{h\/}}, {\it{g\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ {\rm{listp}}\,({\it{s\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{count}}\,({\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\rm{car}}\,({\it{s\/}}))\index{right-coset})\index{set-minus}) $<$ {\rm{count}}\,({\it{s\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  la-lemma4 \\ \index{la-lemma4}
\=\+(({\it{y\/}} $\leq$ {\it{x\/}}) $\wedge$ ({\tt{1}} $\leq$ {\it{y\/}}) $\wedge$ ((({\it{x\/}} $-$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}})\-
\end{tabbing}
             

\begin{tabbing}{\sc Theorem}:  la-lemma5 \\ \index{la-lemma5}
\=\+(\=\+{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} \\ 
$\wedge$$\;\;\;\;${\rm{set-standard}}\,({\it{h\/}})\index{set-standard} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;${\rm{set-standard}}\,({\it{s\/}})\index{set-standard} \\ 
$\wedge$$\;\;\;\;${\rm{op-closed}}\,({\it{h\/}}, {\it{s\/}})\index{op-closed} \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{cardinal}}\,({\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\rm{car}}\,({\it{s\/}}))\index{right-coset})\index{set-minus})\index{cardinal} ${}${\bf{mod}}${}$ {\rm{cardinal}}\,({\it{h\/}})\index{cardinal}) \\ 
$=$$\;\;\;\;${\tt{0}})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{cardinal}}\,({\it{s\/}})\index{cardinal} ${}${\bf{mod}}${}$ {\rm{cardinal}}\,({\it{h\/}})\index{cardinal}) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lagrange-induct} \\  
\=\+{\rm{lagrange-induct}}\,({\it{g\/}}, {\it{h\/}}, {\it{s\/}})\index{lagrange-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ {\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} $\wedge$ {\rm{listp}}\,({\it{s\/}}) \\ 
{\bf then }{\rm{lagrange-induct}}\,({\it{g\/}}, {\it{h\/}}, {\rm{set-minus}}\,({\it{s\/}}, {\rm{right-coset}}\,({\it{h\/}}, {\rm{car}}\,({\it{s\/}}))\index{right-coset})\index{set-minus})\index{lagrange-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lagrange-generalized \\ \index{lagrange-generalized}
\=\+(\=\+{\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} \\ 
$\wedge$$\;\;\;\;${\rm{set-standard}}\,({\it{h\/}})\index{set-standard} \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\it{s\/}}, {\it{g\/}})\index{subset} \\ 
$\wedge$$\;\;\;\;${\rm{set-standard}}\,({\it{s\/}})\index{set-standard} \\ 
$\wedge$$\;\;\;\;${\rm{op-closed}}\,({\it{h\/}}, {\it{s\/}})\index{op-closed})\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{cardinal}}\,({\it{s\/}})\index{cardinal} ${}${\bf{mod}}${}$ {\rm{cardinal}}\,({\it{h\/}})\index{cardinal}) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{divides}$\;\;$
{\rm{divides}}\,({\it{m\/}}, {\it{n\/}})\index{divides} $=$ (({\it{n\/}} ${}${\bf{mod}}${}$ {\it{m\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-op-closed \\ \index{subset-op-closed}
({\rm{group-op}}\,({\it{g\/}})\index{group-op} $\wedge$ {\rm{subset}}\,({\it{h\/}}, {\it{g\/}})\index{subset}) $\rightarrow$ {\rm{op-closed}}\,({\it{h\/}}, {\it{g\/}})\index{op-closed}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lagrange \\ \index{lagrange}
\=\+({\rm{subgroup-op}}\,({\it{h\/}}, {\it{g\/}})\index{subgroup-op} $\wedge$ {\rm{set-standard}}\,({\it{g\/}})\index{set-standard} $\wedge$ {\rm{set-standard}}\,({\it{h\/}})\index{set-standard}) \\ 
$\rightarrow$$\;\;\;\;${\rm{divides}}\,({\rm{cardinal}}\,({\it{h\/}})\index{cardinal}, {\rm{cardinal}}\,({\it{g\/}})\index{cardinal})\index{divides}\-
\end{tabbing}



%\end{list}
\printindex
\end{document}
