\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{"rsa"}} using the compiled version.

\addvspace{18pt}

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

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{inverse} \\  
\=\+{\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{p\/}} $=$ {\tt{2}}$\;\;${\bf then }{\it{j\/}} ${}${\bf{mod}}${}$ {\tt{2}} \\ 
{\bf else }{\rm{exp}}\,({\it{j\/}}, {\it{p\/}} $-$ {\tt{2}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-inverts-lemma \\ \index{inverse-inverts-lemma}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ((({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\rm{exp}}\,({\it{j\/}}, {\it{p\/}} $-\;1$)\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-inverts \\ \index{inverse-inverts}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) $\rightarrow$ ((({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $*$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-is-unique \\ \index{inverse-is-unique}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\tt{1}} $=$ (({\it{m\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}))) $\rightarrow$ ({\rm{inverse}}\,({\it{m\/}}, {\it{p\/}})\index{inverse} $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  s-p-i-i-lemma1 \\ \index{s-p-i-i-lemma1}
\=\+(({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not=$ {\tt{1}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{n\/}} $-\;1$) $*$ ({\it{n\/}} $-\;1$)) $=$ ({\tt{1}} $+$ ({\it{n\/}} $*$ (({\it{n\/}} $-\;1$) $-\;1$))))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  s-p-i-i-lemma2 \\ \index{s-p-i-i-lemma2}
(({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not=$ {\tt{1}})) $\rightarrow$ (((({\it{n\/}} $-\;1$) $*$ ({\it{n\/}} $-\;1$)) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sub1-p-is-involution \\ \index{sub1-p-is-involution}
{\rm{prime}}\,({\it{p\/}})\index{prime} $\rightarrow$ ({\rm{inverse}}\,({\it{p\/}} $-\;1$, {\it{p\/}})\index{inverse} $=$ ({\it{p\/}} $-\;1$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  n-o-i-lemma1 \\ \index{n-o-i-lemma1}
(({\it{x\/}} $*$ {\it{x\/}}) $-$ {\tt{1}}) $=$ (($1\;+$ {\it{x\/}}) $*$ ({\it{x\/}} $-\;1$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  n-o-i-lemma2 \\ \index{n-o-i-lemma2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (((({\it{j\/}} $*$ {\it{j\/}}) $-$ {\tt{1}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(((($1\;+$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $\vee$ ((({\it{j\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  n-o-i-lemma3 \\ \index{n-o-i-lemma3}
(({\it{a\/}} $\not<$ {\tt{1}}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})) $\rightarrow$ ((({\it{a\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  n-o-i-lemma4 \\ \index{n-o-i-lemma4}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $=$ {\it{j\/}})) \\ 
$\rightarrow$$\;\;\;\;$(((($1\;+$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $\vee$ ((({\it{j\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  no-other-involutions \\ \index{no-other-involutions}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{j\/}} $<$ ({\it{p\/}} $-\;1$)) $\wedge$ ({\tt{1}} $<$ {\it{j\/}})) $\rightarrow$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $\not=$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  i-o-i-lemma \\ \index{i-o-i-lemma}
((({\it{p\/}} $-$ {\tt{2}}) $*$ ({\it{p\/}} $-$ {\tt{2}})) $-\;1$) $=$ (({\it{p\/}} $-$ {\tt{3}}) $*$ ({\it{p\/}} $-\;1$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-of-inverse \\ \index{inverse-of-inverse}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{inverse}}\,({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse}, {\it{p\/}})\index{inverse} $=$ ({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  n-z-i-lemma \\ \index{n-z-i-lemma}
(({\it{i\/}} $\simeq {\tt{0}}$) $\wedge$ ({\tt{1}} $<$ {\it{p\/}})) $\rightarrow$ ({\rm{inverse}}\,({\it{i\/}}, {\it{p\/}})\index{inverse} $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  non-zerop-inverse \\ \index{non-zerop-inverse}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) $\rightarrow$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $\not\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  b-i-lemma2 \\ \index{b-i-lemma2}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $=$ ({\it{p\/}} $-\;1$))) \\ 
$\rightarrow$$\;\;\;\;$(({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-\;1$))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  b-i-lemma1 \\ \index{b-i-lemma1}
({\tt{1}} $<$ {\it{p\/}}) $\rightarrow$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $\leq$ ({\it{p\/}} $-\;1$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  bounded-inverse \\ \index{bounded-inverse}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{j\/}} $<$ ({\it{p\/}} $-\;1$))) $\rightarrow$ ({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $<$ ({\it{p\/}} $-\;1$))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{inverse-list} \\  
\=\+{\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{i\/}} $=$ {\tt{1}}$\;\;${\bf then }{\rm{cons}}\,({\tt{1}}, {\bf{nil}}) \\ 
{\bf elseif }{\it{i\/}} $\in$ {\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list}$\;\;${\bf then }{\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list} \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}}, {\rm{cons}}\,({\rm{inverse}}\,({\it{i\/}}, {\it{p\/}})\index{inverse}, {\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list}))$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-inverse-list \\ \index{all-non-zerop-inverse-list}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ ({\it{p\/}} $-\;1$))) $\rightarrow$ {\rm{all-non-zerop}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{all-non-zerop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  bounded-inverse-list \\ \index{bounded-inverse-list}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ ({\it{p\/}} $-\;1$)) $\wedge$ ({\it{j\/}} $=$ ({\it{p\/}} $-$ {\tt{2}}))) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-lesseqp}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list}, {\it{j\/}})\index{all-lesseqp}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-positives \\ \index{subsetp-positives}
{\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\rm{inverse-list}}\,({\it{n\/}}, {\it{p\/}})\index{inverse-list})\index{subsetp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-1 \\ \index{inverse-1}
({\tt{1}} $<$ {\it{p\/}}) $\rightarrow$ ({\rm{inverse}}\,({\tt{1}}, {\it{p\/}})\index{inverse} $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  a-d-i-l-lemma1 \\ \index{a-d-i-l-lemma1}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{i\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{i\/}} $<$ {\it{p\/}}) $\wedge$ ({\it{j\/}} $\in$ {\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $\in$ {\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  a-d-i-l-lemma2 \\ \index{a-d-i-l-lemma2}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$(({\it{i\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{j\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{j\/}} $<$ {\it{p\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{inverse}}\,({\it{j\/}}, {\it{p\/}})\index{inverse} $\in$ {\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list}))\- \\ 
$\rightarrow$$\;\;\;\;$({\it{j\/}} $\in$ {\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  a-d-i-l-lemma3 \\ \index{a-d-i-l-lemma3}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ ({\it{p\/}} $-\;1$)) $\wedge$ {\rm{all-distinct}}\,({\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list})\index{all-distinct}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-distinct}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{all-distinct}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-inverse-list \\ \index{all-distinct-inverse-list}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ ({\it{p\/}} $-\;1$))) $\rightarrow$ {\rm{all-distinct}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{all-distinct}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  t-i-l-lemma1 \\ \index{t-i-l-lemma1}
((({\it{a\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}}) $\rightarrow$ ((({\it{a\/}} $*$ ({\it{b\/}} $*$ {\it{c\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{c\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  t-i-l-lemma \\ \index{t-i-l-lemma}
\=\+((({\it{i\/}} $*$ {\rm{inverse}}\,({\it{i\/}}, {\it{p\/}})\index{inverse}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  t-i-l-lemma3 \\ \index{t-i-l-lemma3}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{i\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) \\ 
$=$$\;\;\;\;$({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}} $-\;1$, {\it{p\/}})\index{inverse-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  t-i-l-lemma4 \\ \index{t-i-l-lemma4}
({\it{i\/}} $\leq$ {\tt{1}}) $\rightarrow$ ({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{times-list} $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-inverse-list \\ \index{times-inverse-list}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $<$ {\it{p\/}})) $\rightarrow$ (({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  delete-x-leave-a \\ \index{delete-x-leave-a}
(({\it{a\/}} $\in$ {\it{s\/}}) $\wedge$ ({\it{a\/}} $\not=$ {\it{x\/}})) $\rightarrow$ ({\it{a\/}} $\in$ {\rm{delete}}\,({\it{x\/}}, {\it{s\/}})\index{delete})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  delete-member-leave-subset \\ \index{delete-member-leave-subset}
({\rm{subsetp}}\,({\it{r\/}}, {\it{s\/}})\index{subsetp} $\wedge$ ({\it{x\/}} $\not\in$ {\it{r\/}})) $\rightarrow$ {\rm{subsetp}}\,({\it{r\/}}, {\rm{delete}}\,({\it{x\/}}, {\it{s\/}})\index{delete})\index{subsetp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-lesseqp-delete \\ \index{all-lesseqp-delete}
({\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} $\wedge$ {\rm{all-lesseqp}}\,({\it{l\/}}, {\it{n\/}})\index{all-lesseqp}) $\rightarrow$ {\rm{all-lesseqp}}\,({\rm{delete}}\,({\it{n\/}}, {\it{l\/}})\index{delete}, {\it{n\/}} $-\;1$)\index{all-lesseqp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  positives-bounded \\ \index{positives-bounded}
({\it{n\/}} $<$ {\it{m\/}}) $\rightarrow$ ({\it{m\/}} $\not\in$ {\rm{positives}}\,({\it{n\/}})\index{positives})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-positives-delete \\ \index{subsetp-positives-delete}
{\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\it{l\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}} $-\;1$)\index{positives}, {\rm{delete}}\,({\it{n\/}}, {\it{l\/}})\index{delete})\index{subsetp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nonzerop-lesseqp-zero \\ \index{nonzerop-lesseqp-zero}
(({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ {\rm{all-lesseqp}}\,({\it{l\/}}, {\it{n\/}})\index{all-lesseqp} $\wedge$ {\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop}) $\rightarrow$ ($\neg$ {\rm{listp}}\,({\it{l\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pigeonhole2-induction} \\  
\=\+{\rm{pigeonhole2-induction}}\,({\it{l\/}}, {\it{n\/}})\index{pigeonhole2-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{pigeonhole2-induction}}\,({\rm{delete}}\,({\it{n\/}}, {\it{l\/}})\index{delete}, {\it{n\/}} $-\;1$)\index{pigeonhole2-induction}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pigeonhole2 \\ \index{pigeonhole2}
\=\+(\=\+{\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} \\ 
$\wedge$$\;\;\;\;${\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} \\ 
$\wedge$$\;\;\;\;${\rm{all-lesseqp}}\,({\it{l\/}}, {\it{n\/}})\index{all-lesseqp} \\ 
$\wedge$$\;\;\;\;${\rm{subsetp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\it{l\/}})\index{subsetp})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\it{l\/}})\index{perm}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-positives-inverse-list \\ \index{perm-positives-inverse-list}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $=$ ({\it{p\/}} $-$ {\tt{2}}))) $\rightarrow$ {\rm{perm}}\,({\rm{positives}}\,({\it{i\/}})\index{positives}, {\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{perm}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  inverse-list-fact \\ \index{inverse-list-fact}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $=$ ({\it{p\/}} $-$ {\tt{2}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{inverse-list}}\,({\it{i\/}}, {\it{p\/}})\index{inverse-list})\index{times-list} $=$ {\rm{fact}}\,({\it{i\/}})\index{fact})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  w-t-lemma \\ \index{w-t-lemma}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{i\/}} $=$ ({\it{p\/}} $-$ {\tt{2}}))) $\rightarrow$ (({\rm{fact}}\,({\it{i\/}})\index{fact} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  wilson-thm \\ \index{wilson-thm}
{\rm{prime}}\,({\it{p\/}})\index{prime} $\rightarrow$ (({\rm{fact}}\,({\it{p\/}} $-\;1$)\index{fact} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{p\/}} $-\;1$))
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"wilson"}} and compile it.

\addvspace{18pt}

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