\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.

|#

; Work of David Russinoff.

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

\addvspace{18pt}

\noindent{\sc Event}:   For efficiency, compile those definitions not yet compiled.

\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{list}}\,({\tt{0}}) \\ 
{\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} $=$ (($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ (({\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$ {\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}:   Enable inverse; name this event `g0219'.\index{g0219}

\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}:   Enable complement; name this event `complement-off'.\index{complement-off}

\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}:   Enable squares; name this event `squares-off'.\index{squares-off}

\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{comp-list} \\  
\=\+{\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{i\/}} $\in$ {\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list}$\;\;${\bf then }{\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list} \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}}, {\rm{cons}}\,({\rm{complement}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{complement}, {\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list}))$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-comp-list \\ \index{all-non-zerop-comp-list}
\=\+({\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{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{all-non-zerop}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  bounded-comp-list \\ \index{bounded-comp-list}
({\it{i\/}} $<$ {\it{p\/}}) $\rightarrow$ {\rm{all-lesseqp}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list}, {\it{p\/}} $-\;1$)\index{all-lesseqp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-positives-comp-list \\ \index{subsetp-positives-comp-list}
{\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\rm{comp-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{subsetp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  comp-list-closed-1 \\ \index{comp-list-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{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{complement}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{complement} $\in$ {\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  comp-list-closed-2 \\ \index{comp-list-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{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{j\/}} $\in$ {\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-comp-list-1 \\ \index{all-distinct-comp-list-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{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{all-distinct})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{all-distinct}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{all-distinct}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-comp-list \\ \index{all-distinct-comp-list}
\=\+({\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{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{all-distinct}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-positives-comp-list \\ \index{perm-positives-comp-list}
\=\+({\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{comp-list}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{perm}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  comp-list-fact \\ \index{comp-list-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{comp-list}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\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-comp-list-1 \\ \index{times-comp-list-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{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{a\/}} $*$ ({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-comp-list-2 \\ \index{times-comp-list-2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{i\/}})\index{divides}) $\wedge$ ({\it{i\/}} $\not\in$ {\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$(({\it{a\/}} $*$ ({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\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-comp-list-3 \\ \index{times-comp-list-3}
\=\+(({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{i\/}} $\not\in$ {\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{length} $\div$ {\tt{2}}) \\ 
$=$$\;\;\;\;$($1\;+$ ({\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{length} $\div$ {\tt{2}})))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-comp-list-4 \\ \index{times-comp-list-4}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-comp-list-5 \\ \index{times-comp-list-5}
\=\+({\it{i\/}} $\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{length} $\div$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-comp-list \\ \index{times-comp-list}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{a\/}}, {\rm{length}}\,({\rm{comp-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{comp-list})\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{comp-list}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\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{comp-list}}\,({\it{p\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{comp-list})\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{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{reflect}$\;\;$
{\rm{reflect}}\,({\it{x\/}}, {\it{p\/}})\index{reflect} $=$ ({\it{p\/}} $-$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{reflect-list} \\  
\=\+{\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list} \\ 
$=$$\;\;\;\;$\=\+{\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}}\,({\rm{reflect}}\,(({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect}, {\rm{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list}) \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list})$\;${\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$$\;\;\;\;$((({\rm{reflect}}\,({\it{y\/}}, {\it{p\/}})\index{reflect} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\rm{reflect}}\,(({\it{y\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\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\/}} $*$ {\rm{reflect}}\,({\it{y\/}}, {\it{p\/}})\index{reflect}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\rm{reflect}}\,(({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\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-reflect-list-1 \\ \index{rem-reflect-list-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{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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-reflect-list-2 \\ \index{rem-reflect-list-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{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{reflect}}\,(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rem-reflect-list-3 \\ \index{rem-reflect-list-3}
\=\+(\=\+({\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{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{reflect}}\,(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{reflect}}\,(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  double-reflect \\ \index{double-reflect}
({\it{a\/}} $\leq$ {\it{p\/}}) $\rightarrow$ (({\rm{reflect}}\,({\rm{reflect}}\,({\it{a\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rem-reflect-list-4 \\ \index{rem-reflect-list-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{reflect-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{reflect}}\,(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}} $-\;1$)\index{exp} $*$ {\rm{fact}}\,({\it{n\/}} $-\;1$)\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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-reflect-list-base-case \\ \index{rem-reflect-list-base-case}
\=\+({\it{n\/}} $\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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-reflect-list \\ \index{rem-reflect-list}
\=\+({\it{p\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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 }{\rm{reflect}}\,(({\rm{exp}}\,({\it{a\/}}, {\it{n\/}})\index{exp} $*$ {\rm{fact}}\,({\it{n\/}})\index{fact}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} ${}${\bf{mod}}${}$ {\it{p\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-reflect-list \\ \index{length-reflect-list}
{\rm{length}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-lesseqp-reflect-list-1 \\ \index{all-lesseqp-reflect-list-1}
(({\it{p\/}} $\div$ {\tt{2}}) $<$ {\it{x\/}}) $\rightarrow$ (({\it{p\/}} $\div$ {\tt{2}}) $\not<$ {\rm{reflect}}\,({\it{x\/}}, {\it{p\/}})\index{reflect})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-lesseqp-reflect-list \\ \index{all-lesseqp-reflect-list}
{\rm{all-lesseqp}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list}, {\it{p\/}} $\div$ {\tt{2}})\index{all-lesseqp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-reflect-list \\ \index{all-non-zerop-reflect-list}
\=\+({\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{reflect-list}}\,({\it{b\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{all-non-zerop}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-1 \\ \index{all-distinct-reflect-list-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-reflect-list-2 \\ \index{all-distinct-reflect-list-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-reflect-list-3 \\ \index{all-distinct-reflect-list-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$$\;\;\;\;$({\rm{reflect}}\,(({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} $\not=$ {\rm{reflect}}\,(({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect})\-
\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-reflect-list-4 \\ \index{all-distinct-reflect-list-4}
(({\it{x\/}} $=$ ({\it{p\/}} $-$ {\it{y\/}})) $\wedge$ ({\it{y\/}} $<$ {\it{p\/}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-5 \\ \index{all-distinct-reflect-list-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{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-6 \\ \index{all-distinct-reflect-list-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-reflect-list-7 \\ \index{all-distinct-reflect-list-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=$ {\rm{reflect}}\,(({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-8 \\ \index{all-distinct-reflect-list-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$$\;\;\;\;$({\rm{reflect}}\,(({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} $\not=$ (({\it{a\/}} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-9 \\ \index{all-distinct-reflect-list-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{reflect-list}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list-10 \\ \index{all-distinct-reflect-list-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$$\;\;\;\;$({\rm{reflect}}\,(({\it{a\/}} $*$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\it{p\/}})\index{reflect} $\not\in$ {\rm{reflect-list}}\,({\it{j\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-reflect-list \\ \index{all-distinct-reflect-list}
\=\+(\=\+{\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{reflect-list}}\,({\it{i\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{all-distinct}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-reflect-list \\ \index{times-reflect-list}
\=\+({\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{reflect-list}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\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{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}:  gauss-lemma \\ \index{gauss-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{plus-list} \\  
\=\+{\rm{plus-list}}\,({\it{l\/}})\index{plus-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{car}}\,({\it{l\/}}) $+$ {\rm{plus-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{plus-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{quot-list} \\  
\=\+{\rm{quot-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{quot-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) $\div$ {\it{p\/}}, {\rm{quot-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{quot-list})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{rem-list} \\  
\=\+{\rm{rem-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{rem-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(({\it{a\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{rem-list}}\,({\it{n\/}} $-\;1$, {\it{a\/}}, {\it{p\/}})\index{rem-list})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rem-quot-list \\ \index{rem-quot-list}
\=\+({\it{a\/}} $*$ {\rm{plus-list}}\,({\rm{positives}}\,({\it{n\/}})\index{positives})\index{plus-list}) \\ 
$=$$\;\;\;\;$(({\it{p\/}} $*$ {\rm{plus-list}}\,({\rm{quot-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{quot-list})\index{plus-list}) $+$ {\rm{plus-list}}\,({\rm{rem-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{rem-list})\index{plus-list})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{even3} \\  
\=\+{\rm{even3}}\,({\it{x\/}})\index{even3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }$\neg$ {\rm{even3}}\,({\it{x\/}} $-\;1$)\index{even3}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-plus \\ \index{even3-plus}
{\rm{even3}}\,({\it{a\/}} $+$ {\it{b\/}})\index{even3} $=$ ({\rm{even3}}\,({\it{a\/}})\index{even3} $=$ {\rm{even3}}\,({\it{b\/}})\index{even3})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-diff \\ \index{even3-diff}
({\it{x\/}} $\leq$ {\it{p\/}}) $\rightarrow$ ({\rm{even3}}\,({\it{p\/}} $-$ {\it{x\/}})\index{even3} $=$ ({\rm{even3}}\,({\it{p\/}})\index{even3} $=$ {\rm{even3}}\,({\it{x\/}})\index{even3}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-times \\ \index{even3-times}
{\rm{even3}}\,({\it{a\/}} $*$ {\it{b\/}})\index{even3} $=$ ({\rm{even3}}\,({\it{a\/}})\index{even3} $\vee$ {\rm{even3}}\,({\it{b\/}})\index{even3})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-rem \\ \index{even3-rem}
($\neg$ {\rm{even3}}\,({\it{p\/}})\index{even3}) $\rightarrow$ ({\rm{even3}}\,({\it{p\/}} $-$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\index{even3} $=$ ($\neg$ {\rm{even3}}\,({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}})\index{even3}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-rem-reflect \\ \index{even3-rem-reflect}
\=\+($\neg$ {\rm{even3}}\,({\it{p\/}})\index{even3}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{res1}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{res1} \\ 
$=$$\;\;\;\;$(\=\+{\rm{even3}}\,({\rm{plus-list}}\,({\rm{rem-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{rem-list})\index{plus-list})\index{even3} \\ 
$\leftrightarrow$$\;\;\;\;${\rm{even3}}\,({\rm{plus-list}}\,({\rm{reflect-list}}\,({\it{n\/}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{plus-list})\index{even3})\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-plus-list-1 \\ \index{perm-plus-list-1}
({\it{x\/}} $\in$ {\it{m\/}}) $\rightarrow$ (({\it{x\/}} $+$ {\rm{plus-list}}\,({\rm{delete}}\,({\it{x\/}}, {\it{m\/}})\index{delete})\index{plus-list}) $=$ {\rm{plus-list}}\,({\it{m\/}})\index{plus-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-plus-list \\ \index{perm-plus-list}
{\rm{perm}}\,({\it{l\/}}, {\it{m\/}})\index{perm} $\rightarrow$ ({\rm{plus-list}}\,({\it{l\/}})\index{plus-list} $=$ {\rm{plus-list}}\,({\it{m\/}})\index{plus-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even3-even \\ \index{even3-even}
{\rm{divides}}\,({\tt{2}}, {\it{p\/}})\index{divides} $=$ {\rm{even3}}\,({\it{p\/}})\index{even3}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-reflect-list \\ \index{plus-reflect-list}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{even3}}\,({\it{p\/}})\index{even3})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{plus-list}}\,({\rm{reflect-list}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{reflect-list})\index{plus-list} \\ 
$=$$\;\;\;\;${\rm{plus-list}}\,({\rm{positives}}\,({\it{p\/}} $\div$ {\tt{2}})\index{positives})\index{plus-list})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equals-have-same-parity \\ \index{equals-have-same-parity}
({\it{x\/}} $=$ {\it{y\/}}) $\rightarrow$ ({\rm{even3}}\,({\it{x\/}})\index{even3} $=$ {\rm{even3}}\,({\it{y\/}})\index{even3})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  res1-quot-list \\ \index{res1-quot-list}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{even3}}\,({\it{p\/}})\index{even3}) $\wedge$ ($\neg$ {\rm{even3}}\,({\it{a\/}})\index{even3}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{a\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{res1}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{res1} $=$ {\rm{even3}}\,({\rm{plus-list}}\,({\rm{quot-list}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{a\/}}, {\it{p\/}})\index{quot-list})\index{plus-list})\index{even3})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{wins1} \\  
\=\+{\rm{wins1}}\,({\it{x\/}}, {\it{l\/}})\index{wins1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{car}}\,({\it{l\/}}) $<$ {\it{x\/}}$\;\;${\bf then }$1\;+$ {\rm{wins1}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{wins1} \\ 
{\bf else }{\rm{wins1}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{wins1}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{wins} \\  
\=\+{\rm{wins}}\,({\it{k\/}}, {\it{l\/}})\index{wins} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{wins1}}\,({\rm{car}}\,({\it{k\/}}), {\it{l\/}})\index{wins1} $+$ {\rm{wins}}\,({\rm{cdr}}\,({\it{k\/}}), {\it{l\/}})\index{wins}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{losses1} \\  
\=\+{\rm{losses1}}\,({\it{x\/}}, {\it{l\/}})\index{losses1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{x\/}} $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }$1\;+$ {\rm{losses1}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{losses1} \\ 
{\bf else }{\rm{losses1}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{losses1}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{losses} \\  
\=\+{\rm{losses}}\,({\it{k\/}}, {\it{l\/}})\index{losses} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{losses1}}\,({\rm{car}}\,({\it{k\/}}), {\it{l\/}})\index{losses1} $+$ {\rm{losses}}\,({\rm{cdr}}\,({\it{k\/}}), {\it{l\/}})\index{losses}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  win-some-lose-some-1 \\ \index{win-some-lose-some-1}
\=\+(({\it{x\/}} $\not\in$ {\it{l\/}}) $\wedge$ {\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{losses1}}\,({\it{x\/}}, {\it{l\/}})\index{losses1} $+$ {\rm{wins1}}\,({\it{x\/}}, {\it{l\/}})\index{wins1}) $=$ {\rm{length}}\,({\it{l\/}})\index{length})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  win-some-lose-some-2 \\ \index{win-some-lose-some-2}
\=\+(({\rm{intersect}}\,({\it{l\/}}, {\it{m\/}})\index{intersect} $\simeq\;${{\bf{nil}}}${}$) $\wedge$ {\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} $\wedge$ {\rm{all-non-zerop}}\,({\it{m\/}})\index{all-non-zerop}) \\ 
$\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-losses-wins \\ \index{equal-losses-wins}
{\rm{losses}}\,({\it{l\/}}, {\it{m\/}})\index{losses} $=$ {\rm{wins}}\,({\it{m\/}}, {\it{l\/}})\index{wins}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  a-winner-every-time \\ \index{a-winner-every-time}
\=\+(({\rm{intersect}}\,({\it{l\/}}, {\it{m\/}})\index{intersect} $\simeq\;${{\bf{nil}}}${}$) $\wedge$ {\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} $\wedge$ {\rm{all-non-zerop}}\,({\it{m\/}})\index{all-non-zerop}) \\ 
$\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}:  length-mults \\ \index{length-mults}
{\rm{length}}\,({\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-n-wins1 \\ \index{leq-n-wins1}
(({\it{n\/}} $*$ {\it{p\/}}) $<$ {\it{a\/}}) $\rightarrow$ ({\it{n\/}} $\leq$ {\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  monotone-wins1 \\ \index{monotone-wins1}
({\it{n\/}} $\leq$ {\it{m\/}}) $\rightarrow$ ({\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1} $\leq$ {\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{m\/}}, {\it{p\/}})\index{mults})\index{wins1})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{quot-quot-induction} \\  
\=\+{\rm{quot-quot-induction}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{d\/}})\index{quot-quot-induction} \\ 
$=$$\;\;\;\;$\=\+{\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{quot-quot-induction}}\,({\it{a\/}} $-$ {\it{d\/}}, {\it{b\/}}, {\it{c\/}} $-$ {\it{b\/}}, {\it{d\/}})\index{quot-quot-induction}$\;${\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-quot-times \\ \index{leq-quot-times}
((({\it{p\/}} $\div$ {\tt{2}}) $*$ {\it{q\/}}) $\div$ {\it{p\/}}) $\leq$ ({\it{q\/}} $\div$ {\tt{2}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{monotone-quot-induction} \\  
\=\+{\rm{monotone-quot-induction}}\,({\it{i\/}}, {\it{j\/}}, {\it{p\/}})\index{monotone-quot-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{p\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{i\/}} $<$ {\it{p\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{j\/}} $<$ {\it{p\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{monotone-quot-induction}}\,({\it{i\/}} $-$ {\it{p\/}}, {\it{j\/}} $-$ {\it{p\/}}, {\it{p\/}})\index{monotone-quot-induction}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  monotone-quot \\ \index{monotone-quot}
({\it{j\/}} $\leq$ {\it{i\/}}) $\rightarrow$ (({\it{j\/}} $\div$ {\it{p\/}}) $\leq$ ({\it{i\/}} $\div$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-quot-times-2 \\ \index{leq-quot-times-2}
({\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}:  leq-quot-wins1-1 \\ \index{leq-quot-wins1-1}
($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{x\/}})\index{divides}) $\rightarrow$ ((({\it{x\/}} $\div$ {\it{p\/}}) $*$ {\it{p\/}}) $<$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-quot-wins1-2 \\ \index{leq-quot-wins1-2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{q\/}})\index{divides}) $\wedge$ ({\it{q\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{j\/}} $*$ {\it{q\/}}) $\div$ {\it{p\/}}) $*$ {\it{p\/}}) $<$ ({\it{j\/}} $*$ {\it{q\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-quot-wins1 \\ \index{leq-quot-wins1}
\=\+(\=\+{\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}})) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{q\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$((({\it{j\/}} $*$ {\it{q\/}}) $\div$ {\it{p\/}}) $\leq$ {\rm{wins1}}\,({\it{j\/}} $*$ {\it{q\/}}, {\rm{mults}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}})\index{mults})\index{wins1})\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{wins2} \\  
\=\+{\rm{wins2}}\,({\it{a\/}}, {\it{n\/}}, {\it{p\/}})\index{wins2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{n\/}} $*$ {\it{p\/}}) $<$ {\it{a\/}}$\;\;${\bf then }{\it{n\/}} \\ 
{\bf else }{\rm{wins2}}\,({\it{a\/}}, {\it{n\/}} $-\;1$, {\it{p\/}})\index{wins2}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-wins2 \\ \index{leq-wins2}
({\rm{wins2}}\,({\it{a\/}}, {\it{n\/}}, {\it{p\/}})\index{wins2} $*$ {\it{p\/}}) $\leq$ {\it{a\/}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-wins1-n \\ \index{leq-wins1-n}
{\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1} $\leq$ {\it{n\/}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-wins1-wins2 \\ \index{leq-wins1-wins2}
{\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1} $\leq$ {\rm{wins2}}\,({\it{a\/}}, {\it{n\/}}, {\it{p\/}})\index{wins2}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-wins1 \\ \index{leq-wins1}
({\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1} $*$ {\it{p\/}}) $\leq$ {\it{a\/}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-wins1-quot \\ \index{leq-wins1-quot}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{wins1}}\,({\it{a\/}}, {\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{wins1} $\leq$ ({\it{a\/}} $\div$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-quot-wins1 \\ \index{equal-quot-wins1}
\=\+(\=\+{\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}})) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{q\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{wins1}}\,({\it{j\/}} $*$ {\it{q\/}}, {\rm{mults}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}})\index{mults})\index{wins1} $=$ (({\it{j\/}} $*$ {\it{q\/}}) $\div$ {\it{p\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-wins-plus-quot-list \\ \index{equal-wins-plus-quot-list}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{divides}}\,({\it{p\/}}, {\it{q\/}})\index{divides}) \\ 
$\wedge$$\;\;\;\;$({\it{q\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $\leq$ ({\it{p\/}} $\div$ {\tt{2}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{wins}}\,({\rm{mults}}\,({\it{j\/}}, {\it{q\/}})\index{mults}, {\rm{mults}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}})\index{mults})\index{wins} $=$ {\rm{plus-list}}\,({\rm{quot-list}}\,({\it{j\/}}, {\it{q\/}}, {\it{p\/}})\index{quot-list})\index{plus-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gauss-corollary \\ \index{gauss-corollary}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{q\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{res1}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{q\/}}, {\it{p\/}})\index{res1} $=$ {\rm{residue}}\,({\it{q\/}}, {\it{p\/}})\index{residue})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  residue-quot-list \\ \index{residue-quot-list}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}}) $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{q\/}} $\not=$ {\tt{2}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{residue}}\,({\it{q\/}}, {\it{p\/}})\index{residue} $=$ {\rm{residue}}\,({\it{p\/}}, {\it{q\/}})\index{residue}) \\ 
$=$$\;\;\;\;${\rm{even3}}\,(\=\+{\rm{plus-list}}\,({\rm{quot-list}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{q\/}}, {\it{p\/}})\index{quot-list})\index{plus-list} \\ 
$+$$\;\;\;\;${\rm{plus-list}}\,({\rm{quot-list}}\,({\it{q\/}} $\div$ {\tt{2}}, {\it{p\/}}, {\it{q\/}})\index{quot-list})\index{plus-list}\-)\index{even3})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-mults \\ \index{all-non-zerop-mults}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{all-non-zerop}}\,({\rm{mults}}\,({\it{n\/}}, {\it{p\/}})\index{mults})\index{all-non-zerop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  empty-intersect-mults-1 \\ \index{empty-intersect-mults-1}
\=\+({\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}:  equal-plus-quot-list-wins \\ \index{equal-plus-quot-list-wins}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{plus-list}}\,({\rm{quot-list}}\,({\it{p\/}} $\div$ {\tt{2}}, {\it{q\/}}, {\it{p\/}})\index{quot-list})\index{plus-list} \\ 
$=$$\;\;\;\;${\rm{wins}}\,({\rm{mults}}\,({\it{p\/}} $\div$ {\tt{2}}, {\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$ {\rm{prime}}\,({\it{q\/}})\index{prime} $\wedge$ ({\it{p\/}} $\not=$ {\it{q\/}}) $\wedge$ ({\it{p\/}} $\not=$ {\tt{2}}) $\wedge$ ({\it{q\/}} $\not=$ {\tt{2}})) \\ 
$\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}
