\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[]


\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-right-id2 \\ \index{plus-right-id2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $+$ {\it{y\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
\=\+({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }$1\;+$ ({\it{x\/}} $+$ {\it{y\/}}) \\ 
{\bf else }$1\;+$ {\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-plus \\ \index{commutativity2-of-plus}
({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{z\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}} $+$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity-of-plus \\ \index{commutativity-of-plus}
({\it{x\/}} $+$ {\it{y\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-plus \\ \index{associativity-of-plus}
(({\it{x\/}} $+$ {\it{y\/}}) $+$ {\it{z\/}}) $=$ ({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-equal-0 \\ \index{plus-equal-0}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ {\tt{0}}) $=$ (({\it{a\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-x-x \\ \index{difference-x-x}
({\it{x\/}} $-$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus \\ \index{difference-plus}
((({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})) $\wedge$ ((({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  difference-0 \\ \index{difference-0}
({\it{y\/}} $\not<$ {\it{x\/}}) $\rightarrow$ (({\it{x\/}} $-$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-difference-0 \\ \index{equal-difference-0}
({\tt{0}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ ({\it{y\/}} $\not<$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-cancellation-0 \\ \index{difference-cancellation-0}
({\it{x\/}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-cancellation-1 \\ \index{difference-cancellation-1}
\=\+(({\it{x\/}} $-$ {\it{y\/}}) $=$ ({\it{z\/}} $-$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{z\/}} \\ 
{\bf elseif }{\it{z\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{x\/}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{z\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-zero2 \\ \index{times-zero2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-plus \\ \index{distributivity-of-times-over-pl!us}
({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
\=\+({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity-of-times \\ \index{commutativity-of-times}
({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-times \\ \index{commutativity2-of-times}
({\it{x\/}} $*$ {\it{y\/}} $*$ {\it{z\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}} $*$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-times \\ \index{associativity-of-times}
(({\it{x\/}} $*$ {\it{y\/}}) $*$ {\it{z\/}}) $=$ ({\it{x\/}} $*$ {\it{y\/}} $*$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-times-0 \\ \index{equal-times-0}
(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{exp} \\  
\=\+{\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{i\/}} $*$ {\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-plus \\ \index{exp-plus}
{\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $+$ {\it{k\/}})\index{exp} $=$ ({\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} $*$ {\rm{exp}}\,({\it{i\/}}, {\it{k\/}})\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-lessp \\ \index{equal-lessp}
\=\+(({\it{x\/}} $<$ {\it{y\/}}) $=$ {\it{z\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} $=$ {\it{z\/}} \\ 
{\bf else }{\bf{f}} $=$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-elim \\ \index{difference-elim}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not<$ {\it{x\/}})) $\rightarrow$ (({\it{x\/}} $+$ ({\it{y\/}} $-$ {\it{x\/}})) $=$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-quotient \\ \index{remainder-quotient}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-wrt-1 \\ \index{remainder-wrt-1}
({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{1}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-wrt-12 \\ \index{remainder-wrt-12}
({\it{x\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-remainder2 \\ \index{lessp-remainder2}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}}) $=$ ({\it{y\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-x-x \\ \index{remainder-x-x}
({\it{x\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  lessp-times-1 \\ \index{lessp-times-1}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{i\/}} $*$ {\it{j\/}}) $\not<$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times-2 \\ \index{lessp-times-2}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{j\/}} $*$ {\it{i\/}}) $\not<$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-quotient1 \\ \index{lessp-quotient1}
(({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{i\/}}) $=$ (({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{j\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{j\/}} $\not=$ {\tt{1}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-remainder1 \\ \index{lessp-remainder1}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{x\/}}) $=$ (({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not<$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus1 \\ \index{difference-plus1}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus2 \\ \index{difference-plus2}
(({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus-cancelation \\ \index{difference-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-difference \\ \index{times-difference}
({\it{x\/}} $*$ ({\it{c\/}} $-$ {\it{w\/}})) $=$ (({\it{c\/}} $*$ {\it{x\/}}) $-$ ({\it{w\/}} $*$ {\it{x\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  divides-times \\ \index{divides-times}
(({\it{x\/}} $*$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus3 \\ \index{difference-plus3}
(({\it{b\/}} $+$ {\it{a\/}} $+$ {\it{c\/}}) $-$ {\it{a\/}}) $=$ ({\it{b\/}} $+$ {\it{c\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-add1-cancellation \\ \index{difference-add1-cancellation}
(($1\;+$ ({\it{y\/}} $+$ {\it{z\/}})) $-$ {\it{z\/}}) $=$ ($1\;+$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-add1 \\ \index{remainder-add1}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}})) $\rightarrow$ ((($1\;+$ ({\it{x\/}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{y\/}}) $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite1 \\ \index{divides-plus-rewrite1}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite2 \\ \index{divides-plus-rewrite2}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite \\ \index{divides-plus-rewrite}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus-cancelation \\ \index{lessp-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $<$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $<$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite-commuted \\ \index{divides-plus-rewrite-commuted}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{y\/}} $+$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  euclid \\ \index{euclid}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{y\/}} $-$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times-cancellation \\ \index{lessp-times-cancellation}
(({\it{x\/}} $*$ {\it{z\/}}) $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus-cancellation3 \\ \index{lessp-plus-cancellation3}
({\it{y\/}} $<$ ({\it{x\/}} $+$ {\it{y\/}})) $=$ ({\it{x\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times1 \\ \index{quotient-times1}
\=\+(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{divides}}\,({\it{x\/}}, {\it{y\/}})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $=$ {\it{y\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-lessp \\ \index{quotient-lessp}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} $\div$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  times-id-iff-1 \\ \index{times-id-iff-1}
({\it{z\/}} $=$ ({\it{w\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{z\/}} $=$ {\tt{0}}) $\vee$ ({\it{w\/}} $=$ {\tt{1}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  greatereqpr-lessp \\ \index{greatereqpr-lessp}
{\rm{greatereqpr}}\,({\it{x\/}}, {\it{y\/}})\index{greatereqpr} $=$ ({\it{x\/}} $\not<$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  greatereqpr-remainder \\ \index{greatereqpr-remainder}
(({\it{z\/}} $\not=$ ($1\;+$ {\it{v\/}})) $\wedge$ {\rm{divides}}\,({\it{z\/}}, $1\;+$ {\it{v\/}})\index{divides}) $\rightarrow$ {\rm{greatereqpr}}\,({\it{v\/}}, {\it{z\/}})\index{greatereqpr}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-times1 \\ \index{divides-times1}
({\it{a\/}} $=$ ({\it{z\/}} $*$ {\it{y\/}})) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-identity1 \\ \index{times-identity1}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{y\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}})) $\rightarrow$ ({\it{x\/}} $\not=$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-identity \\ \index{times-identity}
({\it{x\/}} $=$ ({\it{x\/}} $*$ {\it{y\/}})) $=$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-divides \\ \index{quotient-divides}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $\not=$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times \\ \index{remainder-times}
(({\it{y\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times \\ \index{quotient-times}
\=\+(({\it{y\/}} $*$ {\it{x\/}}) $\div$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  distributivity-of-divides \\ \index{distributivity-of-divides}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{divides}}\,({\it{a\/}}, {\it{w\/}})\index{divides}) $\rightarrow$ (({\it{c\/}} $*$ ({\it{w\/}} $\div$ {\it{a\/}})) $=$ (({\it{c\/}} $*$ {\it{w\/}}) $\div$ {\it{a\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  if-times-then-divides \\ \index{if-times-then-divides}
(({\it{c\/}} $\not\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{c\/}}, {\it{x\/}})\index{divides})) $\rightarrow$ (({\it{c\/}} $*$ {\it{y\/}}) $\not=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-equal-1 \\ \index{times-equal-1}
\=\+(({\it{a\/}} $*$ {\it{b\/}}) $=$ {\tt{1}}) \\ 
$=$$\;\;\;\;$(\=\+({\it{a\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} $-\;1$) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{b\/}} $-\;1$) $=$ {\tt{0}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  divides-implies-times \\ \index{divides-implies-times}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{a\/}} $*$ {\it{c\/}}) $=$ {\it{b\/}})) $\rightarrow$ (({\it{c\/}} $=$ ({\it{b\/}} $\div$ {\it{a\/}})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-1 \\ \index{difference-1}
({\it{x\/}} $-$ {\tt{1}}) $=$ ({\it{x\/}} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-2 \\ \index{difference-2}
(($1\;+$ ($1\;+$ {\it{x\/}})) $-$ {\tt{2}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  half-plus \\ \index{half-plus}
(({\it{x\/}} $+$ {\it{x\/}} $+$ {\it{y\/}}) $\div$ {\tt{2}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $\div$ {\tt{2}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-1 \\ \index{times-1}
({\tt{1}} $*$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-of-0 \\ \index{exp-of-0}
\=\+{\rm{exp}}\,({\tt{0}}, {\it{k\/}})\index{exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-of-1 \\ \index{exp-of-1}
{\rm{exp}}\,({\tt{1}}, {\it{k\/}})\index{exp} $=$ {\tt{1}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-by-0 \\ \index{exp-by-0}
{\rm{exp}}\,({\it{x\/}}, {\tt{0}})\index{exp} $=$ {\tt{1}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-times \\ \index{exp-times}
{\rm{exp}}\,({\it{i\/}} $*$ {\it{j\/}}, {\it{k\/}})\index{exp} $=$ ({\rm{exp}}\,({\it{i\/}}, {\it{k\/}})\index{exp} $*$ {\rm{exp}}\,({\it{j\/}}, {\it{k\/}})\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-exp \\ \index{exp-exp}
{\rm{exp}}\,({\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp}, {\it{k\/}})\index{exp} $=$ {\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $*$ {\it{k\/}})\index{exp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-times-1 \\ \index{remainder-plus-times-1}
(({\it{x\/}} $+$ ({\it{i\/}} $*$ {\it{j\/}})) ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-times-2 \\ \index{remainder-plus-times-2}
(({\it{x\/}} $+$ ({\it{j\/}} $*$ {\it{i\/}})) ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-1 \\ \index{remainder-times-1}
(({\it{b\/}} $*$ {\it{a\/}} $*$ {\it{c\/}}) ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-1 \\ \index{remainder-of-1}
\=\+({\tt{1}} ${}${\bf{mod}}${}$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  equal-length-0 \\ \index{equal-length-0}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}}) $=$ ({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-difference-times \\ \index{remainder-difference-times}
((({\it{p\/}} $*$ {\it{x\/}}) $-$ ({\it{p\/}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-remainder-divisor \\ \index{lessp-remainder-divisor}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}})
\end{tabbing}


\noindent{\sc Event}:   Make the library {\tt{"arith"}}.

\addvspace{18pt}

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