\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}; From Matt Kaufmann, ICSCA, Univ. of Texas, 2/23/87

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"arith"}}.

\addvspace{18pt}

\begin{verbatim}; The first definition is one
; whose only purpose is to specify an induction scheme later.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{my-ind} \\  
\=\+{\rm{my-ind}}\,({\it{x\/}}, {\it{y\/}})\index{my-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $=$ {\tt{0}})\-$\;\;${\bf then }{\rm{my-ind}}\,({\it{x\/}} $\div$ {\tt{2}}, {\it{y\/}} $\div$ {\tt{2}})\index{my-ind} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Here's a lemma that I found useful in a proof below.  The
; theorem-prover proves this automatically.  I immediately
; disable it because I'm afraid that automatic use of this lemma
; may cause infinite looping by the rewriter.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  move-consts-to-front \\ \index{move-consts-to-front}
(({\it{b\/}} $*$ {\it{c\/}}) $*$ ({\it{d\/}} $*$ {\it{e\/}})) $=$ (({\it{b\/}} $*$ {\it{d\/}}) $*$ ({\it{c\/}} $*$ {\it{e\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable move-consts-to-front.

\addvspace{18pt}

\begin{verbatim}; Here's a lemma that I found useful in the proof of the main
; result.  Though I don't remember for sure, I think that I
; discovered this lemma and the one above it in the course of
; trying to give an interactive proof of the main result.
; However, the one following it was (I'll guess) discovered in
; the course of trying to carry out the proof of the main lemma,
; REMAINDER-TIMES-ODDS, below.  That lemma, in turn, has an
; immediate corollary the one just below it, namely
; DIVIDES-2-SQUARE, and I'm sure you'll see why I could use that
; one.

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

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

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

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

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

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

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