\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 Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

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

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE 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 Robert S. Boyer or J Strother Moore 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.

|#

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

\addvspace{18pt}

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

\addvspace{18pt}

\noindent{\sc Event}:   Disable euclid.

\addvspace{18pt}

\noindent{\sc Event}:   Disable quotient-divides.

\addvspace{18pt}

\noindent{\sc Event}:   Disable if-times-then-divides.

\addvspace{18pt}

\noindent{\sc Event}:   Disable times.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{crypt} \\  
\=\+{\rm{crypt}}\,({\it{m\/}}, {\it{e\/}}, {\it{n\/}})\index{crypt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\rm{even}}\,({\it{e\/}})\index{even}$\;\;${\bf then }{\rm{square}}\,({\rm{crypt}}\,({\it{m\/}}, {\it{e\/}} $\div$ {\tt{2}}, {\it{n\/}})\index{crypt})\index{square} ${}${\bf{mod}}${}$ {\it{n\/}} \\ 
{\bf else }({\it{m\/}} $*$ ({\rm{square}}\,({\rm{crypt}}\,({\it{m\/}}, {\it{e\/}} $\div$ {\tt{2}}, {\it{n\/}})\index{crypt})\index{square} ${}${\bf{mod}}${}$ {\it{n\/}})) ${}${\bf{mod}}${}$ {\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-mod-1 \\ \index{times-mod-1}
(({\it{x\/}} $*$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{n\/}})) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ (({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-mod-2 \\ \index{times-mod-2}
(({\it{a\/}} $*$ ({\it{b\/}} $*$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{n\/}}))) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ (({\it{a\/}} $*$ {\it{b\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-correct \\ \index{crypt-correct}
({\it{n\/}} $\not=$ {\tt{1}}) $\rightarrow$ ({\rm{crypt}}\,({\it{m\/}}, {\it{e\/}}, {\it{n\/}})\index{crypt} $=$ ({\rm{exp}}\,({\it{m\/}}, {\it{e\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{n\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-mod-3 \\ \index{times-mod-3}
((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ (({\it{a\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-exp-lemma \\ \index{remainder-exp-lemma}
\=\+(({\it{y\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ ({\it{z\/}} ${}${\bf{mod}}${}$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ (({\it{x\/}} $*$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{a\/}})) $=$ {\bf{t}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-exp \\ \index{remainder-exp}
({\rm{exp}}\,({\it{a\/}} ${}${\bf{mod}}${}$ {\it{n\/}}, {\it{i\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ ({\rm{exp}}\,({\it{a\/}}, {\it{i\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-mod-is-1 \\ \index{exp-mod-is-1}
(({\rm{exp}}\,({\it{m\/}}, {\it{j\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}}) $\rightarrow$ (({\rm{exp}}\,({\it{m\/}}, {\it{i\/}} $*$ {\it{j\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pdifference} \\  
\=\+{\rm{pdifference}}\,({\it{a\/}}, {\it{b\/}})\index{pdifference} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\it{b\/}} $-$ {\it{a\/}} \\ 
{\bf else }{\it{a\/}} $-$ {\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-distributes-over-pdifference \\ \index{times-distributes-over-pdiffere!nce}
({\it{m\/}} $*$ {\rm{pdifference}}\,({\it{a\/}}, {\it{b\/}})\index{pdifference}) $=$ {\rm{pdifference}}\,({\it{m\/}} $*$ {\it{a\/}}, {\it{m\/}} $*$ {\it{b\/}})\index{pdifference}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-mods-trick-1 \\ \index{equal-mods-trick-1}
(({\rm{pdifference}}\,({\it{a\/}}, {\it{b\/}})\index{pdifference} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $=$ {\bf{t}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-mods-trick-2 \\ \index{equal-mods-trick-2}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $\rightarrow$ (({\rm{pdifference}}\,({\it{a\/}}, {\it{b\/}})\index{pdifference} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}})
\end{tabbing}

\noindent{\sc Event}:   Disable pdifference.

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  prime-key-trick \\ \index{prime-key-trick}
\=\+(\=\+((({\it{m\/}} $*$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{m\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{p\/}})\index{prime})\- \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) $=$ {\bf{t}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  product-divides-lemma \\ \index{product-divides-lemma}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{y\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  product-divides \\ \index{product-divides}
\=\+(\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{q\/}}) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\it{q\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ ({\it{p\/}} $*$ {\it{q\/}})) $=$ {\tt{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  thm-53-specialized-to-primes \\ \index{thm-53-specialized-to-primes}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\it{q\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{q\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{q\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{p\/}} $*$ {\it{q\/}})) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ ({\it{p\/}} $*$ {\it{q\/}})))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  corollary-53 \\ \index{corollary-53}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\it{q\/}}) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{q\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{q\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $<$ ({\it{p\/}} $*$ {\it{q\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{p\/}} $*$ {\it{q\/}})) $=$ {\it{b\/}}) $=$ {\bf{t}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  thm-55-specialized-to-primes \\ \index{thm-55-specialized-to-primes}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{m\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\it{m\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$=$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{p\/}})))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  corollary-55 \\ \index{corollary-55}
\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{m\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}})) \\ 
$=$$\;\;\;\;$((({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $\vee$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{all-distinct} \\  
\=\+{\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{car}}\,({\it{l\/}}) $\not\in$ {\rm{cdr}}\,({\it{l\/}})) $\wedge$ {\rm{all-distinct}}\,({\rm{cdr}}\,({\it{l\/}}))\index{all-distinct}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{all-lesseqp} \\  
\=\+{\rm{all-lesseqp}}\,({\it{l\/}}, {\it{n\/}})\index{all-lesseqp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\it{n\/}} $\not<$ {\rm{car}}\,({\it{l\/}})) $\wedge$ {\rm{all-lesseqp}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{n\/}})\index{all-lesseqp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{all-non-zerop} \\  
\=\+{\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }({\rm{car}}\,({\it{l\/}}) $\not\simeq {\tt{0}}$) $\wedge$ {\rm{all-non-zerop}}\,({\rm{cdr}}\,({\it{l\/}}))\index{all-non-zerop}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{positives} \\  
\=\+{\rm{positives}}\,({\it{n\/}})\index{positives} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\it{n\/}}, {\rm{positives}}\,({\it{n\/}} $-\;1$)\index{positives})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  listp-positives \\ \index{listp-positives}
{\rm{listp}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}) $=$ ({\it{n\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  car-positives \\ \index{car-positives}
\=\+{\rm{car}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-positives \\ \index{member-positives}
\=\+({\it{x\/}} $\in$ {\rm{positives}}\,({\it{n\/}})\index{positives}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{x\/}} $<$ ($1\;+$ {\it{n\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-delete \\ \index{all-non-zerop-delete}
{\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} $\rightarrow$ {\rm{all-non-zerop}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{all-non-zerop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-delete \\ \index{all-distinct-delete}
{\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} $\rightarrow$ {\rm{all-distinct}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{all-distinct}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pigeon-hole-principle-lemma-1 \\ \index{pigeon-hole-principle-lemma-1}
\=\+({\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} $\wedge$ {\rm{all-lesseqp}}\,({\it{l\/}}, $1\;+$ {\it{n\/}})\index{all-lesseqp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{all-lesseqp}}\,({\rm{delete}}\,($1\;+$ {\it{n\/}}, {\it{l\/}})\index{delete}, {\it{n\/}})\index{all-lesseqp}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pigeon-hole-principle-lemma-2 \\ \index{pigeon-hole-principle-lemma-2}
((($1\;+$ {\it{n\/}}) $\not\in$ {\it{x\/}}) $\wedge$ {\rm{all-lesseqp}}\,({\it{x\/}}, $1\;+$ {\it{n\/}})\index{all-lesseqp}) $\rightarrow$ {\rm{all-lesseqp}}\,({\it{x\/}}, {\it{n\/}})\index{all-lesseqp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-member \\ \index{perm-member}
({\rm{perm}}\,({\it{a\/}}, {\it{b\/}})\index{perm} $\wedge$ ({\it{x\/}} $\in$ {\it{a\/}})) $\rightarrow$ ({\it{x\/}} $\in$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pigeon-hole-induction} \\  
\=\+{\rm{pigeon-hole-induction}}\,({\it{l\/}})\index{pigeon-hole-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{length}}\,({\it{l\/}})\index{length} $\in$ {\it{l\/}} \\ 
{\bf then }{\rm{pigeon-hole-induction}}\,({\rm{delete}}\,({\rm{length}}\,({\it{l\/}})\index{length}, {\it{l\/}})\index{delete})\index{pigeon-hole-induction} \\ 
{\bf else }{\rm{pigeon-hole-induction}}\,({\rm{cdr}}\,({\it{l\/}}))\index{pigeon-hole-induction}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pigeon-hole-principle \\ \index{pigeon-hole-principle}
\=\+({\rm{all-non-zerop}}\,({\it{l\/}})\index{all-non-zerop} $\wedge$ {\rm{all-distinct}}\,({\it{l\/}})\index{all-distinct} $\wedge$ {\rm{all-lesseqp}}\,({\it{l\/}}, {\rm{length}}\,({\it{l\/}})\index{length})\index{all-lesseqp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\rm{positives}}\,({\rm{length}}\,({\it{l\/}})\index{length})\index{positives}, {\it{l\/}})\index{perm}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  perm-times-list \\ \index{perm-times-list}
{\rm{perm}}\,({\it{l1\/}}, {\it{l2\/}})\index{perm} $\rightarrow$ ({\rm{times-list}}\,({\it{l1\/}})\index{times-list} $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-list-positives \\ \index{times-list-positives}
{\rm{times-list}}\,({\rm{positives}}\,({\it{n\/}})\index{positives})\index{times-list} $=$ {\rm{fact}}\,({\it{n\/}})\index{fact}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-list-equal-fact \\ \index{times-list-equal-fact}
{\rm{perm}}\,({\rm{positives}}\,({\it{n\/}})\index{positives}, {\it{l\/}})\index{perm} $\rightarrow$ ({\rm{times-list}}\,({\it{l\/}})\index{times-list} $=$ {\rm{fact}}\,({\it{n\/}})\index{fact})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-fact \\ \index{prime-fact}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ ({\it{n\/}} $<$ {\it{p\/}})) $\rightarrow$ (({\rm{fact}}\,({\it{n\/}})\index{fact} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{s} \\  
\=\+{\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(({\it{m\/}} $*$ {\it{n\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}, {\rm{s}}\,({\it{n\/}} $-\;1$, {\it{m\/}}, {\it{p\/}})\index{s})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-times-list-s \\ \index{remainder-times-list-s}
({\rm{times-list}}\,({\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s})\index{times-list} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ (({\rm{fact}}\,({\it{n\/}})\index{fact} $*$ {\rm{exp}}\,({\it{m\/}}, {\it{n\/}})\index{exp}) ${}${\bf{mod}}${}$ {\it{p\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-s-lemma \\ \index{all-distinct-s-lemma}
\=\+({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{n1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{n2\/}} $<$ {\it{n1\/}}) $\wedge$ ({\it{n1\/}} $<$ {\it{p\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{m\/}} $*$ {\it{n1\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $\not\in$ {\rm{s}}\,({\it{n2\/}}, {\it{m\/}}, {\it{p\/}})\index{s})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-distinct-s \\ \index{all-distinct-s}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{n\/}} $<$ {\it{p\/}})) $\rightarrow$ {\rm{all-distinct}}\,({\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s})\index{all-distinct}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-non-zerop-s \\ \index{all-non-zerop-s}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}}) $\wedge$ ({\it{n\/}} $<$ {\it{p\/}})) $\rightarrow$ {\rm{all-non-zerop}}\,({\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s})\index{all-non-zerop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  all-lesseqp-s \\ \index{all-lesseqp-s}
({\it{p\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ {\rm{all-lesseqp}}\,({\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s}, {\it{p\/}} $-\;1$)\index{all-lesseqp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-s \\ \index{length-s}
{\rm{length}}\,({\rm{s}}\,({\it{n\/}}, {\it{m\/}}, {\it{p\/}})\index{s})\index{length} $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  fermat-thm \\ \index{fermat-thm}
({\rm{prime}}\,({\it{p\/}})\index{prime} $\wedge$ (({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $\not=$ {\tt{0}})) $\rightarrow$ (({\rm{exp}}\,({\it{m\/}}, {\it{p\/}} $-\;1$)\index{exp} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-inverts-step-1 \\ \index{crypt-inverts-step-1}
{\rm{prime}}\,({\it{p\/}})\index{prime} $\rightarrow$ ((({\it{m\/}} $*$ {\rm{exp}}\,({\it{m\/}}, {\it{k\/}} $*$ ({\it{p\/}} $-\;1$))\index{exp}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-inverts-step-1a \\ \index{crypt-inverts-step-1a}
\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\rightarrow$$\;\;\;\;$((({\it{m\/}} $*$ {\rm{exp}}\,({\it{m\/}}, {\it{k\/}} $*$ ({\it{p\/}} $-\;1$) $*$ ({\it{q\/}} $-\;1$))\index{exp}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ ({\it{m\/}} ${}${\bf{mod}}${}$ {\it{p\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-inverts-step-1b \\ \index{crypt-inverts-step-1b}
\=\+{\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\rightarrow$$\;\;\;\;$((({\it{m\/}} $*$ {\rm{exp}}\,({\it{m\/}}, {\it{k\/}} $*$ ({\it{p\/}} $-\;1$) $*$ ({\it{q\/}} $-\;1$))\index{exp}) ${}${\bf{mod}}${}$ {\it{q\/}}) $=$ ({\it{m\/}} ${}${\bf{mod}}${}$ {\it{q\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-inverts-step-2 \\ \index{crypt-inverts-step-2}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\it{q\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $<$ ({\it{p\/}} $*$ {\it{q\/}})) \\ 
$\wedge$$\;\;\;\;$(({\it{ed\/}} ${}${\bf{mod}}${}$ (({\it{p\/}} $-\;1$) $*$ ({\it{q\/}} $-\;1$))) $=$ {\tt{1}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{exp}}\,({\it{m\/}}, {\it{ed\/}})\index{exp} ${}${\bf{mod}}${}$ ({\it{p\/}} $*$ {\it{q\/}})) $=$ {\it{m\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crypt-inverts \\ \index{crypt-inverts}
\=\+(\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;${\rm{prime}}\,({\it{q\/}})\index{prime} \\ 
$\wedge$$\;\;\;\;$({\it{p\/}} $\not=$ {\it{q\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $=$ ({\it{p\/}} $*$ {\it{q\/}})) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{m\/}} $<$ {\it{n\/}}) \\ 
$\wedge$$\;\;\;\;$((({\it{e\/}} $*$ {\it{d\/}}) ${}${\bf{mod}}${}$ (({\it{p\/}} $-\;1$) $*$ ({\it{q\/}} $-\;1$))) $=$ {\tt{1}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{crypt}}\,({\rm{crypt}}\,({\it{m\/}}, {\it{e\/}}, {\it{n\/}})\index{crypt}, {\it{d\/}}, {\it{n\/}})\index{crypt} $=$ {\it{m\/}})\-
\end{tabbing}


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

\addvspace{18pt}

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