\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 David Russinoff.  All Rights Reserved.

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1994 by David Russinoff.  All Rights
 Reserved."

 NO WARRANTY

 David Russinoff 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 David Russinoff 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.

|#

; Mon Sep 17 12:10:54 CDT 1990

; This events file is an addition to the events files described in A
; Computational Logic Handbook.

; This file is a new version of the proof of Gauss's law of quadratic
; reciprocity.  It was composed entirely by David Russinoff, who also
; composed the Wilson and Gauss events in basic.events.  According to
; Russinoff, the version below is much better than the one in basic.events.
; This version also corresponds to a forthcoming paper of Russinoff in
; the Journal of Automated Reasoning.

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"wilson"}} using the compiled version.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{squares} \\  
\=\+{\rm{squares}}\,({\it{n\/}}, {\it{p\/}})\index{squares} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\tt{0}}, {\bf{nil}}) \\ 
{\bf else }{\rm{cons}}\,(({\it{n\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{squares}}\,({\it{n\/}} $-\;1$, {\it{p\/}})\index{squares})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{residue}$\;\;$
{\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue} $=$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\in$ {\rm{squares}}\,({\it{p\/}}, {\it{p\/}})\index{squares})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-squares-1 \\ \index{all-squares-1}
(({\it{p\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{m\/}} $\leq$ {\it{n\/}})) $\rightarrow$ ((({\it{m\/}} $*$ {\it{m\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\in$ {\rm{squares}}\,({\it{n\/}}, {\it{p\/}})\index{squares})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-squares-2 \\ \index{all-squares-2}
(({\it{y\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ((({\it{y\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $*$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-squares \\ \index{all-squares}
(({\it{p\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not\in$ {\rm{squares}}\,({\it{p\/}}, {\it{p\/}})\index{squares})) $\rightarrow$ ({\it{x\/}} $\not=$ (({\it{y\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-1 \\ \index{euler-1-1}
($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\rightarrow$ (({\tt{2}} $*$ ({\it{p\/}} $\div$ {\tt{2}})) $=$ ({\it{p\/}} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-2 \\ \index{euler-1-2}
($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\rightarrow$ ({\rm{exp}}\,({\it{i\/}} $*$ {\it{i\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} $=$ {\rm{exp}}\,({\it{i\/}}, {\it{p\/}} $-\;1$)\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-3 \\ \index{euler-1-3}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $\rightarrow$ (({\rm{exp}}\,({\it{a\/}}, {\it{c\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\rm{exp}}\,({\it{b\/}}, {\it{c\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-4 \\ \index{euler-1-4}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{i\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{i\/}} $*$ {\it{i\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-5 \\ \index{euler-1-5}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{i\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{i\/}})\index{divides})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-6 \\ \index{euler-1-6}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{i\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1-7 \\ \index{euler-1-7}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\in$ {\rm{squares}}\,({\it{i\/}}, {\it{p\/}})\index{squares}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-1 \\ \index{euler-1}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{complement}$\;\;$
{\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $=$ (({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $*$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable inverse.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  complement-works \\ \index{complement-works}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{j\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{j\/}} $*$ {\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bounded-complement \\ \index{bounded-complement}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $<$ {\it{p\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable complement.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  non-zerop-complement \\ \index{non-zerop-complement}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{j\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $\not\simeq {\tt{0}}$)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  complement-is-unique \\ \index{complement-is-unique}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ((({\it{j\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable squares.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  no-self-complement \\ \index{no-self-complement}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{j\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{j\/}} $\not=$ {\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  complement-of-complement \\ \index{complement-of-complement}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{j\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{complement}}\,({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement}, {\it{a\/}}, {\it{p\/}})\index{complement} $=$ ({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{complements} \\  
\=\+{\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{i\/}} $\in$ {\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements}$\;\;${\bf then }{\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements} \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}}, {\rm{cons}}\,({\rm{complement}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complement}, {\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements}))$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-non-zerop-complements \\ \index{all-non-zerop-complements}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ {\it{p\/}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-non-zerop}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{all-non-zerop}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  bounded-complements \\ \index{bounded-complements}
({\it{i\/}} $<$ {\it{p\/}}) $\rightarrow$ {\rm{all-lesseqp}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements}, {\it{p\/}} $-\;1$)\index{all-lesseqp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subsetp-positives-complements \\ \index{subsetp-positives-complements}
{\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\rm{complements}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{subsetp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  complements-closed-1 \\ \index{complements-closed-1}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\in$ {\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $\in$ {\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  complements-closed-2 \\ \index{complements-closed-2}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $\in$ {\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{j\/}} $\in$ {\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-complements-1 \\ \index{all-distinct-complements-1}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue}) \\ 
$\wedge$$\;\;\;\;${\rm{all-distinct}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{all-distinct})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-distinct}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{all-distinct}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-complements \\ \index{all-distinct-complements}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ {\it{p\/}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-distinct}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{all-distinct}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  perm-positives-complements \\ \index{perm-positives-complements}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})) \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\rm{positives}}\,({\it{p\/}} $-\;1$)\index{positives}, {\rm{complements}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{perm}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  complements-fact \\ \index{complements-fact}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{complements}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} $=$ {\rm{fact}}\,({\it{p\/}} $-\;1$)\index{fact})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-mod-4 \\ \index{times-mod-4}
\=\+((({\it{i\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{i\/}} $*$ ({\it{j\/}} $*$ {\it{k\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{a\/}} $*$ ({\it{k\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements-1 \\ \index{times-complements-1}
\=\+(\=\+((({\it{i\/}} $*$ {\rm{complement}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complement}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{i\/}} $\not\in$ {\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{a\/}} $*$ ({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements-2 \\ \index{times-complements-2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{i\/}})\index{divides}) $\wedge$ ({\it{i\/}} $\not\in$ {\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{a\/}} $*$ ({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus-1 \\ \index{quotient-plus-1}
\=\+(({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ ({\it{x\/}} $+$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(({\it{y\/}} $\div$ {\it{n\/}}) $=$ ($1\;+$ ({\it{x\/}} $\div$ {\it{n\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements-3 \\ \index{times-complements-3}
\=\+(({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{i\/}} $\not\in$ {\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{length}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}}) \\ 
$=$$\;\;\;\;$($1\;+$ ({\rm{length}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements-4 \\ \index{times-complements-4}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{complements}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements-5 \\ \index{times-complements-5}
\=\+({\it{i\/}} $\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-complements \\ \index{times-complements}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{complements}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sub1-length-delete \\ \index{sub1-length-delete}
({\it{x\/}} $\in$ {\it{b\/}}) $\rightarrow$ ({\rm{length}}\,({\rm{delete}}\,({\it{x\/}}, {\it{b\/}})\index{delete})\index{length} $=$ ({\rm{length}}\,({\it{b\/}})\index{length} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-length-perm \\ \index{equal-length-perm}
{\rm{perm}}\,({\it{a\/}}, {\it{b\/}})\index{perm} $\rightarrow$ ({\rm{length}}\,({\it{a\/}})\index{length} $=$ {\rm{length}}\,({\it{b\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-positives \\ \index{length-positives}
{\rm{length}}\,({\rm{positives}}\,({\it{n\/}})\index{positives})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-2-1 \\ \index{euler-2-1}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{complements}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-\;1$))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-2-2 \\ \index{euler-2-2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\rm{complements}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{complements})\index{length} $=$ ({\it{p\/}} $-\;1$))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-2-3 \\ \index{euler-2-3}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides} $=$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}} $-\;1$)\index{divides}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-2-4 \\ \index{euler-2-4}
($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\rightarrow$ ((({\it{p\/}} $-\;1$) $\div$ {\tt{2}}) $=$ ({\it{p\/}} $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-2 \\ \index{euler-2}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-\;1$))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{evenp} \\  
\=\+{\rm{evenp}}\,({\it{x\/}})\index{evenp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }$\neg$ {\rm{evenp}}\,({\it{x\/}} $-\;1$)\index{evenp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  evenp-plus \\ \index{evenp-plus}
{\rm{evenp}}\,({\it{a\/}} $+$ {\it{b\/}})\index{evenp} $=$ ({\rm{evenp}}\,({\it{a\/}})\index{evenp} $=$ {\rm{evenp}}\,({\it{b\/}})\index{evenp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  evenp-diff \\ \index{evenp-diff}
{\rm{evenp}}\,({\it{p\/}} $-$ {\it{x\/}})\index{evenp} $=$ (({\it{p\/}} $<$ {\it{x\/}}) $\vee$ ({\rm{evenp}}\,({\it{p\/}})\index{evenp} $=$ {\rm{evenp}}\,({\it{x\/}})\index{evenp}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  evenp-times \\ \index{evenp-times}
{\rm{evenp}}\,({\it{a\/}} $*$ {\it{b\/}})\index{evenp} $=$ ({\rm{evenp}}\,({\it{a\/}})\index{evenp} $\vee$ {\rm{evenp}}\,({\it{b\/}})\index{evenp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  evenp-even \\ \index{evenp-even}
{\rm{even}}\,({\it{p\/}})\index{even} $=$ {\rm{evenp}}\,({\it{p\/}})\index{evenp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-plus \\ \index{even-plus}
{\rm{even}}\,({\it{a\/}} $+$ {\it{b\/}})\index{even} $=$ ({\rm{even}}\,({\it{a\/}})\index{even} $=$ {\rm{even}}\,({\it{b\/}})\index{even})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-diff \\ \index{even-diff}
{\rm{even}}\,({\it{p\/}} $-$ {\it{x\/}})\index{even} $=$ (({\it{p\/}} $<$ {\it{x\/}}) $\vee$ ({\rm{even}}\,({\it{p\/}})\index{even} $=$ {\rm{even}}\,({\it{x\/}})\index{even}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-times \\ \index{even-times}
{\rm{even}}\,({\it{a\/}} $*$ {\it{b\/}})\index{even} $=$ ({\rm{even}}\,({\it{a\/}})\index{even} $\vee$ {\rm{even}}\,({\it{b\/}})\index{even})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-rem \\ \index{even-rem}
($\neg$ {\rm{even}}\,({\it{p\/}})\index{even}) $\rightarrow$ ({\rm{even}}\,({\it{p\/}} $-$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\index{even} $=$ ($\neg$ {\rm{even}}\,({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}})\index{even}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-add1 \\ \index{even-add1}
{\rm{even}}\,($1\;+$ {\it{x\/}})\index{even} $=$ ($\neg$ {\rm{even}}\,({\it{x\/}})\index{even})
\end{tabbing}


\noindent{\sc Event}:   Disable evenp-even.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  even-prime-2 \\ \index{even-prime-2}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}})) $\rightarrow$ ($\neg$ {\rm{even}}\,({\it{p\/}})\index{even})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-prime \\ \index{even-prime}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}})) $\rightarrow$ (({\it{p\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euler-criterion \\ \index{euler-criterion}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{p\/}} $-\;1$$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable euler-1.

\addvspace{18pt}


\noindent{\sc Event}:   Disable euler-2.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{res1} \\  
\=\+{\rm{res1}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{res1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{p\/}} $\div$ {\tt{2}}) $<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})$\;\;${\bf then }$\neg$ {\rm{res1}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{res1} \\ 
{\bf else }{\rm{res1}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{res1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{reflections} \\  
\=\+{\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }({\it{p\/}} $\div$ {\tt{2}}) $<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
{\bf then }{\rm{cons}}\,({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}), {\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections}) \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  diff-mod-1 \\ \index{diff-mod-1}
({\it{b\/}} $\leq$ {\it{a\/}}) $\rightarrow$ ((({\it{a\/}} $-$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{a\/}} $-$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-diff-times \\ \index{rem-diff-times}
\=\+(({\it{x\/}} $<$ {\it{p\/}}) $\wedge$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$))) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{b\/}} $*$ {\it{p\/}}) $-$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-$ {\it{x\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reflect-commutes-with-times-1 \\ \index{reflect-commutes-with-times-1}
\=\+({\it{y\/}} $\leq$ {\it{p\/}}) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{p\/}} $-$ {\it{y\/}}) $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{p\/}} $-$ (({\it{y\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reflect-commutes-with-times-2 \\ \index{reflect-commutes-with-times-2}
\=\+({\it{y\/}} $\leq$ {\it{p\/}}) \\ 
$\rightarrow$$\;\;\;\;$((({\it{x\/}} $*$ ({\it{p\/}} $-$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{p\/}} $-$ (({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-exp-fact \\ \index{times-exp-fact}
\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $*$ {\it{n\/}}) $*$ ({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact})) ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rem-reflections-1 \\ \index{rem-reflections-1}
\=\+(\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{p\/}} $\div$ {\tt{2}}) $\not<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-reflections-2 \\ \index{rem-reflections-2}
\=\+(\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{p\/}} $\div$ {\tt{2}}) $<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $-$ (({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-reflections-3 \\ \index{rem-reflections-3}
\=\+(\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$((({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $-$ (({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $-$ (({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  double-reflect \\ \index{double-reflect}
({\it{a\/}} $\leq$ {\it{p\/}}) $\rightarrow$ ((({\it{p\/}} $-$ (({\it{p\/}} $-$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-reflections-4 \\ \index{rem-reflections-4}
\=\+(\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{p\/}} $\div$ {\tt{2}}) $<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $-$ (({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-reflections-base-case \\ \index{rem-reflections-base-case}
\=\+({\it{n\/}} $\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rem-reflections \\ \index{rem-reflections}
\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{res1}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{res1}$\;\;${\bf then }({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}} \\ 
{\bf else }({\it{p\/}} $-$ (({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-reflections \\ \index{length-reflections}
{\rm{length}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-lesseqp-reflections-1 \\ \index{all-lesseqp-reflections-1}
(({\it{p\/}} $\div$ {\tt{2}}) $<$ {\it{x\/}}) $\rightarrow$ (({\it{p\/}} $\div$ {\tt{2}}) $\not<$ ({\it{p\/}} $-$ {\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-lesseqp-reflections \\ \index{all-lesseqp-reflections}
{\rm{all-lesseqp}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections}, {\it{p\/}} $\div$ {\tt{2}})\index{all-lesseqp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-non-zerop-reflections \\ \index{all-non-zerop-reflections}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ({\it{b\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-non-zerop}}\,({\rm{reflections}}\,({\it{b\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{all-non-zerop}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-1 \\ \index{all-distinct-reflections-1}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{j\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{p\/}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-2 \\ \index{all-distinct-reflections-2}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $<$ {\it{p\/}}) $\wedge$ ({\it{y\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{p\/}} $-$ {\it{x\/}}) $=$ ({\it{p\/}} $-$ {\it{y\/}})) $=$ ({\it{x\/}} $=$ {\it{y\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-remainder \\ \index{numberp-remainder}
({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-3 \\ \index{all-distinct-reflections-3}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{j\/}} $<$ {\it{i\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{p\/}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) $\not=$ ({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-mod-1 \\ \index{plus-mod-1}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-mod-2 \\ \index{plus-mod-2}
(({\it{y\/}} $+$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-4 \\ \index{all-distinct-reflections-4}
(({\it{x\/}} $=$ ({\it{p\/}} $-$ {\it{y\/}})) $\wedge$ ({\it{y\/}} $<$ {\it{p\/}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{'}}{\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-5 \\ \index{all-distinct-reflections-5}
\=\+(((({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))) $\wedge$ ({\it{p\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ ({\it{i\/}} $+$ {\it{j\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{'}}{\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-6 \\ \index{all-distinct-reflections-6}
\=\+(({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) $\wedge$ ({\it{j\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{i\/}} $+$ {\it{j\/}}) $\not\simeq {\tt{0}}$) $\wedge$ (({\it{i\/}} $+$ {\it{j\/}}) $<$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-7 \\ \index{all-distinct-reflections-7}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) $\wedge$ ({\it{j\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ ({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-8 \\ \index{all-distinct-reflections-8}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) $\wedge$ ({\it{j\/}} $<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) $\not=$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-9 \\ \index{all-distinct-reflections-9}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\not\in$ {\rm{reflections}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections-10 \\ \index{all-distinct-reflections-10}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{p\/}} $-$ (({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) $\not\in$ {\rm{reflections}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-distinct-reflections \\ \index{all-distinct-reflections}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-distinct}}\,({\rm{reflections}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{all-distinct}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-reflections \\ \index{times-reflections}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{reflections}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{times-list} $=$ {\rm{fact}}\,({\it{p\/}} $\div$ {\tt{2}})\index{fact})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-x-x-even \\ \index{plus-x-x-even}
(({\it{x\/}} $+$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{'}}{\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res1-rem-1-1 \\ \index{res1-rem-1-1}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides})) $\rightarrow$ ((({\it{p\/}} $-$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res1-rem-1 \\ \index{res1-rem-1}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;${\rm{res1}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{res1})\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-lessp \\ \index{remainder-lessp}
({\it{a\/}} $<$ {\it{p\/}}) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\rm{fix}}\,({\it{a\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res1-rem-2 \\ \index{res1-rem-2}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{res1}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{res1}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{a\/}}, {\it{p\/}} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  two-even \\ \index{two-even}
($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides}) $\rightarrow$ (({\it{p\/}} $-\;1$) $\not=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  perm-reflections \\ \index{perm-reflections}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\rm{positives}}\,({\it{p\/}} $\div$ {\tt{2}})\index{positives}, {\rm{reflections}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{perm}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gauss-lemma-lemma \\ \index{gauss-lemma-lemma}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{res1}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{res1} $=$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mu} \\  
\=\+{\rm{mu}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{mu} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{p\/}} $\div$ {\tt{2}}) $<$ (({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})$\;\;${\bf then }$1\;+$ {\rm{mu}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{mu} \\ 
{\bf else }{\rm{mu}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{mu}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{gauss}$\;\;$
{\rm{gauss}}\,({\it{a\/}}, {\it{p\/}})\index{gauss} $=$ {\rm{even}}\,({\rm{mu}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{mu})\index{even}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  res1-gauss \\ \index{res1-gauss}
{\rm{res1}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{res1} $=$ {\rm{even}}\,({\rm{mu}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{mu})\index{even}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gauss-lemma \\ \index{gauss-lemma}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{gauss}}\,({\it{a\/}}, {\it{p\/}})\index{gauss} $=$ {\rm{residue}}\,({\it{a\/}}, {\it{p\/}})\index{residue})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum} \\  
\=\+{\rm{sum}}\,({\it{l\/}})\index{sum} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\rm{car}}\,({\it{l\/}}) $+$ {\rm{sum}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sum} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{quotients} \\  
\=\+{\rm{quotients}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{quotients} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) $\div$ {\it{p\/}}, {\rm{quotients}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{quotients})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{remainders} \\  
\=\+{\rm{remainders}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{remainders} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{remainders}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{remainders})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-remainder-sum \\ \index{quotient-remainder-sum}
\=\+({\it{a\/}} $*$ {\rm{sum}}\,({\rm{positives}}\,({\it{n\/}})\index{positives})\index{sum}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $*$ {\rm{sum}}\,({\rm{quotients}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{quotients})\index{sum}) $+$ {\rm{sum}}\,({\rm{remainders}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{remainders})\index{sum})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-remainder-sum-parity \\ \index{quotient-remainder-sum-parity}
\=\+{\rm{even}}\,({\it{a\/}} $*$ {\rm{sum}}\,({\rm{positives}}\,({\it{n\/}})\index{positives})\index{sum})\index{even} \\ 
$=$$\;\;\;\;${\rm{even}}\,(({\it{p\/}} $*$ {\rm{sum}}\,({\rm{quotients}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{quotients})\index{sum}) $+$ {\rm{sum}}\,({\rm{remainders}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{remainders})\index{sum})\index{even}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  even-mu \\ \index{even-mu}
\=\+($\neg$ {\rm{even}}\,({\it{p\/}})\index{even}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{even}}\,({\rm{mu}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{mu})\index{even} \\ 
$=$$\;\;\;\;$(\=\+{\rm{even}}\,({\rm{sum}}\,({\rm{remainders}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{remainders})\index{sum})\index{even} \\ 
$\leftrightarrow$$\;\;\;\;${\rm{even}}\,({\rm{sum}}\,({\rm{reflections}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{sum})\index{even})\-)\-\-
\end{tabbing}

 \begin{tabbing}{\sc Theorem}:  perm-sum-lemma \\ \index{perm-sum-lemma}
({\it{x\/}} $\in$ {\it{m\/}}) $\rightarrow$ (({\it{x\/}} $+$ {\rm{sum}}\,({\rm{delete}}\,({\it{x\/}}, {\it{m\/}})\index{delete})\index{sum}) $=$ {\rm{sum}}\,({\it{m\/}})\index{sum})
\end{tabbing}

 \begin{tabbing}{\sc Theorem}:  perm-sum \\ \index{perm-sum}
{\rm{perm}}\,({\it{l\/}}, {\it{m\/}})\index{perm} $\rightarrow$ ({\rm{sum}}\,({\it{l\/}})\index{sum} $=$ {\rm{sum}}\,({\it{m\/}})\index{sum})
\end{tabbing}

 \begin{tabbing}{\sc Theorem}:  sum-reflections \\ \index{sum-reflections}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sum}}\,({\rm{reflections}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{reflections})\index{sum} $=$ {\rm{sum}}\,({\rm{positives}}\,({\it{p\/}} $\div$ {\tt{2}})\index{positives})\index{sum})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gauss-quotients \\ \index{gauss-quotients}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ($\neg$ {\rm{even}}\,({\it{a\/}})\index{even}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{gauss}}\,({\it{a\/}}, {\it{p\/}})\index{gauss} $=$ {\rm{even}}\,({\rm{sum}}\,({\rm{quotients}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{quotients})\index{sum})\index{even})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-residue-even-plus \\ \index{equal-residue-even-plus}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{q\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{residue}}\,({\it{q\/}}, {\it{p\/}})\index{residue} $=$ {\rm{residue}}\,({\it{p\/}}, {\it{q\/}})\index{residue}) \\ 
$=$$\;\;\;\;${\rm{even}}\,(\=\+{\rm{sum}}\,({\rm{quotients}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{q\/}}, {\it{p\/}})\index{quotients})\index{sum} \\ 
$+$$\;\;\;\;${\rm{sum}}\,({\rm{quotients}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}}, {\it{q\/}})\index{quotients})\index{sum}\-)\index{even})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{w} \\  
\=\+{\rm{w}}\,({\it{x\/}}, {\it{l\/}})\index{w} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{l\/}}) $<$ {\it{x\/}}$\;\;${\bf then }$1\;+$ {\rm{w}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{w} \\ 
{\bf else }{\rm{w}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{w}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{wins} \\  
\=\+{\rm{wins}}\,({\it{k\/}}, {\it{l\/}})\index{wins} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{k\/}})$\;\;${\bf then }{\rm{w}}\,({\rm{car}}\,({\it{k\/}}), {\it{l\/}})\index{w} $+$ {\rm{wins}}\,({\rm{cdr}}\,({\it{k\/}}), {\it{l\/}})\index{wins} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{all-numberp} \\  
\=\+{\rm{all-numberp}}\,({\it{l\/}})\index{all-numberp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }({\rm{car}}\,({\it{l\/}}) $\in\;${\bf{N}}${}$) $\wedge$ {\rm{all-numberp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{all-numberp} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{l} \\  
\=\+{\rm{l}}\,({\it{x\/}}, {\it{l\/}})\index{l} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }$1\;+$ {\rm{l}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{l} \\ 
{\bf else }{\rm{l}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{l}$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{losses} \\  
\=\+{\rm{losses}}\,({\it{k\/}}, {\it{l\/}})\index{losses} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{k\/}})$\;\;${\bf then }{\rm{l}}\,({\rm{car}}\,({\it{k\/}}), {\it{l\/}})\index{l} $+$ {\rm{losses}}\,({\rm{cdr}}\,({\it{k\/}}), {\it{l\/}})\index{losses} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-l-w \\ \index{plus-l-w}
\=\+(({\it{x\/}} $\not\in$ {\it{l\/}}) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{all-numberp}}\,({\it{l\/}})\index{all-numberp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{l}}\,({\it{x\/}}, {\it{l\/}})\index{l} $+$ {\rm{w}}\,({\it{x\/}}, {\it{l\/}})\index{w}) $=$ {\rm{length}}\,({\it{l\/}})\index{length})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-wins-losses \\ \index{plus-wins-losses}
\=\+(({\rm{intersect}}\,({\it{l\/}}, {\it{m\/}})\index{intersect} $\simeq\;${{\bf{nil}}}${}$) $\wedge$ {\rm{all-numberp}}\,({\it{l\/}})\index{all-numberp} $\wedge$ {\rm{all-numberp}}\,({\it{m\/}})\index{all-numberp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{wins}}\,({\it{l\/}}, {\it{m\/}})\index{wins} $+$ {\rm{losses}}\,({\it{l\/}}, {\it{m\/}})\index{losses}) $=$ ({\rm{length}}\,({\it{l\/}})\index{length} $*$ {\rm{length}}\,({\it{m\/}})\index{length}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-wins-losses \\ \index{equal-wins-losses}
{\rm{losses}}\,({\it{l\/}}, {\it{m\/}})\index{losses} $=$ {\rm{wins}}\,({\it{m\/}}, {\it{l\/}})\index{wins}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-wins-wins \\ \index{plus-wins-wins}
\=\+(({\rm{intersect}}\,({\it{l\/}}, {\it{m\/}})\index{intersect} $\simeq\;${{\bf{nil}}}${}$) $\wedge$ {\rm{all-numberp}}\,({\it{l\/}})\index{all-numberp} $\wedge$ {\rm{all-numberp}}\,({\it{m\/}})\index{all-numberp}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{wins}}\,({\it{l\/}}, {\it{m\/}})\index{wins} $+$ {\rm{wins}}\,({\it{m\/}}, {\it{l\/}})\index{wins}) $=$ ({\rm{length}}\,({\it{l\/}})\index{length} $*$ {\rm{length}}\,({\it{m\/}})\index{length}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{mults} \\  
\=\+{\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\it{n\/}} $*$ {\it{p\/}}, {\rm{mults}}\,({\it{n\/}} $-\;1$, {\it{p\/}})\index{mults})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  all-numberp-mults \\ \index{all-numberp-mults}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{all-numberp}}\,({\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{all-numberp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-intersect-mults-lemma \\ \index{empty-intersect-mults-lemma}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{q\/}}) $\wedge$ ({\it{j\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{i\/}} $*$ {\it{p\/}}) $\not\in$ {\rm{mults}}\,({\it{j\/}}, {\it{q\/}})\index{mults})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  empty-intersect-mults \\ \index{empty-intersect-mults}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}}) $\wedge$ ({\it{i\/}} $<$ {\it{q\/}})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{listp}}\,({\rm{intersect}}\,({\rm{mults}}\,({\it{i\/}}, {\it{p\/}})\index{mults}, {\rm{mults}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{q\/}})\index{mults})\index{intersect}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-mults \\ \index{length-mults}
({\it{n\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{length}}\,({\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{length} $=$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-a \\ \index{lessp-a}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\it{a\/}} $<$ (($1\;+$ ({\it{a\/}} $\div$ {\it{p\/}})) $*$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-w-n \\ \index{leq-w-n}
{\it{n\/}} $\not<$ {\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-rewrite \\ \index{lessp-rewrite}
(({\it{a\/}} $<$ ({\it{m\/}} $*$ {\it{p\/}})) $\wedge$ ({\it{m\/}} $\leq$ {\it{n\/}})) $\rightarrow$ ({\it{a\/}} $<$ ({\it{n\/}} $*$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-w-m \\ \index{lessp-w-m}
({\it{a\/}} $<$ ({\it{m\/}} $*$ {\it{p\/}})) $\rightarrow$ ({\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w} $<$ {\it{m\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-w-quotient \\ \index{leq-w-quotient}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w} $\leq$ ({\it{a\/}} $\div$ {\it{p\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  monotone-w \\ \index{monotone-w}
({\it{m\/}} $\leq$ {\it{n\/}}) $\rightarrow$ ({\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{m\/}}, {\it{p\/}})\index{mults})\index{w} $\leq$ {\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-n-w \\ \index{leq-n-w}
(({\it{n\/}} $*$ {\it{p\/}}) $<$ {\it{a\/}}) $\rightarrow$ ({\it{n\/}} $\leq$ {\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-quotient-w \\ \index{leq-quotient-w}
\=\+(({\it{p\/}} $\not\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ (({\it{a\/}} $\div$ {\it{p\/}}) $\leq$ {\it{n\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{a\/}} $\div$ {\it{p\/}}) $\leq$ {\rm{w}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{w})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lqq-induct} \\  
\=\+{\rm{lqq-induct}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{d\/}})\index{lqq-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{d\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{a\/}} $<$ {\it{d\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{c\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{lqq-induct}}\,({\it{a\/}} $-$ {\it{d\/}}, {\it{b\/}}, {\it{c\/}} $-$ {\it{b\/}}, {\it{d\/}})\index{lqq-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-times-quot \\ \index{leq-times-quot}
(({\it{b\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{a\/}} $*$ {\it{b\/}}) $\leq$ ({\it{c\/}} $*$ {\it{d\/}}))) $\rightarrow$ (({\it{a\/}} $\div$ {\it{d\/}}) $\leq$ ({\it{c\/}} $\div$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-j-a \\ \index{leq-j-a}
({\it{j\/}} $\leq$ {\it{a\/}}) $\rightarrow$ (({\it{j\/}} $*$ {\it{q\/}}) $\leq$ ({\it{a\/}} $*$ {\it{q\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-quot-times \\ \index{leq-quot-times}
({\it{j\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})) $\rightarrow$ ((({\it{j\/}} $*$ {\it{q\/}}) $\div$ {\it{p\/}}) $\leq$ ({\it{q\/}} $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-quot-w \\ \index{equal-quot-w}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{q\/}})\index{divides}) $\wedge$ ({\it{j\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{w}}\,({\it{j\/}} $*$ {\it{q\/}}, {\rm{mults}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}})\index{mults})\index{w} $=$ (({\it{j\/}} $*$ {\it{q\/}}) $\div$ {\it{p\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-wins-sum-quotients \\ \index{equal-wins-sum-quotients}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{q\/}})\index{divides}) $\wedge$ ({\it{j\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sum}}\,({\rm{quotients}}\,({\it{j\/}}, {\it{q\/}}, {\it{p\/}})\index{quotients})\index{sum} $=$ {\rm{wins}}\,({\rm{mults}}\,({\it{j\/}}, {\it{q\/}})\index{mults}, {\rm{mults}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}})\index{mults})\index{wins})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  law-of-quadratic-reciprocity \\ \index{law-of-quadratic-reciprocity}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{q\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{residue}}\,({\it{q\/}}, {\it{p\/}})\index{residue} $=$ {\rm{residue}}\,({\it{p\/}}, {\it{q\/}})\index{residue}) $=$ {\rm{even}}\,(({\it{p\/}} $\div$ {\tt{2}}) $*$ ({\it{q\/}} $\div$ {\tt{2}}))\index{even})\-
\end{tabbing}





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