\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 Computational Logic, Inc.  All Rights Reserved.

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

 NO WARRANTY

 Computational Logic, Inc. 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 Computational Logic, Inc. 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.
|#

; William R. Bevier, Matt Kaufmann, and Matt Wilding

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

\addvspace{18pt}

\begin{verbatim};; Jan 91 - some additional facts mostly having to do with GCD
;; added by MMW

;; Oct 90 - modified by MMW to eliminate theories

;; Tue Sep 26 10:20:45 1989, from ~wilding/numerical/newnat.events

;; NATURALS Theory

;; Created by Bill Bevier 1988 (see CLI internal note 057)

;; Modifications by Bill Bevier and Matt Wilding (9/89) including
;; adding some new metalemmas for times, reorganizing the theories,
;; removing some extraneous lemmas, and removing dependence upon
;; other theories (by adding the pertinent lemmas).

;; This script requires the bags theory

;; This script sets up a theory for the NATURALS with the following subtheories
;; ADDITION
;; MULTIPLICATION
;; REMAINDER
;; QUOTIENT
;; EXPONENTIATION 
;; LOGS
;; GCDS

;; The theories of EXPONENTIATION, LOGS, and GCDS still need a lot of work

; --------------------------------------------------------------------------------
; ARITHMETIC
; --------------------------------------------------------------------------------

; -------------------- PLUS & DIFFERENCE --------------------

; ---------- EQUAL ----------

\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-plus-0 \\ \index{equal-plus-0}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ {\tt{0}}) $=$ (({\it{a\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$))
\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}


\noindent{\sc Event}:   Disable plus-cancellation.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  difference-cancellation \\ \index{difference-cancellation}
\=\+(({\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}


\noindent{\sc Event}:   Disable difference-cancellation.

\addvspace{18pt}

\begin{verbatim}; ---------- PLUS ----------

\end{verbatim}\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}:  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}:  plus-zero-arg2 \\ \index{plus-zero-arg2}
({\it{y\/}} $\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $+$ {\it{y\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1-arg1 \\ \index{plus-add1-arg1}
(($1\;+$ {\it{a\/}}) $+$ {\it{b\/}}) $=$ ($1\;+$ ({\it{a\/}} $+$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plus-add1-arg2 \\ \index{plus-add1-arg2}
\=\+({\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}:  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-difference-arg1 \\ \index{plus-difference-arg1}
\=\+(({\it{a\/}} $-$ {\it{b\/}}) $+$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }({\it{a\/}} $+$ {\it{c\/}}) $-$ {\it{b\/}} \\ 
{\bf else }{\tt{0}} $+$ {\it{c\/}}$\;${\bf  endif}\-\-
\end{tabbing}
       
\begin{tabbing}{\sc Theorem}:  plus-difference-arg2 \\ \index{plus-difference-arg2}
\=\+({\it{a\/}} $+$ ({\it{b\/}} $-$ {\it{c\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{c\/}} $<$ {\it{b\/}}$\;\;${\bf then }({\it{a\/}} $+$ {\it{b\/}}) $-$ {\it{c\/}} \\ 
{\bf else }{\it{a\/}} $+$ {\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; ---------- DIFFERENCE-PLUS cancellation rules ----------
;
; Here are the basic canonicalization rules for differences of sums. These
; are subsumed by the meta lemmas and are therefore globally disabled.
; They are here merely to prove the meta lemmas.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  difference-plus-cancellation-proof \\ \index{difference-plus-cancellation-pr!oof}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}


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


\noindent{\sc Event}:   Disable difference-plus-cancellation.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-plus-plus-cancellation-proof \\ \index{difference-plus-plus-cancellati!on-proof}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-plus-plus-cancellation \\ \index{difference-plus-plus-cancellati!on}
\=\+((({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{y\/}} $+$ {\it{x\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{z\/}} $+$ {\it{x\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{y\/}} $+$ {\it{x\/}}) $-$ ({\it{z\/}} $+$ {\it{x\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable difference-plus-plus-cancellation.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-plus-plus-cancellation-hack \\ \index{difference-plus-plus-cancellati!on-hack}
(({\it{w\/}} $+$ {\it{x\/}} $+$ {\it{a\/}}) $-$ ({\it{y\/}} $+$ {\it{z\/}} $+$ {\it{a\/}})) $=$ (({\it{w\/}} $+$ {\it{x\/}}) $-$ ({\it{y\/}} $+$ {\it{z\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable difference-plus-plus-cancellation-hack.

\addvspace{18pt}

\begin{verbatim}; Here are a few more facts about difference needed to prove the meta lemmas.
; These are disabled here. We re-prove them after the proof of the meta
; lemmas so that they will fire before the meta lemmas in subsequent proofs.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  diff-sub1-arg2 \\ \index{diff-sub1-arg2}
\=\+({\it{a\/}} $-$ ({\it{b\/}} $-\;1$)) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{a\/}}) \\ 
{\bf elseif }{\it{a\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ ({\it{a\/}} $-$ {\it{b\/}})$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable diff-sub1-arg2.

\addvspace{18pt}

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


\begin{tabbing}{\sc Theorem}:  diff-diff-arg2 \\ \index{diff-diff-arg2}
\=\+({\it{a\/}} $-$ ({\it{b\/}} $-$ {\it{c\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{c\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{a\/}}) \\ 
{\bf else }({\it{a\/}} $+$ {\it{c\/}}) $-$ {\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim}; diff-diff-diff should be removed, but since the hack lemmas for
; correctness-of-cancel-difference-plus are designed for it, we'll
; keep it around.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  diff-diff-diff \\ \index{diff-diff-diff}
\=\+(({\it{b\/}} $\leq$ {\it{a\/}}) $\wedge$ ({\it{d\/}} $\leq$ {\it{c\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $-$ {\it{b\/}}) $-$ ({\it{c\/}} $-$ {\it{d\/}})) $=$ (({\it{a\/}} $+$ {\it{d\/}}) $-$ ({\it{b\/}} $+$ {\it{c\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable diff-diff-diff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  difference-lessp-arg1 \\ \index{difference-lessp-arg1}
({\it{a\/}} $<$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} $-$ {\it{b\/}}) $=$ {\tt{0}})
\end{tabbing}


\noindent{\sc Event}:   Disable difference-lessp-arg1.

\addvspace{18pt}

\begin{verbatim}; --------------------------------------------------------------------------------
; Meta Lemmas to Cancel PLUS and DIFFERENCE expressions
; --------------------------------------------------------------------------------

; ---------- PLUS-TREE and PLUS-FRINGE ----------

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{plus-fringe} \\  
\=\+{\rm{plus-fringe}}\,({\it{x\/}})\index{plus-fringe} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
{\bf then }{\rm{append}}\,({\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{plus-tree} \\  
\=\+{\rm{plus-tree}}\,({\it{l\/}})\index{plus-tree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{'}}{\tt{'}}{\tt{0}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{l\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{fix}}, {\rm{car}}\,({\it{l\/}})) \\ 
{\bf elseif }{\rm{cddr}}\,({\it{l\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{plus}}, {\rm{car}}\,({\it{l\/}}), {\rm{cadr}}\,({\it{l\/}})) \\ 
{\bf else }{\rm{list}}\,({\tt{'}}{\tt{plus}}, {\rm{car}}\,({\it{l\/}}), {\rm{plus-tree}}\,({\rm{cdr}}\,({\it{l\/}}))\index{plus-tree})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-eval\$-plus \\ \index{numberp-eval\$-plus}
({\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}})) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}


\noindent{\sc Event}:   Disable numberp-eval\$-plus.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  numberp-eval\$-plus-tree \\ \index{numberp-eval\$-plus-tree}
{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{l\/}})\index{plus-tree}, {\it{a\/}}) $\in\;${\bf{N}}${}$
\end{tabbing}


\noindent{\sc Event}:   Disable numberp-eval\$-plus-tree.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  member-implies-plus-tree-greatereqp \\ \index{member-implies-plus-tree-greate!reqp}
({\it{x\/}} $\in$ {\it{y\/}}) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}}) $\not<$ {\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable member-implies-plus-tree-greatereqp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-tree-delete \\ \index{plus-tree-delete}
\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete})\index{plus-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}}) $-$ {\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) \\ 
{\bf else }{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}})$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable plus-tree-delete.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  subbagp-implies-plus-tree-greatereqp \\ \index{subbagp-implies-plus-tree-greate!reqp}
{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}}) $\not<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{x\/}})\index{plus-tree}, {\it{a\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable subbagp-implies-plus-tree-greatereqp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-tree-bagdiff \\ \index{plus-tree-bagdiff}
\=\+{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\rm{bagdiff}}\,({\it{y\/}}, {\it{x\/}})\index{bagdiff})\index{plus-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}}) $-$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{x\/}})\index{plus-tree}, {\it{a\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable plus-tree-bagdiff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  numberp-eval\$-bridge \\ \index{numberp-eval\$-bridge}
({\rm{eval\$}}\,({\bf{t}}, {\it{z\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{x\/}})\index{plus-tree}, {\it{a\/}})) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\it{z\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}


\noindent{\sc Event}:   Disable numberp-eval\$-bridge.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  bridge-to-subbagp-implies-plus-tree-greatereqp \\ \index{bridge-to-subbagp-implies-plus-t!ree-greatereqp}
\=\+(\=\+{\rm{subbagp}}\,({\it{y\/}}, {\rm{plus-fringe}}\,({\it{z\/}})\index{plus-fringe})\index{subbagp} \\ 
$\wedge$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{z\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\rm{plus-fringe}}\,({\it{z\/}})\index{plus-fringe})\index{plus-tree}, {\it{a\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{eval\$}}\,({\bf{t}}, {\it{z\/}}, {\it{a\/}}) $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}})) $=$ {\bf{f}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable bridge-to-subbagp-implies-plus-tree-greatereqp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-plus-tree-append \\ \index{eval\$-plus-tree-append}
\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{plus-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{x\/}})\index{plus-tree}, {\it{a\/}}) $+$ {\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\it{y\/}})\index{plus-tree}, {\it{a\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-plus-tree-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-tree-plus-fringe \\ \index{plus-tree-plus-fringe}
{\rm{eval\$}}\,({\bf{t}}, {\rm{plus-tree}}\,({\rm{plus-fringe}}\,({\it{x\/}})\index{plus-fringe})\index{plus-tree}, {\it{a\/}}) $=$ {\rm{fix}}\,({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable plus-tree-plus-fringe.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  member-implies-numberp \\ \index{member-implies-numberp}
(({\it{c\/}} $\in$ {\rm{plus-fringe}}\,({\it{x\/}})\index{plus-fringe}) $\wedge$ ({\rm{eval\$}}\,({\bf{t}}, {\it{c\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}


\noindent{\sc Event}:   Disable member-implies-numberp.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cadr-eval\$-list \\ \index{cadr-eval\$-list}
\=\+({\rm{car}}\,({\rm{eval\$}}\,({\tt{'}}{\tt{list}}, {\it{x\/}}, {\it{a\/}})) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{car}}\,({\it{x\/}}), {\it{a\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{cdr}}\,({\rm{eval\$}}\,({\tt{'}}{\tt{list}}, {\it{x\/}}, {\it{a\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{eval\$}}\,({\tt{'}}{\tt{list}}, {\rm{cdr}}\,({\it{x\/}}), {\it{a\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable cadr-eval\$-list.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-quote \\ \index{eval\$-quote}
{\rm{eval\$}}\,({\bf{t}}, {\rm{cons}}\,({\tt{'}}{\tt{quote}}, {\it{args\/}}), {\it{a\/}}) $=$ {\rm{car}}\,({\it{args\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-quote.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  listp-eval\$ \\ \index{listp-eval\$}
{\rm{listp}}\,({\rm{eval\$}}\,({\tt{'}}{\tt{list}}, {\it{x\/}}, {\it{a\/}})) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable listp-eval\$.

\addvspace{18pt}

\begin{verbatim}; ---------- CANCEL PLUS ----------

; CANCEL-EQUAL-PLUS cancels identical terms in a term which is the equality
; of two sums. For example,
; 
;   (EQUAL (PLUS A B C) (PLUS B D E)) => (EQUAL (PLUS A C) (PLUS D E))
;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cancel-equal-plus} \\  
\=\+{\rm{cancel-equal-plus}}\,({\it{x\/}})\index{cancel-equal-plus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{equal}}) \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree})\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{if}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{numberp}}, {\rm{caddr}}\,({\it{x\/}})), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\rm{plus-tree}}\,({\rm{delete}}\,({\rm{caddr}}\,({\it{x\/}}), {\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe})\index{delete})\index{plus-tree}, \\ 
{\tt{'}}{\tt{'}}{\tt{0}})\-, \\ 
{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\bf{f}}))\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{if}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{numberp}}, {\rm{cadr}}\,({\it{x\/}})), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\tt{'}}{\tt{'}}{\tt{0}}, \\ 
{\rm{plus-tree}}\,({\rm{delete}}\,({\rm{cadr}}\,({\it{x\/}}), {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\index{delete})\index{plus-tree})\-, \\ 
{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\bf{f}}))\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-equal-plus \\ \index{correctness-of-cancel-equal-plu!s}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-equal-plus}}\,({\it{x\/}})\index{cancel-equal-plus}, {\it{a\/}})
\end{tabbing}

\begin{verbatim}; ---------- CANCEL-DIFFERENCE-PLUS ----------

; CANCEL-DIFFERENCE-PLUS cancels identical terms in a term which is the 
; difference of two sums. For example,
; 
;  (DIFFERENCE (PLUS A B C) (PLUS B D E)) => (DIFFERENCE (PLUS A C) (PLUS D E))
;
; Using rewrite rules, we canonicalize terms involving  PLUS and DIFFERENCE 
; to be the DIFFERENCE of two sums. Then CANCEL-DIFFERENCE-PLUS cancels out 
; like terms.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cancel-difference-plus} \\  
\=\+{\rm{cancel-difference-plus}}\,({\it{x\/}})\index{cancel-difference-plus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{difference}}) \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{difference}}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree})\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe})\- \\ 
{\bf then }{\rm{plus-tree}}\,({\rm{delete}}\,({\rm{caddr}}\,({\it{x\/}}), {\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe})\index{delete})\index{plus-tree} \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-$\;\;${\bf then }{\tt{'}}{\tt{'}}{\tt{0}} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-difference-plus \\ \index{correctness-of-cancel-difference!-plus}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-difference-plus}}\,({\it{x\/}})\index{cancel-difference-plus}, {\it{a\/}})
\end{tabbing}

\begin{verbatim}; ---------- DIFFERENCE ----------

; Here are the rules for difference terms which we want to try before
; the meta lemmas. They help canonicalize terms to differences of sums.

\end{verbatim}\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}:  difference-leq-arg1 \\ \index{difference-leq-arg1}
({\it{a\/}} $\leq$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} $-$ {\it{b\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-add1-arg2 \\ \index{difference-add1-arg2}
\=\+({\it{a\/}} $-$ ($1\;+$ {\it{b\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }({\it{a\/}} $-$ {\it{b\/}}) $-\;1$ \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-sub1-arg2 \\ \index{difference-sub1-arg2}
\=\+({\it{a\/}} $-$ ({\it{b\/}} $-\;1$)) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{a\/}}) \\ 
{\bf elseif }{\it{a\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ ({\it{a\/}} $-$ {\it{b\/}})$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  difference-difference-arg2 \\ \index{difference-difference-arg2}
\=\+({\it{a\/}} $-$ ({\it{b\/}} $-$ {\it{c\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{c\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{a\/}}) \\ 
{\bf else }({\it{a\/}} $+$ {\it{c\/}}) $-$ {\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{verbatim}; ---------- LESSP ----------

\end{verbatim}\begin{tabbing}{\sc Theorem}:  lessp-difference-cancellation \\ \index{lessp-difference-cancellation}
\=\+(({\it{a\/}} $-$ {\it{c\/}}) $<$ ({\it{b\/}} $-$ {\it{c\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{c\/}} $\leq$ {\it{a\/}}$\;\;${\bf then }{\it{a\/}} $<$ {\it{b\/}} \\ 
{\bf else }{\it{c\/}} $<$ {\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-difference-cancellation.

\addvspace{18pt}

\begin{verbatim}; CANCEL-LESSP-PLUS cancels LESSP terms whose arguments are sums.
; Examples:
; (LESSP (PLUS A B C) (PLUS A C D)) -> (LESSP (FIX B) (FIX D))
; (LESSP A (PLUS A B))  -> (NOT (ZEROP (FIX B)))
; (LESSP (PLUS A B) A)  -> F

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cancel-lessp-plus} \\  
\=\+{\rm{cancel-lessp-plus}}\,({\it{x\/}})\index{cancel-lessp-plus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{lessp}}) \\ 
{\bf then }\=\+{\bf if }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{lessp}}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree}, \\ 
{\rm{plus-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe}, \\ 
{\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\-\index{bagint})\-\index{bagdiff})\index{plus-tree})\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{plus-fringe})\- \\ 
{\bf then }{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\bf{f}}) \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{x\/}}) $\in$ {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{not}}, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{zerop}}, \\ 
{\rm{plus-tree}}\,({\rm{delete}}\,({\rm{cadr}}\,({\it{x\/}}), {\rm{plus-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{plus-fringe})\index{delete})\index{plus-tree})\-)\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-lessp-plus \\ \index{correctness-of-cancel-lessp-plu!s}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-lessp-plus}}\,({\it{x\/}})\index{cancel-lessp-plus}, {\it{a\/}})
\end{tabbing}



\begin{verbatim}; ---------- TIMES ----------

\end{verbatim}\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 Theorem}:  equal-times-1 \\ \index{equal-times-1}
(({\it{a\/}} $*$ {\it{b\/}}) $=$ {\tt{1}}) $=$ (({\it{a\/}} $=$ {\tt{1}}) $\wedge$ ({\it{b\/}} $=$ {\tt{1}}))
\end{tabbing}

\begin{verbatim};(prove-lemma equal-sub1-times-0 (rewrite)
;       (equal (equal (sub1 (times a b)) 0)
;             (or (zerop a)
;                 (zerop b)
;                 (and (equal a 1) (equal b 1)))))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-sub1-0 \\ \index{equal-sub1-0}
(({\it{x\/}} $-\;1$) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{x\/}} $=$ {\tt{1}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-zero \\ \index{times-zero}
({\it{y\/}} $\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\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{y\/}} $*$ {\it{x\/}}) $=$ ({\it{x\/}} $*$ {\it{y\/}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  times-distributes-over-plus \\ \index{times-distributes-over-plus}
\=\+(({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ {\it{y\/}}) $*$ {\it{z\/}}) $=$ (({\it{x\/}} $*$ {\it{z\/}}) $+$ ({\it{y\/}} $*$ {\it{z\/}})))\-
\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}:  times-distributes-over-difference-proof \\ \index{times-distributes-over-differen!ce-proof}
(({\it{a\/}} $-$ {\it{b\/}}) $*$ {\it{c\/}}) $=$ (({\it{a\/}} $*$ {\it{c\/}}) $-$ ({\it{b\/}} $*$ {\it{c\/}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  times-distributes-over-difference \\ \index{times-distributes-over-differen!ce}
\=\+((({\it{a\/}} $-$ {\it{b\/}}) $*$ {\it{c\/}}) $=$ (({\it{a\/}} $*$ {\it{c\/}}) $-$ ({\it{b\/}} $*$ {\it{c\/}}))) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} $*$ ({\it{b\/}} $-$ {\it{c\/}})) $=$ (({\it{a\/}} $*$ {\it{b\/}}) $-$ ({\it{a\/}} $*$ {\it{c\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-quotient-proof \\ \index{times-quotient-proof}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}})) $\rightarrow$ ((({\it{y\/}} $\div$ {\it{x\/}}) $*$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  lessp-times1-proof \\ \index{lessp-times1-proof}
(({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ (({\it{a\/}} $<$ ({\it{b\/}} $*$ {\it{c\/}})) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times1 \\ \index{lessp-times1}
\=\+(({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $<$ ({\it{b\/}} $*$ {\it{c\/}})) $=$ {\bf{t}}) $\wedge$ (({\it{a\/}} $<$ ({\it{c\/}} $*$ {\it{b\/}})) $=$ {\bf{t}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times2-proof \\ \index{lessp-times2-proof}
(({\it{a\/}} $\leq$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ((({\it{b\/}} $*$ {\it{c\/}}) $<$ {\it{a\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times2 \\ \index{lessp-times2}
\=\+(({\it{a\/}} $\leq$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{b\/}} $*$ {\it{c\/}}) $<$ {\it{a\/}}) $=$ {\bf{f}}) $\wedge$ ((({\it{c\/}} $*$ {\it{b\/}}) $<$ {\it{a\/}}) $=$ {\bf{f}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times3-proof1 \\ \index{lessp-times3-proof1}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\tt{1}} $<$ {\it{b\/}})) $\rightarrow$ ({\it{a\/}} $<$ ({\it{a\/}} $*$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times3-proof2 \\ \index{lessp-times3-proof2}
({\it{a\/}} $<$ ({\it{a\/}} $*$ {\it{b\/}})) $\rightarrow$ (({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\tt{1}} $<$ {\it{b\/}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  lessp-times3 \\ \index{lessp-times3}
\=\+(({\it{a\/}} $<$ ({\it{a\/}} $*$ {\it{b\/}})) $=$ (({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\tt{1}} $<$ {\it{b\/}}))) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} $<$ ({\it{b\/}} $*$ {\it{a\/}})) $=$ (({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\tt{1}} $<$ {\it{b\/}})))\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  lessp-times-cancellation-proof \\ \index{lessp-times-cancellation-proof}
(({\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-times-cancellation1 \\ \index{lessp-times-cancellation1}
\=\+((({\it{x\/}} $*$ {\it{z\/}}) $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{z\/}} $*$ {\it{x\/}}) $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $*$ {\it{z\/}}) $<$ ({\it{z\/}} $*$ {\it{y\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{z\/}} $*$ {\it{x\/}}) $<$ ({\it{z\/}} $*$ {\it{y\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-times-cancellation1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-plus-times-proof \\ \index{lessp-plus-times-proof}
({\it{x\/}} $<$ {\it{a\/}}) $\rightarrow$ ((({\it{x\/}} $+$ ({\it{a\/}} $*$ {\it{b\/}})) $<$ ({\it{a\/}} $*$ {\it{c\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus-times1 \\ \index{lessp-plus-times1}
\=\+((({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) $<$ {\it{b\/}}) $=$ (({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$((({\it{a\/}} $+$ ({\it{c\/}} $*$ {\it{b\/}})) $<$ {\it{b\/}}) $=$ (({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$(((({\it{c\/}} $*$ {\it{b\/}}) $+$ {\it{a\/}}) $<$ {\it{b\/}}) $=$ (({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$(((({\it{b\/}} $*$ {\it{c\/}}) $+$ {\it{a\/}}) $<$ {\it{b\/}}) $=$ (({\it{a\/}} $<$ {\it{b\/}}) $\wedge$ ({\it{c\/}} $\simeq {\tt{0}}$)))\-
\end{tabbing}       

\begin{tabbing}{\sc Theorem}:  lessp-plus-times2 \\ \index{lessp-plus-times2}
\=\+(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{x\/}} $+$ ({\it{a\/}} $*$ {\it{b\/}})) $<$ ({\it{a\/}} $*$ {\it{c\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ ({\it{b\/}} $*$ {\it{a\/}})) $<$ ({\it{a\/}} $*$ {\it{c\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ ({\it{a\/}} $*$ {\it{b\/}})) $<$ ({\it{c\/}} $*$ {\it{a\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ ({\it{b\/}} $*$ {\it{a\/}})) $<$ ({\it{c\/}} $*$ {\it{a\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{a\/}} $*$ {\it{b\/}}) $+$ {\it{x\/}}) $<$ ({\it{a\/}} $*$ {\it{c\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{b\/}} $*$ {\it{a\/}}) $+$ {\it{x\/}}) $<$ ({\it{a\/}} $*$ {\it{c\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{a\/}} $*$ {\it{b\/}}) $+$ {\it{x\/}}) $<$ ({\it{c\/}} $*$ {\it{a\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{b\/}} $*$ {\it{a\/}}) $+$ {\it{x\/}}) $<$ ({\it{c\/}} $*$ {\it{a\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-times \\ \index{lessp-1-times}
\=\+({\tt{1}} $<$ ({\it{a\/}} $*$ {\it{b\/}})) \\ 
$=$$\;\;\;\;$($\neg$ (({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ (({\it{a\/}} $=$ {\tt{1}}) $\wedge$ ({\it{b\/}} $=$ {\tt{1}}))))\-
\end{tabbing}




\begin{verbatim};;; meta lemmas to cancel lessp-times and equal-times expressions
;; examples
;; (lessp (times b (times d a)) (times b (times e (times a f)))) -> 
;;                                            (and (and (not (zerop a)) 
;;                                                      (not (zerop b)))
;;                                                 (lessp (fix d) (times e f)))
;;
;; (equal (times b (times c d)) (times b d))    -> 
;;                                           (or (or (zerop b) (zerop d))
;;                                               (equal (fix c) 1))


\end{verbatim}\begin{tabbing}{\sc Definition}:\index{times-tree} \\  
\=\+{\rm{times-tree}}\,({\it{x\/}})\index{times-tree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{'}}{\tt{'}}{\tt{1}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{fix}}, {\rm{car}}\,({\it{x\/}})) \\ 
{\bf elseif }{\rm{cddr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{times}}, {\rm{car}}\,({\it{x\/}}), {\rm{cadr}}\,({\it{x\/}})) \\ 
{\bf else }{\rm{list}}\,({\tt{'}}{\tt{times}}, {\rm{car}}\,({\it{x\/}}), {\rm{times-tree}}\,({\rm{cdr}}\,({\it{x\/}}))\index{times-tree})$\;${\bf  endif}\-\-
\end{tabbing}
                    
\begin{tabbing}{\sc Definition}:\index{times-fringe} \\  
\=\+{\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
{\bf then }{\rm{append}}\,({\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{or-zerop-tree} \\  
\=\+{\rm{or-zerop-tree}}\,({\it{x\/}})\index{or-zerop-tree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{'}}{\tt{(}}{\tt{false}}{\tt{)}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{car}}\,({\it{x\/}})) \\ 
{\bf elseif }{\rm{cddr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf then }{\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{car}}\,({\it{x\/}})), {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{cadr}}\,({\it{x\/}}))) \\ 
{\bf else }{\rm{list}}\,({\tt{'}}{\tt{or}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{car}}\,({\it{x\/}})), {\rm{or-zerop-tree}}\,({\rm{cdr}}\,({\it{x\/}}))\index{or-zerop-tree})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{and-not-zerop-tree} \\  
\=\+{\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}} \\ 
{\bf elseif }{\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{car}}\,({\it{x\/}}))) \\ 
{\bf else }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{car}}\,({\it{x\/}}))), \\ 
{\rm{and-not-zerop-tree}}\,({\rm{cdr}}\,({\it{x\/}}))\index{and-not-zerop-tree})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-eval\$-times \\ \index{numberp-eval\$-times}
({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}


\noindent{\sc Event}:   Disable numberp-eval\$-times.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  eval\$-times \\ \index{eval\$-times}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-times.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  eval\$-or \\ \index{eval\$-or}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{or}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $\vee$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-or.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-equal \\ \index{eval\$-equal}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{equal}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-equal.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-lessp \\ \index{eval\$-lessp}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{lessp}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-lessp.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  eval\$-quotient \\ \index{eval\$-quotient}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{quotient}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $\div$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})))\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-quotient.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-if \\ \index{eval\$-if}
\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{if}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}})$\;\;${\bf then }{\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}}) \\ 
{\bf else }{\rm{eval\$}}\,({\bf{t}}, {\rm{cadddr}}\,({\it{x\/}}), {\it{a\/}})$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-if.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  numberp-eval\$-times-tree \\ \index{numberp-eval\$-times-tree}
{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $\in\;${\bf{N}}${}$
\end{tabbing}


\noindent{\sc Event}:   Disable numberp-eval\$-times-tree.

\addvspace{18pt}


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

\begin{tabbing}{\sc Theorem}:  infer-equality-from-not-lessp \\ \index{infer-equality-from-not-lessp}
(({\it{a\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{b\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ((({\it{a\/}} $\not<$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $\not<$ {\it{a\/}})) $=$ ({\it{a\/}} $=$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-times-arg1 \\ \index{equal-times-arg1}
({\it{a\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ((({\it{a\/}} $*$ {\it{x\/}}) $=$ ({\it{a\/}} $*$ {\it{y\/}})) $=$ ({\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable equal-times-arg1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-times-bridge \\ \index{equal-times-bridge}
(({\it{a\/}} $*$ {\it{b\/}}) $=$ ({\it{c\/}} $*$ ({\it{a\/}} $*$ {\it{d\/}}))) $=$ (({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\rm{fix}}\,({\it{b\/}}) $=$ ({\it{c\/}} $*$ {\it{d\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable equal-times-bridge.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-times-member \\ \index{eval\$-times-member}
\=\+({\it{e\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\it{e\/}}, {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{delete}}\,({\it{e\/}}, {\it{x\/}})\index{delete})\index{times-tree}, {\it{a\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-times-member.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  zerop-makes-times-tree-zero \\ \index{zerop-makes-times-tree-zero}
\=\+(($\neg$ {\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree}, {\it{a\/}})) $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}) $=$ {\tt{0}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-makes-times-tree-zero.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  or-zerop-tree-is-not-zerop-tree \\ \index{or-zerop-tree-is-not-zerop-tree}
{\rm{eval\$}}\,({\bf{t}}, {\rm{or-zerop-tree}}\,({\it{x\/}})\index{or-zerop-tree}, {\it{a\/}}) $=$ ($\neg$ {\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree}, {\it{a\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable or-zerop-tree-is-not-zerop-tree.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  zerop-makes-times-tree-zero2 \\ \index{zerop-makes-times-tree-zero2}
\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{or-zerop-tree}}\,({\it{x\/}})\index{or-zerop-tree}, {\it{a\/}}) $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}) $=$ {\tt{0}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-makes-times-tree-zero2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  times-tree-append \\ \index{times-tree-append}
\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{times-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable times-tree-append.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  times-tree-of-times-fringe \\ \index{times-tree-of-times-fringe}
{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe})\index{times-tree}, {\it{a\/}}) $=$ {\rm{fix}}\,({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable times-tree-of-times-fringe.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{cancel-lessp-times} \\  
\=\+{\rm{cancel-lessp-times}}\,({\it{x\/}})\index{cancel-lessp-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{lessp}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}})\- \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\index{bagint}) \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{and-not-zerop-tree}}\,({\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\index{and-not-zerop-tree}, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{lessp}}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree})\-)\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  eval\$-lessp-times-tree-bagdiff \\ \index{eval\$-lessp-times-tree-bagdiff}
\=\+({\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{z\/}})\index{subbagp} $\wedge$ {\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree}, {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{y\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}) \\ 
$<$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{z\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}))\- \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}) $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{z\/}})\index{times-tree}, {\it{a\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-lessp-times-tree-bagdiff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  zerop-makes-lessp-false-bridge \\ \index{zerop-makes-lessp-false-bridge}
\=\+(\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{y\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\rm{and-not-zerop-tree}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, {\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe})\index{bagint})\index{and-not-zerop-tree}, \\ 
{\it{a\/}})\-))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})) \\ 
$<$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{y\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{y\/}}), {\it{a\/}})))\- \\ 
$=$$\;\;\;\;${\bf{f}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-makes-lessp-false-bridge.

\addvspace{18pt}


\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-lessp-times \\ \index{correctness-of-cancel-lessp-time!s}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-lessp-times}}\,({\it{x\/}})\index{cancel-lessp-times}, {\it{a\/}})
\end{tabbing}



\begin{tabbing}{\sc Definition}:\index{cancel-equal-times} \\  
\=\+{\rm{cancel-equal-times}}\,({\it{x\/}})\index{cancel-equal-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{equal}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}})\- \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\index{bagint}) \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{or}}, \\ 
{\rm{or-zerop-tree}}\,({\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\index{or-zerop-tree}, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree})\-)\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zerop-makes-equal-true-bridge \\ \index{zerop-makes-equal-true-bridge}
\=\+(\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{y\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{or-zerop-tree}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, {\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe})\index{bagint})\index{or-zerop-tree}, {\it{a\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})) \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{y\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{y\/}}), {\it{a\/}})))\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-makes-equal-true-bridge.

\addvspace{18pt}
                       
\begin{tabbing}{\sc Theorem}:  eval\$-equal-times-tree-bagdiff \\ \index{eval\$-equal-times-tree-bagdiff}
\=\+({\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{z\/}})\index{subbagp} $\wedge$ ($\neg$ {\rm{eval\$}}\,({\bf{t}}, {\rm{or-zerop-tree}}\,({\it{x\/}})\index{or-zerop-tree}, {\it{a\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{y\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{z\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}))\- \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{z\/}})\index{times-tree}, {\it{a\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-equal-times-tree-bagdiff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cancel-equal-times-preserves-inequality \\ \index{cancel-equal-times-preserves-ineq!uality}
\=\+(\=\+{\rm{subbagp}}\,({\it{z\/}}, {\it{x\/}})\index{subbagp} \\ 
$\wedge$$\;\;\;\;${\rm{subbagp}}\,({\it{z\/}}, {\it{y\/}})\index{subbagp} \\ 
$\wedge$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $\not=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{x\/}}, {\it{z\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}) \\ 
$\not=$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{y\/}}, {\it{z\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable cancel-equal-times-preserves-inequality.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  cancel-equal-times-preserves-inequality-bridge \\ \index{cancel-equal-times-preserves-ineq!uality-bridge}
\=\+(\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{y\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$(\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})) \\ 
$\not=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{y\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{y\/}}), {\it{a\/}})))\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, \\ 
{\rm{bagint}}\,({\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, {\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe})\index{bagint})\-\index{bagdiff})\index{times-tree}, \\ 
{\it{a\/}})\- \\ 
$\not=$$\;\;\;\;${\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree}, \\ 
{\it{a\/}})\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable cancel-equal-times-preserves-inequality-bridge.

\addvspace{18pt}
                    
\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-equal-times \\ \index{correctness-of-cancel-equal-time!s}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-equal-times}}\,({\it{x\/}})\index{cancel-equal-times}, {\it{a\/}})
\end{tabbing}






\begin{verbatim}; ---------- REMAINDER ----------

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

\begin{tabbing}{\sc Theorem}:  remainder-noop \\ \index{remainder-noop}
({\it{a\/}} $<$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\rm{fix}}\,({\it{a\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-of-non-number \\ \index{remainder-of-non-number}
({\it{a\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ ({\tt{0}} ${}${\bf{mod}}${}$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-zero \\ \index{remainder-zero}
({\it{x\/}} $\simeq {\tt{0}}$) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}

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


\noindent{\sc Event}:   Disable plus-remainder-times-quotient.

\addvspace{18pt}

\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{verbatim}; (prove-lemma remainder-sub1 (rewrite)
;        (implies (and (not (zerop a))
;                    (not (zerop b)))
;               (equal (remainder (sub1 a) b)
;                      (if (equal (remainder a b) 0)
;                          (sub1 b)
;                          (sub1 (remainder a b)))))
;        ((enable lessp-remainder
;               remainder-noop
;               remainder-quotient-elim)
;       (enable-theory addition)
;       (induct (remainder a b))))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-add1 \\ \index{remainder-add1}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) $\rightarrow$ ((($1\;+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ ({\tt{1}} ${}${\bf{mod}}${}$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-proof \\ \index{remainder-plus-proof}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus \\ \index{remainder-plus}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{b\/}} $+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ (({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{c\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-plus-0-proof \\ \index{equal-remainder-plus-0-proof}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-plus-0 \\ \index{equal-remainder-plus-0}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})) \\ 
$\wedge$$\;\;\;\;$(((({\it{b\/}} $+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})) \\ 
$\wedge$$\;\;\;\;$(\=\+((({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-plus-remainder-proof \\ \index{equal-remainder-plus-remainder-p!roof}
({\it{a\/}} $<$ {\it{c\/}}) $\rightarrow$ (((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) $=$ ({\it{a\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-remainder-plus-remainder \\ \index{equal-remainder-plus-remainder}
\=\+({\it{a\/}} $<$ {\it{c\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) $=$ ({\it{a\/}} $\simeq {\tt{0}}$)) \\ 
$\wedge$$\;\;\;\;$(((({\it{b\/}} $+$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) $=$ ({\it{a\/}} $\simeq {\tt{0}}$)))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable equal-remainder-plus-remainder.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  remainder-times1 \\ \index{remainder-times1}
\=\+(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{a\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ ((({\it{b\/}} $*$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}))\-
\end{tabbing}

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

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

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

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


\noindent{\sc Event}:   Disable remainder-times-times.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  remainder-times2 \\ \index{remainder-times2}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ ({\it{z\/}} $*$ (({\it{a\/}} $\div$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{y\/}}))) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} ${}${\bf{mod}}${}$ ({\it{z\/}} $*$ {\it{y\/}})) $=$ ({\it{z\/}} $*$ (({\it{a\/}} $\div$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{y\/}}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times2-instance \\ \index{remainder-times2-instance}
\=\+((({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ ({\it{x\/}} $*$ {\it{z\/}})) $=$ ({\it{x\/}} $*$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{x\/}} $*$ {\it{z\/}}) ${}${\bf{mod}}${}$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $*$ {\it{z\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-difference1 \\ \index{remainder-difference1}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $-$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $-$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{double-remainder-induction} \\  
\=\+{\rm{double-remainder-induction}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}})\index{double-remainder-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{c\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{a\/}} $<$ {\it{c\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{b\/}} $<$ {\it{c\/}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{double-remainder-induction}}\,({\it{a\/}} $-$ {\it{c\/}}, {\it{b\/}} $-$ {\it{c\/}}, {\it{c\/}})\index{double-remainder-induction}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-difference2 \\ \index{remainder-difference2}
\=\+((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $-$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\it{c\/}} $-$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-difference3 \\ \index{remainder-difference3}
\=\+((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $-$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }{\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable remainder-difference3.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  equal-remainder-difference-0 \\ \index{equal-remainder-difference-0}
\=\+((({\it{a\/}} $-$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\leq$ {\it{a\/}}$\;\;${\bf then }({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable equal-remainder-difference-0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  lessp-plus-fact \\ \index{lessp-plus-fact}
\=\+((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{c\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{b\/}} $<$ {\it{c\/}}) $\wedge$ ({\it{a\/}} $<$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $+$ {\it{b\/}}) $<$ {\it{c\/}}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable lessp-plus-fact.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  remainder-plus-fact \\ \index{remainder-plus-fact}
\=\+((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{c\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{a\/}} $<$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $+$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{a\/}} $+$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-times-times-proof \\ \index{remainder-plus-times-times-proo!f}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{d\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $+$ (({\it{b\/}} $*$ {\it{c\/}}) ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{d\/}}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-times-times \\ \index{remainder-plus-times-times}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{d\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $+$ (({\it{b\/}} $*$ {\it{c\/}}) ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{d\/}}))))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{a\/}} $+$ ({\it{c\/}} $*$ {\it{b\/}})) ${}${\bf{mod}}${}$ ({\it{d\/}} $*$ {\it{b\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $+$ (({\it{c\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ ({\it{d\/}} $*$ {\it{b\/}}))))\-)\-\-
\end{tabbing}

\begin{verbatim}; REMAINDER-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES-TIMES and REMAINDER-PLUS-TIMES-TIMES

\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-plus-times-times-instance \\ \index{remainder-plus-times-times-inst!ance}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}}) $+$ ({\it{b\/}} $*$ {\it{d\/}})) ${}${\bf{mod}}${}$ ({\it{b\/}} $*$ {\it{e\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $+$ ({\it{b\/}} $*$ (({\it{c\/}} $+$ {\it{d\/}}) ${}${\bf{mod}}${}$ {\it{e\/}}))))\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{a\/}} $+$ ({\it{c\/}} $*$ {\it{b\/}}) $+$ ({\it{d\/}} $*$ {\it{b\/}})) ${}${\bf{mod}}${}$ ({\it{e\/}} $*$ {\it{b\/}})) \\ 
$=$$\;\;\;\;$({\it{a\/}} $+$ ({\it{b\/}} $*$ (({\it{c\/}} $+$ {\it{d\/}}) ${}${\bf{mod}}${}$ {\it{e\/}}))))\-)\-\-
\end{tabbing}

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


\begin{tabbing}{\sc Theorem}:  remainder-1-arg1 \\ \index{remainder-1-arg1}
\=\+({\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 Theorem}:  remainder-1-arg2 \\ \index{remainder-1-arg2}
({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{1}}) $=$ {\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}:  transitivity-of-divides \\ \index{transitivity-of-divides}
((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})
\end{tabbing}




\begin{verbatim}; ---------- QUOTIENT, DIVIDES  ----------

\end{verbatim}\begin{tabbing}{\sc Theorem}:  quotient-noop \\ \index{quotient-noop}
({\it{b\/}} $=$ {\tt{1}}) $\rightarrow$ (({\it{a\/}} $\div$ {\it{b\/}}) $=$ {\rm{fix}}\,({\it{a\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-of-non-number \\ \index{quotient-of-non-number}
({\it{a\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{a\/}} $\div$ {\it{n\/}}) $=$ ({\tt{0}} $\div$ {\it{n\/}}))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  quotient-add1 \\ \index{quotient-add1}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(($1\;+$ {\it{a\/}}) $\div$ {\it{b\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $=$ {\tt{1}}$\;\;${\bf then }$1\;+$ ({\it{a\/}} $\div$ {\it{b\/}}) \\ 
{\bf else }{\it{a\/}} $\div$ {\it{b\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-quotient-0 \\ \index{equal-quotient-0}
(({\it{a\/}} $\div$ {\it{b\/}}) $=$ {\tt{0}}) $=$ (({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{a\/}} $<$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-sub1 \\ \index{quotient-sub1}
\=\+(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $-\;1$) $\div$ {\it{b\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}}) $=$ {\tt{0}}$\;\;${\bf then }({\it{a\/}} $\div$ {\it{b\/}}) $-\;1$ \\ 
{\bf else }{\it{a\/}} $\div$ {\it{b\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus-proof \\ \index{quotient-plus-proof}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{a\/}} $+$ {\it{b\/}}) $\div$ {\it{c\/}}) $=$ (({\it{a\/}} $\div$ {\it{c\/}}) $+$ ({\it{b\/}} $\div$ {\it{c\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus \\ \index{quotient-plus}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $+$ {\it{b\/}}) $\div$ {\it{c\/}}) $=$ (({\it{a\/}} $\div$ {\it{c\/}}) $+$ ({\it{b\/}} $\div$ {\it{c\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{b\/}} $+$ {\it{a\/}}) $\div$ {\it{c\/}}) $=$ (({\it{a\/}} $\div$ {\it{c\/}}) $+$ ({\it{b\/}} $\div$ {\it{c\/}}))) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{a\/}}) $\div$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$((({\it{x\/}} $+$ {\it{y\/}}) $\div$ {\it{c\/}}) $+$ ({\it{a\/}} $\div$ {\it{c\/}})))\-)\-\-
\end{tabbing}

\begin{verbatim}; I need QUOTIENT-TIMES-INSTANCE to prove the more general QUOTIENT-TIMES,
; but I want QUOTIENT-TIMES-INSTANCE to be tried first (i.e. come after
; QUOTIENT-TIMES in the event list.) So first, prove QUOTIENT-TIMES-INSTANCE-TEMP,
; then prove QUOTIENT-TIMES, and finally give QUOTIENT-TIMES-INSTANCE.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  quotient-times-instance-temp-proof \\ \index{quotient-times-instance-temp-pr!oof}
\=\+(({\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}:  quotient-times-instance-temp \\ \index{quotient-times-instance-temp}
\=\+(\=\+(({\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}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{x\/}} $*$ {\it{y\/}}) $\div$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable quotient-times-instance-temp.

\addvspace{18pt}

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

\begin{tabbing}{\sc Theorem}:  quotient-times \\ \index{quotient-times}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $*$ {\it{b\/}}) $\div$ {\it{c\/}}) $=$ ({\it{b\/}} $*$ ({\it{a\/}} $\div$ {\it{c\/}}))) \\ 
$\wedge$$\;\;\;\;$((({\it{b\/}} $*$ {\it{a\/}}) $\div$ {\it{c\/}}) $=$ ({\it{b\/}} $*$ ({\it{a\/}} $\div$ {\it{c\/}}))))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times-instance \\ \index{quotient-times-instance}
\=\+(\=\+(({\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}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{x\/}} $*$ {\it{y\/}}) $\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}:  quotient-times-times-proof \\ \index{quotient-times-times-proof}
\=\+(({\it{x\/}} $*$ {\it{y\/}}) $\div$ ({\it{x\/}} $*$ {\it{z\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\it{y\/}} $\div$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}

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


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  quotient-difference1 \\ \index{quotient-difference1}
\=\+(({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ ({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $-$ {\it{b\/}}) $\div$ {\it{c\/}}) $=$ (({\it{a\/}} $\div$ {\it{c\/}}) $-$ ({\it{b\/}} $\div$ {\it{c\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-lessp-arg1 \\ \index{quotient-lessp-arg1}
({\it{a\/}} $<$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} $\div$ {\it{b\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-difference2 \\ \index{quotient-difference2}
\=\+((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $-$ {\it{b\/}}) $\div$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }({\it{a\/}} $\div$ {\it{c\/}}) $-$ ($1\;+$ ({\it{b\/}} $\div$ {\it{c\/}})) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-difference3 \\ \index{quotient-difference3}
\=\+((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{a\/}} $-$ {\it{b\/}}) $\div$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $<$ {\it{a\/}}$\;\;${\bf then }({\it{a\/}} $\div$ {\it{c\/}}) $-$ ({\it{b\/}} $\div$ {\it{c\/}}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-equals-its-first-argument \\ \index{remainder-equals-its-first-argu!ment}
({\it{a\/}} $=$ ({\it{a\/}} ${}${\bf{mod}}${}$ {\it{b\/}})) $=$ (({\it{a\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{a\/}} $<$ {\it{b\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable remainder-equals-its-first-argument.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  quotient-remainder-times \\ \index{quotient-remainder-times}
(({\it{x\/}} ${}${\bf{mod}}${}$ ({\it{a\/}} $*$ {\it{b\/}})) $\div$ {\it{a\/}}) $=$ (({\it{x\/}} $\div$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  quotient-remainder-instance \\ \index{quotient-remainder-instance}
(({\it{x\/}} ${}${\bf{mod}}${}$ ({\it{a\/}} $*$ {\it{b\/}})) $\div$ {\it{a\/}}) $=$ (({\it{x\/}} $\div$ {\it{a\/}}) ${}${\bf{mod}}${}$ {\it{b\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus-fact \\ \index{quotient-plus-fact}
\=\+((({\it{b\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{c\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{a\/}} $<$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $+$ {\it{b\/}}) $\div$ {\it{c\/}}) $=$ ({\it{b\/}} $\div$ {\it{c\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus-times-times-proof \\ \index{quotient-plus-times-times-proof}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) $\div$ ({\it{b\/}} $*$ {\it{d\/}})) $=$ (({\it{b\/}} $*$ {\it{c\/}}) $\div$ ({\it{b\/}} $*$ {\it{d\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus-times-times \\ \index{quotient-plus-times-times}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) $\div$ ({\it{b\/}} $*$ {\it{d\/}})) $=$ (({\it{b\/}} $*$ {\it{c\/}}) $\div$ ({\it{b\/}} $*$ {\it{d\/}}))) \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}})) $\div$ ({\it{b\/}} $*$ {\it{d\/}})) \\ 
$=$$\;\;\;\;$(({\it{b\/}} $*$ {\it{c\/}}) $\div$ ({\it{b\/}} $*$ {\it{d\/}})))\-)\-\-
\end{tabbing}

\begin{verbatim}; QUOTIENT-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; QUOTIENT-TIMES-TIMES, QUOTIENT-PLUS-TIMES-TIMES and TIMES-DISTRIBUTES-OVER-PLUS

\end{verbatim}\begin{tabbing}{\sc Theorem}:  quotient-plus-times-times-instance \\ \index{quotient-plus-times-times-insta!nce}
\=\+({\it{a\/}} $<$ {\it{b\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+(({\it{a\/}} $+$ ({\it{b\/}} $*$ {\it{c\/}}) $+$ ({\it{b\/}} $*$ {\it{d\/}})) $\div$ ({\it{b\/}} $*$ {\it{e\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }({\it{c\/}} $+$ {\it{d\/}}) $\div$ {\it{e\/}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{a\/}} $+$ ({\it{c\/}} $*$ {\it{b\/}}) $+$ ({\it{d\/}} $*$ {\it{b\/}})) $\div$ ({\it{e\/}} $*$ {\it{b\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }({\it{d\/}} $+$ {\it{c\/}}) $\div$ {\it{e\/}}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-quotient \\ \index{quotient-quotient}
(({\it{b\/}} $\div$ {\it{a\/}}) $\div$ {\it{c\/}}) $=$ ({\it{b\/}} $\div$ ({\it{a\/}} $*$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-quotient \\ \index{leq-quotient}
({\it{a\/}} $<$ {\it{b\/}}) $\rightarrow$ (({\it{a\/}} $\div$ {\it{c\/}}) $\leq$ ({\it{b\/}} $\div$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-1-arg2 \\ \index{quotient-1-arg2}
({\it{n\/}} $\div$ {\tt{1}}) $=$ {\rm{fix}}\,({\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-1-arg1-casesplit \\ \index{quotient-1-arg1-casesplit}
({\it{n\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{n\/}} $=$ {\tt{1}}) $\vee$ ({\tt{1}} $<$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-1-arg1 \\ \index{quotient-1-arg1}
\=\+({\tt{1}} $\div$ {\it{n\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}


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

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


\begin{verbatim};; Metalemma to cancel quotient-times expressions

;; ex.
;; (quotient (times a b) (times c (times d a)))  -> 
;;                                           (if (not (zerop a))
;;                                               (quotient (fix b) (times c d))
;;                                            (zero))
;;

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{cancel-quotient-times} \\  
\=\+{\rm{cancel-quotient-times}}\,({\it{x\/}})\index{cancel-quotient-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{quotient}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}})\- \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\index{bagint}) \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{if}}, \\ 
{\rm{and-not-zerop-tree}}\,({\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\index{and-not-zerop-tree}, \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{quotient}}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree}, \\ 
{\rm{times-tree}}\,({\rm{bagdiff}}\,(\=\+{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{bagint}}\,(\=\+{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe}, \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{bagint})\-\index{bagdiff})\index{times-tree})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{zero}}{\tt{)}})\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  zerop-makes-quotient-zero-bridge \\ \index{zerop-makes-quotient-zero-bridge}
\=\+(\=\+({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{y\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\rm{and-not-zerop-tree}}\,({\rm{bagint}}\,({\rm{times-fringe}}\,({\it{x\/}})\index{times-fringe}, {\rm{times-fringe}}\,({\it{y\/}})\index{times-fringe})\index{bagint})\index{and-not-zerop-tree}, \\ 
{\it{a\/}})\-))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{x\/}}), {\it{a\/}})) \\ 
$\div$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{y\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{caddr}}\,({\it{y\/}}), {\it{a\/}})))\- \\ 
$=$$\;\;\;\;${\tt{0}})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable zerop-makes-quotient-zero-bridge.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-quotient-times-tree-bagdiff \\ \index{eval\$-quotient-times-tree-bagdi!ff}
\=\+({\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{z\/}})\index{subbagp} $\wedge$ {\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree}, {\it{a\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{y\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}) \\ 
$\div$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{bagdiff}}\,({\it{z\/}}, {\it{x\/}})\index{bagdiff})\index{times-tree}, {\it{a\/}}))\- \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{y\/}})\index{times-tree}, {\it{a\/}}) $\div$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{z\/}})\index{times-tree}, {\it{a\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable eval\$-quotient-times-tree-bagdiff.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  correctness-of-cancel-quotient-times \\ \index{correctness-of-cancel-quotient-ti!mes}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel-quotient-times}}\,({\it{x\/}})\index{cancel-quotient-times}, {\it{a\/}})
\end{tabbing}


\begin{verbatim};;; exp, log, and gcd

\end{verbatim}\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 Definition}:\index{log} \\  
\=\+{\rm{log}}\,({\it{base\/}}, {\it{n\/}})\index{log} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{base\/}} $<$ {\tt{2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{log}}\,({\it{base\/}}, {\it{n\/}} $\div$ {\it{base\/}})\index{log}$\;${\bf  endif}\-\-
\end{tabbing}



\begin{tabbing}{\sc Definition}:\index{gcd} \\  
\=\+{\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{fix}}\,({\it{y\/}}) \\ 
{\bf elseif }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf elseif }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\rm{gcd}}\,({\it{x\/}}, {\it{y\/}} $-$ {\it{x\/}})\index{gcd} \\ 
{\bf else }{\rm{gcd}}\,({\it{x\/}} $-$ {\it{y\/}}, {\it{y\/}})\index{gcd}$\;${\bf  endif}\-\-
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  remainder-exp \\ \index{remainder-exp}
({\it{k\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\rm{exp}}\,({\it{n\/}}, {\it{k\/}})\index{exp} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\tt{0}})
\end{tabbing}


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


\begin{tabbing}{\sc Theorem}:  remainder-exp-exp \\ \index{remainder-exp-exp}
({\it{i\/}} $\leq$ {\it{j\/}}) $\rightarrow$ (({\rm{exp}}\,({\it{a\/}}, {\it{j\/}})\index{exp} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\it{a\/}}, {\it{i\/}})\index{exp}) $=$ {\tt{0}})
\end{tabbing}


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


\begin{tabbing}{\sc Theorem}:  exp-zero \\ \index{exp-zero}
({\it{k\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{exp}}\,({\it{n\/}}, {\it{k\/}})\index{exp} $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-add1 \\ \index{exp-add1}
{\rm{exp}}\,({\it{n\/}}, $1\;+$ {\it{k\/}})\index{exp} $=$ ({\it{n\/}} $*$ {\rm{exp}}\,({\it{n\/}}, {\it{k\/}})\index{exp})
\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}:  exp-0-arg1 \\ \index{exp-0-arg1}
\=\+{\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-1-arg1 \\ \index{exp-1-arg1}
{\rm{exp}}\,({\tt{1}}, {\it{k\/}})\index{exp} $=$ {\tt{1}}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-0-arg2 \\ \index{exp-0-arg2}
{\rm{exp}}\,({\it{n\/}}, {\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}:  equal-exp-0 \\ \index{equal-exp-0}
({\rm{exp}}\,({\it{n\/}}, {\it{k\/}})\index{exp} $=$ {\tt{0}}) $=$ (({\it{n\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{k\/}} $\not\simeq {\tt{0}}$))
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  exp-difference \\ \index{exp-difference}
(({\it{c\/}} $\leq$ {\it{b\/}}) $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{exp}}\,({\it{a\/}}, {\it{b\/}} $-$ {\it{c\/}})\index{exp} $=$ ({\rm{exp}}\,({\it{a\/}}, {\it{b\/}})\index{exp} $\div$ {\rm{exp}}\,({\it{a\/}}, {\it{c\/}})\index{exp}))
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  equal-log-0 \\ \index{equal-log-0}
({\rm{log}}\,({\it{base\/}}, {\it{n\/}})\index{log} $=$ {\tt{0}}) $=$ (({\it{base\/}} $<$ {\tt{2}}) $\vee$ ({\it{n\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-0 \\ \index{log-0}
({\it{n\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{log}}\,({\it{base\/}}, {\it{n\/}})\index{log} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-1 \\ \index{log-1}
({\tt{1}} $<$ {\it{base\/}}) $\rightarrow$ ({\rm{log}}\,({\it{base\/}}, {\tt{1}})\index{log} $=$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{double-log-induction} \\  
\=\+{\rm{double-log-induction}}\,({\it{base\/}}, {\it{a\/}}, {\it{b\/}})\index{double-log-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{base\/}} $<$ {\tt{2}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{a\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{b\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{double-log-induction}}\,({\it{base\/}}, {\it{a\/}} $\div$ {\it{base\/}}, {\it{b\/}} $\div$ {\it{base\/}})\index{double-log-induction}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  leq-log-log \\ \index{leq-log-log}
({\it{n\/}} $\leq$ {\it{m\/}}) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $\leq$ {\rm{log}}\,({\it{c\/}}, {\it{m\/}})\index{log})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-quotient \\ \index{log-quotient}
({\tt{1}} $<$ {\it{c\/}}) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ {\it{c\/}})\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-quotient-times-proof \\ \index{log-quotient-times-proof}
({\tt{1}} $<$ {\it{c\/}}) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ ({\it{c\/}} $*$ {\it{m\/}}))\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ {\it{m\/}})\index{log} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-quotient-times \\ \index{log-quotient-times}
\=\+({\tt{1}} $<$ {\it{c\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ ({\it{c\/}} $*$ {\it{m\/}}))\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ {\it{m\/}})\index{log} $-\;1$)) \\ 
$\wedge$$\;\;\;\;$({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ ({\it{m\/}} $*$ {\it{c\/}}))\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ {\it{m\/}})\index{log} $-\;1$)))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-quotient-exp \\ \index{log-quotient-exp}
({\tt{1}} $<$ {\it{c\/}}) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $\div$ {\rm{exp}}\,({\it{c\/}}, {\it{m\/}})\index{exp})\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $-$ {\it{m\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-times-proof \\ \index{log-times-proof}
(({\tt{1}} $<$ {\it{c\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{c\/}} $*$ {\it{n\/}})\index{log} $=$ ($1\;+$ {\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  log-times \\ \index{log-times}
\=\+(({\tt{1}} $<$ {\it{c\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{log}}\,({\it{c\/}}, {\it{c\/}} $*$ {\it{n\/}})\index{log} $=$ ($1\;+$ {\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log})) \\ 
$\wedge$$\;\;\;\;$({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $*$ {\it{c\/}})\index{log} $=$ ($1\;+$ {\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-times-exp-proof \\ \index{log-times-exp-proof}
(({\tt{1}} $<$ {\it{c\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $*$ {\rm{exp}}\,({\it{c\/}}, {\it{m\/}})\index{exp})\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $+$ {\it{m\/}}))
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  log-times-exp \\ \index{log-times-exp}
\=\+(({\tt{1}} $<$ {\it{c\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{log}}\,({\it{c\/}}, {\it{n\/}} $*$ {\rm{exp}}\,({\it{c\/}}, {\it{m\/}})\index{exp})\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $+$ {\it{m\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{log}}\,({\it{c\/}}, {\rm{exp}}\,({\it{c\/}}, {\it{m\/}})\index{exp} $*$ {\it{n\/}})\index{log} $=$ ({\rm{log}}\,({\it{c\/}}, {\it{n\/}})\index{log} $+$ {\it{m\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  log-exp \\ \index{log-exp}
({\tt{1}} $<$ {\it{c\/}}) $\rightarrow$ ({\rm{log}}\,({\it{c\/}}, {\rm{exp}}\,({\it{c\/}}, {\it{n\/}})\index{exp})\index{log} $=$ ($1\;+$ {\it{n\/}}))
\end{tabbing}





\begin{tabbing}{\sc Theorem}:  commutativity-of-gcd \\ \index{commutativity-of-gcd}
{\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{single-number-induction} \\  
\=\+{\rm{single-number-induction}}\,({\it{n\/}})\index{single-number-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{single-number-induction}}\,({\it{n\/}} $-\;1$)\index{single-number-induction}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-0 \\ \index{gcd-0}
({\rm{gcd}}\,({\tt{0}}, {\it{x\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{x\/}})) $\wedge$ ({\rm{gcd}}\,({\it{x\/}}, {\tt{0}})\index{gcd} $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  lessp-gcd \\ \index{lessp-gcd}
({\it{b\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ((({\it{b\/}} $<$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ {\bf{f}}) $\wedge$ (({\it{b\/}} $<$ {\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd}) $=$ {\bf{f}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  gcd-plus-instance-temp-proof \\ \index{gcd-plus-instance-temp-proof}
{\rm{gcd}}\,({\it{a\/}}, {\it{a\/}} $+$ {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-plus-instance-temp \\ \index{gcd-plus-instance-temp}
({\rm{gcd}}\,({\it{a\/}}, {\it{a\/}} $+$ {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $\wedge$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $+$ {\it{a\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-plus-proof \\ \index{gcd-plus-proof}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $\rightarrow$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $+$ {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-plus \\ \index{gcd-plus}
\=\+(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $+$ {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{a\/}}, {\it{c\/}} $+$ {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{b\/}} $+$ {\it{c\/}}, {\it{a\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{c\/}} $+$ {\it{b\/}}, {\it{a\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-plus-instance \\ \index{gcd-plus-instance}
({\rm{gcd}}\,({\it{a\/}}, {\it{a\/}} $+$ {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $\wedge$ ({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}} $+$ {\it{a\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-gcd \\ \index{remainder-gcd}
(({\it{a\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ {\tt{0}}) $\wedge$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ {\tt{0}})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-gcd-proof \\ \index{distributivity-of-times-over-gc!d-proof}
{\rm{gcd}}\,({\it{x\/}} $*$ {\it{z\/}}, {\it{y\/}} $*$ {\it{z\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-gcd \\ \index{distributivity-of-times-over-gc!d}
\=\+({\rm{gcd}}\,({\it{x\/}} $*$ {\it{z\/}}, {\it{y\/}} $*$ {\it{z\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{z\/}} $*$ {\it{x\/}}, {\it{y\/}} $*$ {\it{z\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{x\/}} $*$ {\it{z\/}}, {\it{z\/}} $*$ {\it{y\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{z\/}} $*$ {\it{x\/}}, {\it{z\/}} $*$ {\it{y\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gcd-is-the-greatest \\ \index{gcd-is-the-greatest}
\=\+(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$({\it{z\/}} $\leq$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  common-divisor-divides-gcd \\ \index{common-divisor-divides-gcd}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})) $\rightarrow$ (({\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}

\begin{verbatim}; We prove ASSOCIATIVITY-OF-GCD and COMMUTATIVITY2-OF-GCD roughly the same way.
; Use GCD-IS-THE-GREATEST twice to show that each side of the equality is
; less than or equal to the other side.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  associativity-of-gcd-zero-case \\ \index{associativity-of-gcd-zero-case}
(({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{c\/}} $\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{gcd}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\rm{gcd}}\,({\it{b\/}}, {\it{c\/}})\index{gcd})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  associativity-of-gcd \\ \index{associativity-of-gcd}
{\rm{gcd}}\,({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{c\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\rm{gcd}}\,({\it{b\/}}, {\it{c\/}})\index{gcd})\index{gcd}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-gcd-zero-case \\ \index{commutativity2-of-gcd-zero-case}
(({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{c\/}} $\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{gcd}}\,({\it{b\/}}, {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\rm{gcd}}\,({\it{b\/}}, {\it{c\/}})\index{gcd})\index{gcd})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  commutativity2-of-gcd \\ \index{commutativity2-of-gcd}
{\rm{gcd}}\,({\it{b\/}}, {\rm{gcd}}\,({\it{a\/}}, {\it{c\/}})\index{gcd})\index{gcd} $=$ {\rm{gcd}}\,({\it{a\/}}, {\rm{gcd}}\,({\it{b\/}}, {\it{c\/}})\index{gcd})\index{gcd}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  gcd-idempotence \\ \index{gcd-idempotence}
({\rm{gcd}}\,({\it{x\/}}, {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})\index{gcd} $=$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $\wedge$ ({\rm{gcd}}\,({\it{y\/}}, {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})\index{gcd} $=$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})
\end{tabbing}

\begin{verbatim};;; new stuff

\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-zero \\ \index{gcd-zero}
({\it{x\/}} $\simeq {\tt{0}}$) $\rightarrow$ (({\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{y\/}})) $\wedge$ ({\rm{gcd}}\,({\it{y\/}}, {\it{x\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{y\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-quotient-gcd-0 \\ \index{remainder-quotient-gcd-0}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ ({\it{x\/}} $\div$ {\it{a\/}})) $=$ {\tt{0}})
\end{tabbing}
       
\begin{tabbing}{\sc Theorem}:  remainder-gcd-0 \\ \index{remainder-gcd-0}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$((({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ {\tt{0}}) $\wedge$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd}) $=$ {\tt{0}}))\-
\end{tabbing}

\begin{verbatim};I think this is not important
;(prove-lemma gcd-of-reduce-numbers-helper-helper (rewrite)
;            (equal
;             (remainder a (gcd (quotient a (gcd a b)) (quotient b (gcd a b))))
;             0))

; I believe that the following works just as well as this one because
; of commutativity-of-gcd 
;(prove-lemma gcd-of-reduced-numbers-helper (rewrite)
;       (implies
;       (not (zerop a))
;       (and
;        (equal (gcd (quotient a (gcd a b))
;                  (quotient b (gcd a b)))
;             1)
;        (equal (gcd (quotient b (gcd a b))
;                  (quotient a (gcd a b)))
;             1)
;        (equal (gcd (quotient b (gcd b a))
;                  (quotient a (gcd b a)))
;             1)
;        (equal (gcd (quotient a (gcd b a))
;                  (quotient b (gcd b a)))
;             1))))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-quotient-gcd \\ \index{gcd-quotient-gcd}
\=\+({\it{a\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{gcd}}\,({\it{a\/}} $\div$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}, {\it{b\/}} $\div$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd})\index{gcd} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$({\rm{gcd}}\,({\it{b\/}} $\div$ {\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd}, {\it{a\/}} $\div$ {\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd})\index{gcd} $=$ {\tt{1}}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-gcd2 \\ \index{lessp-gcd2}
\=\+(({\it{b\/}} $<$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ (({\it{b\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$))) \\ 
$\wedge$$\;\;\;\;$(({\it{b\/}} $<$ {\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd}) $=$ (({\it{b\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{a\/}} $\not\simeq {\tt{0}}$)))\-
\end{tabbing}


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

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

\begin{verbatim};; replaced by gcd-zero
;(lemma gcd-zerop (rewrite)
;       (implies
;       (zerop x)
;       (and
;        (equal (gcd x z) (fix z))
;        (equal (gcd z x) (fix z))))
;       ((enable-theory naturals)
;       (enable gcd)))

; (disable gcd-zerop) ; subsumed by gcd-remainder

\end{verbatim}\begin{tabbing}{\sc Theorem}:  gcd-remainder \\ \index{gcd-remainder}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (({\rm{gcd}}\,({\it{x\/}}, {\it{z\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{z\/}})) $\wedge$ ({\rm{gcd}}\,({\it{z\/}}, {\it{x\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{z\/}})))
\end{tabbing}


\noindent{\sc Event}:   Disable gcd-zero.

\addvspace{18pt} \begin{verbatim}; subsumed by gcd-remainder

; no longer needed
;(lemma equal-times-x-x-fact (rewrite)
;       (implies (and (not (equal x 0))
;                    (not (equal y 1)))
;               (and
;                (equal (equal (times x y) x) f)
;                (equal (equal (times y x) x) f)))
;       ((enable-theory naturals)
;       (induct (times y x))))

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


\begin{tabbing}{\sc Theorem}:  equal-x-gcd-x-y \\ \index{equal-x-gcd-x-y}
\=\+({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{x\/}} $=$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}))) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $=$ {\rm{gcd}}\,({\it{y\/}}, {\it{x\/}})\index{gcd}) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}))))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  quotient-difference \\ \index{quotient-difference}
\=\+(({\it{x\/}} $-$ {\it{y\/}}) $\div$ {\it{z\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $<$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}})$\;\;${\bf then }(({\it{x\/}} $\div$ {\it{z\/}}) $-$ ({\it{y\/}} $\div$ {\it{z\/}})) $-\;1$ \\ 
{\bf else }({\it{x\/}} $\div$ {\it{z\/}}) $-$ ({\it{y\/}} $\div$ {\it{z\/}})$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  equal-as-remainder \\ \index{equal-as-remainder}
\=\+((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $=$ {\it{y\/}}) $=$ {\bf{t}})\-
\end{tabbing}


\noindent{\sc Event}:   Disable equal-as-remainder.

\addvspace{18pt}

\begin{verbatim};; add so as to control rewriting equal better
\end{verbatim}\begin{tabbing}{\sc Theorem}:  equal-gcd-gcd-as-remainder \\ \index{equal-gcd-gcd-as-remainder}
\=\+((({\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd}) $=$ {\tt{0}}) $\wedge$ (({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-gcd-0-means \\ \index{remainder-gcd-0-means}
\=\+((({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})) \\ 
$\wedge$$\;\;\;\;$((({\rm{gcd}}\,({\it{b\/}}, {\it{a\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) $\rightarrow$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-gcd-arg1 \\ \index{remainder-gcd-arg1}
\=\+(({\rm{gcd}}\,({\it{a\/}}, {\it{b\/}})\index{gcd} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}} \\ 
{\bf then }\=\+{\bf if }({\it{b\/}} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-diff1 \\ \index{remainder-diff1}
\=\+((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{w\/}} $*$ {\it{x\/}}) $\not<$ {\it{z\/}})) \\ 
$\rightarrow$$\;\;\;\;$((((({\it{w\/}} $*$ {\it{x\/}}) $-$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}}) $=$ (({\it{z\/}} ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-diff2 \\ \index{remainder-diff2}
\=\+(\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{w\/}} $*$ {\it{x\/}}) $\not<$ {\it{z\/}}) \\ 
$\wedge$$\;\;\;\;$(((({\it{w\/}} $*$ {\it{x\/}}) $-$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{z\/}} ${}${\bf{mod}}${}$ {\it{d\/}}) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-gcd-difference-times-hack \\ \index{remainder-gcd-difference-times-!hack}
(({\it{w\/}} $*$ {\it{x\/}}) $\not<$ {\it{z\/}}) $\rightarrow$ (({\it{z\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{x\/}}, ({\it{w\/}} $*$ {\it{x\/}}) $-$ {\it{z\/}})\index{gcd}) $=$ {\tt{0}})
\end{tabbing}

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

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



\noindent{\sc Event}:   Let us define the theory {\it{addition}} to consist of the following events: equal-plus-0,
equal-difference-0,
commutativity-of-plus,
commutativity2-of-plus,
plus-zero-arg2,
plus-add1-arg2,
plus-add1-arg1,
associativity-of-plus,
plus-difference-arg1,
plus-difference-arg2,
diff-diff-arg1,
diff-diff-arg2,
correctness-of-cancel-equal-plus,
correctness-of-cancel-difference-plus,
difference-elim,
difference-leq-arg1,
difference-add1-arg2,
difference-sub1-arg2,
difference-difference-arg1,
difference-difference-arg2,
difference-x-x,
correctness-of-cancel-lessp-plus.\index{addition}

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{multiplication}} to consist of the following events: equal-times-0,
equal-times-1,
equal-sub1-0,
times-zero,
times-add1,
commutativity-of-times,
times-distributes-over-plus,
commutativity2-of-times,
associativity-of-times,
times-distributes-over-difference,
times-quotient,
times-1-arg1,
lessp-times1,
lessp-times2,
lessp-times3,
lessp-plus-times1,
lessp-plus-times2,
lessp-1-times,
correctness-of-cancel-lessp-times,
correctness-of-cancel-equal-times,
equal-times-x-x.\index{multiplication}

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{remainders}} to consist of the following events: lessp-remainder,
remainder-noop,
remainder-of-non-number,
remainder-zero,
remainder-quotient-elim,
remainder-add1,
remainder-plus,
equal-remainder-plus-0,
remainder-times1,
remainder-times1-instance,
remainder-times2,
remainder-times2-instance,
remainder-difference1,
remainder-difference2,
remainder-plus-times-times,
remainder-plus-times-times-instance,
remainder-remainder,
remainder-1-arg1,
remainder-1-arg2,
remainder-x-x,
remainder-quotient-gcd-0,
remainder-gcd-0,
remainder-gcd-arg1,
remainder-diff1,
remainder-diff2.\index{remainders}

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{quotients}} to consist of the following events: quotient-noop,
quotient-of-non-number,
quotient-zero,
quotient-add1,
equal-quotient-0,
quotient-sub1,
quotient-plus,
quotient-times,
quotient-times-instance,
quotient-difference1,
quotient-lessp-arg1,
quotient-difference2,
quotient-difference3,
quotient-remainder-times,
quotient-remainder,
quotient-remainder-instance,
quotient-plus-times-times,
quotient-plus-times-times-instance,
quotient-quotient,
quotient-1-arg2,
quotient-1-arg1,
quotient-x-x,
lessp-quotient,
correctness-of-cancel-quotient-times,
quotient-difference.\index{quotients}

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{exponentiation}} to consist of the following events: equal-exp-0,
equal-exp-1,
exp-exp,
exp-add1,
exp-times,
exp-1-arg1,
exp-zero,
exp-0-arg2,
exp-0-arg1,
exp-difference,
exp-plus,
quotient-exp,
remainder-exp-exp,
remainder-exp.\index{exponentiation}

\addvspace{18pt}


\noindent{\sc Event}:   Let us define the theory {\it{logs}} to consist of the following events: log-exp,
log-times-exp,
log-times,
log-quotient-exp,
log-quotient-times,
log-quotient,
log-1,
log-0,
equal-log-0,
exp-exp.\index{logs}

\addvspace{18pt}



\noindent{\sc Event}:   Let us define the theory {\it{gcds}} to consist of the following events: commutativity2-of-gcd,
associativity-of-gcd,
common-divisor-divides-gcd,
distributivity-of-times-over-gcd,
lessp-gcd,
equal-gcd-0,
gcd-idempotence,
gcd-x-x,
remainder-gcd,
gcd-plus,
gcd-plus-instance,
gcd-1,
commutativity-of-gcd,
gcd-zero,
lessp-gcd2,
gcd-times,
gcd-remainder,
equal-x-gcd-x-y,
equal-gcd-gcd-as-remainder,
remainder-gcd-0-means,
gcd-quotient-gcd,
gcd-difference1,
gcd-difference2.\index{gcds}

\addvspace{18pt}



\noindent{\sc Event}:   Let us define the theory {\it{naturals}} to consist of the following events: addition,
multiplication,
remainders,
quotients,
exponentiation,
logs,
gcds.\index{naturals}

\addvspace{18pt}


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

\addvspace{18pt}

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