\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 Yuan Yu.  All Rights Reserved.

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

 NO WARRANTY

 Yuan Yu 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 Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
 LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
 OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
 OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
 PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
 FOR ANY CLAIM BY ANY OTHER PARTY.

|#

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

\addvspace{18pt}

\begin{verbatim}#|
----------------------------------------------------------------------------
Date:      Jan, 1991
Modified:  May 18, 1992.
File:      mc20-0.events
----------------------------------------------------------------------------
                 
                  AN ARITHMETIC SUBLIBRARY
|#

; before we start to write our specification, some preliminary theories
; have to be established.

;              THEOREMS ABOUT SET AND BAG
; subset relation.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subset} \\  
\=\+{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subset}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subset} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; delete the elements of x from the set y.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{delete} \\  
\=\+{\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{y\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{y\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{y\/}}), {\rm{delete}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{delete})$\;${\bf  endif}\- \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; determines whether x is a subbag of y.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subbagp} \\  
\=\+{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subbagp}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{delete})\index{subbagp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the difference.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bagdiff} \\  
\=\+{\rm{bagdiff}}\,({\it{x\/}}, {\it{y\/}})\index{bagdiff} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{y\/}}) $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{bagdiff}}\,({\rm{delete}}\,({\rm{car}}\,({\it{y\/}}), {\it{x\/}})\index{delete}, {\rm{cdr}}\,({\it{y\/}}))\index{bagdiff} \\ 
{\bf else }{\rm{bagdiff}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{bagdiff}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the intersection.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{bagint} \\  
\=\+{\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}} \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{bagint}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{delete})\index{bagint}) \\ 
{\bf else }{\rm{bagint}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{bagint}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-non-member \\ \index{delete-non-member}
({\it{x\/}} $\not\in$ {\it{y\/}}) $\rightarrow$ ({\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete} $=$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-delete \\ \index{member-delete}
({\it{x\/}} $\in$ {\rm{delete}}\,({\it{u\/}}, {\it{v\/}})\index{delete}) $\rightarrow$ ({\it{x\/}} $\in$ {\it{v\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete-commutativity \\ \index{delete-commutativity}
{\rm{delete}}\,({\it{x\/}}, {\rm{delete}}\,({\it{y\/}}, {\it{z\/}})\index{delete})\index{delete} $=$ {\rm{delete}}\,({\it{y\/}}, {\rm{delete}}\,({\it{x\/}}, {\it{z\/}})\index{delete})\index{delete}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-delete \\ \index{subbagp-delete}
{\rm{subbagp}}\,({\it{x\/}}, {\rm{delete}}\,({\it{u\/}}, {\it{y\/}})\index{delete})\index{subbagp} $\rightarrow$ {\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-cdr1 \\ \index{subbagp-cdr1}
{\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp} $\rightarrow$ {\rm{subbagp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-cdr2 \\ \index{subbagp-cdr2}
{\rm{subbagp}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{subbagp} $\rightarrow$ {\rm{subbagp}}\,({\it{x\/}}, {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-bagint1 \\ \index{subbagp-bagint1}
{\rm{subbagp}}\,({\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint}, {\it{x\/}})\index{subbagp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subbagp-bagint2 \\ \index{subbagp-bagint2}
{\rm{subbagp}}\,({\rm{bagint}}\,({\it{x\/}}, {\it{y\/}})\index{bagint}, {\it{y\/}})\index{subbagp}
\end{tabbing}

\begin{verbatim};             THEOREMS ABOUT NATURAL NUMBERS
; lemmas about lessp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  lessp-of-1 \\ \index{lessp-of-1}
({\it{x\/}} $<$ {\tt{1}}) $=$ ({\it{x\/}} $\simeq {\tt{0}}$)
\end{tabbing}

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

\begin{verbatim}; lemmas about plus.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
({\tt{1}} $+$ {\it{x\/}}) $=$ ($1\;+$ {\it{x\/}})
\end{tabbing}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  plus-equal-cancel0 \\ \index{plus-equal-cancel0}
(({\it{x\/}} $+$ {\it{y\/}}) $=$ {\it{x\/}}) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  difference-lessp \\ \index{difference-lessp}
(({\it{m\/}} $-$ {\it{n\/}}) $<$ {\it{m\/}}) $=$ (({\it{m\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  difference-lessp1 \\ \index{difference-lessp1}
({\it{x\/}} $<$ {\it{z\/}}) $\rightarrow$ ((({\it{x\/}} $-$ {\it{y\/}}) $<$ {\it{z\/}}) $=$ {\bf{t}})
\end{tabbing}

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

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

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

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

\begin{verbatim}; meta lemmas for plus and difference.  Stolen from basic.events.
\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{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{plus}}) $\rightarrow$ ({\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $\in\;${\bf{N}}${}$)
\end{tabbing}

\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}

\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}

\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}

\begin{tabbing}{\sc Theorem}:  subbagp-implies-plus-tree-geq \\ \index{subbagp-implies-plus-tree-geq}
{\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}

\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}

\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}

\begin{tabbing}{\sc Theorem}:  bridge-to-subbagp-implies-plus-tree-geq \\ \index{bridge-to-subbagp-implies-plus-t!ree-geq}
\=\+(\=\+{\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}

\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}

\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}

\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}

\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}

\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}

\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}

\begin{verbatim}; the meta lemma to cancel identical plus terms in equality.  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}; the meta lemma to cancel identical plus terms in lessp.  For example,
; (DIFFERENCE (PLUS A B C) (PLUS B D E)) => (DIFFERENCE (PLUS A C) (PLUS D E)).
\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}; the meta lemma to cancel identical plus terms in lessp.  For example,
;   (LESSP (PLUS A B C) (PLUS B D E)) => (LESSP (PLUS A C) (PLUS D E)).
\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{tabbing}{\sc Theorem}:  plus-lessp-cancel-2 \\ \index{plus-lessp-cancel-2}
(({\it{y\/}} $+$ {\it{x\/}}) $<$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $<$ {\it{z\/}})
\end{tabbing}

\begin{verbatim}; lemmas about times.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  times-zero \\ \index{times-zero}
(({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) $=$ ({\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  times-add1-sub1 \\ \index{times-add1-sub1}
\=\+($1\;+$ ({\it{a\/}} $*$ ({\it{b\/}} $-\;1$))) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }({\it{a\/}} $*$ {\it{b\/}}) $-$ ({\it{a\/}} $-\;1$)$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{verbatim}; x is a boolean value, iff x is either T or F.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{boolean}$\;\;$
{\rm{boolean}}\,({\it{x\/}})\index{boolean} $=$ ({\rm{truep}}\,({\it{x\/}}) $\vee$ {\rm{falsep}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-iff \\ \index{equal-iff}
({\rm{boolean}}\,({\it{p\/}})\index{boolean} $\wedge$ {\rm{boolean}}\,({\it{q\/}})\index{boolean}) $\rightarrow$ (({\it{p\/}} $=$ {\it{q\/}}) $=$ ({\it{p\/}} $\leftrightarrow$ {\it{q\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-equal-cancel0 \\ \index{times-equal-cancel0}
\=\+(\=\+(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$(\=\+({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{x\/}} $=$ {\tt{1}}$\;${\bf  endif}\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{y\/}} $*$ {\it{x\/}}) $=$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$(\=\+({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $=$ {\tt{0}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{x\/}} $=$ {\tt{1}}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

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

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

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

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

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


\noindent{\sc Event}:   Disable equal-iff.

\addvspace{18pt}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  times2-add1-lessp-cancel \\ \index{times2-add1-lessp-cancel}
(($1\;+$ ({\tt{2}} $*$ {\it{i\/}})) $<$ ({\tt{2}} $*$ {\it{j\/}})) $=$ ({\it{i\/}} $<$ {\it{j\/}})
\end{tabbing}

\begin{verbatim}; meta lemmas for times.  Stolen and modified from naturals.events.
\end{verbatim}\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{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{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}

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

\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}

\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}

\begin{tabbing}{\sc Theorem}:  eval\$-times-tree-append \\ \index{eval\$-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}

\begin{tabbing}{\sc Theorem}:  times-tree-times-fringe \\ \index{times-tree-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}

\begin{tabbing}{\sc Theorem}:  eval\$-lessp-times-tree-bagdiff \\ \index{eval\$-lessp-times-tree-bagdiff}
\=\+({\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} $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{z\/}})\index{subbagp}) \\ 
$\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}

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

\begin{tabbing}{\sc Theorem}:  and-not-zerop-tree-lessp \\ \index{and-not-zerop-tree-lessp}
{\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\it{x\/}})\index{and-not-zerop-tree}, {\it{a\/}}) $=$ ({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $\not<$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{eval\$-and-not-zerop-tree-end} \\  
\=\+{\rm{eval\$-and-not-zerop-tree-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{eval\$-and-not-zerop-tree-end} \\ 
$=$$\;\;\;\;${\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{and-not-zerop-tree}, {\it{a\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  and-not-zerop-tree-delete \\ \index{and-not-zerop-tree-delete}
\=\+({\it{w\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{eval\$}}\,({\bf{t}}, {\rm{and-not-zerop-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{and-not-zerop-tree}, {\it{a\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}}) $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{eval\$-and-not-zerop-tree-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{eval\$-and-not-zerop-tree-end} \\ 
{\bf else }{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $\not<$ {\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}})$\;${\bf  endif}\-)\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable and-not-zerop-tree-lessp.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{lessp-1-times-tree-delete-end} \\  
\=\+{\rm{lessp-1-times-tree-delete-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{lessp-1-times-tree-delete-end} \\ 
$=$$\;\;\;\;$({\tt{1}} $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{times-tree}, {\it{a\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-1-times-tree-delete \\ \index{lessp-1-times-tree-delete}
\=\+({\it{w\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\tt{1}} $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{times-tree}, {\it{a\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}}) $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{lessp-1-times-tree-delete-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{lessp-1-times-tree-delete-end} \\ 
{\bf else }{\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}}) $<$ {\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval\$-times-fringe-member-zero \\ \index{eval\$-times-fringe-member-zero}
\=\+(({\it{e\/}} $\in$ {\rm{times-fringe}}\,({\rm{cons}}\,({\tt{'}}{\tt{times}}, {\it{x\/}}))\index{times-fringe}) $\wedge$ ({\rm{eval\$}}\,({\bf{t}}, {\it{e\/}}, {\it{a\/}}) $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{eval\$}}\,({\bf{t}}, {\rm{car}}\,({\it{x\/}}), {\it{a\/}}) $*$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cadr}}\,({\it{x\/}}), {\it{a\/}})) $=$ {\tt{0}})\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{cancel-lessp-times} \\  
\=\+{\rm{cancel-lessp-times}}\,({\it{x\/}})\index{cancel-lessp-times} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{lessp}}) \\ 
{\bf then }\=\+{\bf if }({\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 elseif }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{x\/}}) $\in$ {\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{caddr}}\,({\it{x\/}}))), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{not}}, \\ 
{\rm{and-not-zerop-tree}}\,({\rm{delete}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe})\-\index{delete})\index{and-not-zerop-tree})\-)\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{x\/}}) $\in$ {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{list}}\,({\tt{'}}{\tt{zerop}}, {\rm{cadr}}\,({\it{x\/}}))), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{lessp}}, \\ 
{\tt{'}}{\tt{'}}{\tt{1}}, \\ 
{\rm{times-tree}}\,({\rm{delete}}\,({\rm{cadr}}\,({\it{x\/}}), {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\index{delete})\index{times-tree})\-)\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the meta lemma to cancel identical times terms in lessp. For example,
; (lessp (times b (times c d)) (times b d)) =>
;         (and (and (not (zerop b)) (not (zerop d))) (lessp (fix c) 1))
\end{verbatim}\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}


\noindent{\sc Event}:   Disable and-not-zerop-tree-delete.

\addvspace{18pt}

\noindent{\sc Event}:   Disable lessp-1-times-tree-delete.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  eval\$-equal-times-tree-bagdiff \\ \index{eval\$-equal-times-tree-bagdiff}
\=\+({\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} $\wedge$ {\rm{subbagp}}\,({\it{x\/}}, {\it{z\/}})\index{subbagp}) \\ 
$\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}

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

\begin{tabbing}{\sc Definition}:\index{equal-1-eval\$-times-tree-delete!-end} \\  
\=\+{\rm{equal-1-eval\$-times-tree-delete-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{equal-1-eval\$-times-tree-delete!-end} \\ 
$=$$\;\;\;\;$({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{times-tree}, {\it{a\/}}) $=$ {\tt{1}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equal-1-times-tree-delete \\ \index{equal-1-times-tree-delete}
\=\+({\it{w\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\rm{delete}}\,({\it{w\/}}, {\it{x\/}})\index{delete})\index{times-tree}, {\it{a\/}}) $=$ {\tt{1}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}}) $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{equal-1-eval\$-times-tree-delete-end}}\,({\it{w\/}}, {\it{x\/}}, {\it{a\/}})\index{equal-1-eval\$-times-tree-delete!-end} \\ 
{\bf else }{\rm{eval\$}}\,({\bf{t}}, {\rm{times-tree}}\,({\it{x\/}})\index{times-tree}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\it{w\/}}, {\it{a\/}})$\;${\bf  endif}\-)\-\-
\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}} \\ 
{\bf then }\=\+{\bf if }({\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{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})\-, \\ 
{\tt{'}}{\tt{(}}{\tt{true}}{\tt{)}})\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caadr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{x\/}}) $\in$ {\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{numberp}}, {\rm{caddr}}\,({\it{x\/}})), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{or}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{equal}}, {\rm{caddr}}\,({\it{x\/}}), {\tt{'}}{\tt{'}}{\tt{0}}), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\rm{times-tree}}\,({\rm{delete}}\,(\=\+{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{times-fringe}}\,({\rm{cadr}}\,({\it{x\/}}))\index{times-fringe})\-\index{delete})\index{times-tree}, \\ 
{\tt{'}}{\tt{'}}{\tt{1}})\-)\-)\- \\ 
{\bf elseif }\=\+{\rm{listp}}\,({\rm{caddr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{caaddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{times}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{x\/}}) $\in$ {\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\- \\ 
{\bf then }{\rm{list}}\,(\=\+{\tt{'}}{\tt{and}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{numberp}}, {\rm{cadr}}\,({\it{x\/}})), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{or}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{equal}}, {\rm{cadr}}\,({\it{x\/}}), {\tt{'}}{\tt{'}}{\tt{0}}), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{equal}}, \\ 
{\rm{times-tree}}\,({\rm{delete}}\,(\=\+{\rm{cadr}}\,({\it{x\/}}), \\ 
{\rm{times-fringe}}\,({\rm{caddr}}\,({\it{x\/}}))\index{times-fringe})\-\index{delete})\index{times-tree}, \\ 
{\tt{'}}{\tt{'}}{\tt{1}})\-)\-)\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; the meta lemma to cancel identical times term in equality.  For example,
;     (equal (times b (times c d)) (times b d)) =>
;          (or (or (zerop b) (zerop d)) (equal (fix c) 1))
\end{verbatim}\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}


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

\addvspace{18pt}

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

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

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

\begin{tabbing}{\sc Theorem}:  exp-plus \\ \index{exp-plus}
({\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp} $*$ {\rm{exp}}\,({\it{x\/}}, {\it{z\/}})\index{exp}) $=$ {\rm{exp}}\,({\it{x\/}}, {\it{y\/}} $+$ {\it{z\/}})\index{exp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  exp-exp \\ \index{exp-exp}
{\rm{exp}}\,({\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp}, {\it{z\/}})\index{exp} $=$ {\rm{exp}}\,({\it{x\/}}, {\it{y\/}} $*$ {\it{z\/}})\index{exp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-of-2-0 \\ \index{exp-of-2-0}
({\it{m\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{exp}}\,({\it{m\/}}, {\it{n\/}})\index{exp} $\not<$ {\tt{1}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-of-2-1 \\ \index{exp-of-2-1}
({\tt{1}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}) $=$ ({\it{n\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  exp-lessp \\ \index{exp-lessp}
\=\+({\rm{exp}}\,({\it{x\/}}, {\it{y\/}})\index{exp} $<$ {\rm{exp}}\,({\it{x\/}}, {\it{z\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{z\/}} $\simeq {\tt{0}}$) \\ 
{\bf elseif }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{y\/}} $<$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable times.

\addvspace{18pt}

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

\begin{verbatim}; lemmas about remainder and quotient.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-exit \\ \index{remainder-exit}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ (({\it{i\/}} ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ {\rm{fix}}\,({\it{i\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-exit \\ \index{quotient-exit}
({\it{i\/}} $<$ {\it{j\/}}) $\rightarrow$ (({\it{i\/}} $\div$ {\it{j\/}}) $=$ {\tt{0}})
\end{tabbing}

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

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

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

\begin{tabbing}{\sc Theorem}:  quotient-1 \\ \index{quotient-1}
\=\+(\=\+({\tt{1}} $\div$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(({\it{m\/}} $\div$ {\tt{1}}) $=$ {\rm{fix}}\,({\it{m\/}}))\-
\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}:  quotient-x-x \\ \index{quotient-x-x}
\=\+({\it{x\/}} $\div$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

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

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

\begin{verbatim}; A generalization lemma about quotient. 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  quotient-generalize \\ \index{quotient-generalize}
\=\+(({\it{m\/}} $\div$ {\it{n\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{m\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{n\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\it{m\/}} $<$ {\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}


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

\addvspace{18pt}

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

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

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

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

\begin{tabbing}{\sc Theorem}:  quotient-leq \\ \index{quotient-leq}
{\it{i\/}} $\not<$ ({\it{i\/}} $\div$ {\it{j\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-wrt-2 \\ \index{remainder-wrt-2}
({\it{n\/}} ${}${\bf{mod}}${}$ {\tt{2}}) $<$ {\tt{2}}
\end{tabbing}

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  remainder-plus-add1 \\ \index{remainder-plus-add1}
(({\it{i\/}} ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ {\tt{0}}) $\rightarrow$ ((($1\;+$ ({\it{x\/}} $+$ {\it{i\/}})) ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ (($1\;+$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{j\/}}))
\end{tabbing}

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

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

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

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

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

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

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

\begin{tabbing}{\sc Theorem}:  quotient-plus1 \\ \index{quotient-plus1}
(({\it{i\/}} ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{x\/}} $+$ {\it{i\/}}) $\div$ {\it{j\/}}) $=$ (({\it{x\/}} $\div$ {\it{j\/}}) $+$ ({\it{i\/}} $\div$ {\it{j\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-plus2 \\ \index{quotient-plus2}
(({\it{i\/}} ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ {\tt{0}}) $\rightarrow$ ((({\it{i\/}} $+$ {\it{x\/}}) $\div$ {\it{j\/}}) $=$ (({\it{i\/}} $\div$ {\it{j\/}}) $+$ ({\it{x\/}} $\div$ {\it{j\/}})))
\end{tabbing}

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

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

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

\begin{tabbing}{\sc Theorem}:  quotient-plus-add1 \\ \index{quotient-plus-add1}
\=\+(({\it{i\/}} ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$((($1\;+$ ({\it{x\/}} $+$ {\it{i\/}})) $\div$ {\it{j\/}}) $=$ ((($1\;+$ {\it{x\/}}) $\div$ {\it{j\/}}) $+$ ({\it{i\/}} $\div$ {\it{j\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-difference-plus1 \\ \index{quotient-difference-plus1}
\=\+(({\it{x\/}} $\not<$ {\it{z\/}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{w\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{z\/}}) $\div$ {\it{w\/}}) $=$ ((({\it{x\/}} $-$ {\it{z\/}}) $\div$ {\it{w\/}}) $+$ ({\it{y\/}} $\div$ {\it{w\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-difference-plus2 \\ \index{quotient-difference-plus2}
\=\+(({\it{y\/}} $\not<$ {\it{z\/}}) $\wedge$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{w\/}}) $=$ {\tt{0}})) \\ 
$\rightarrow$$\;\;\;\;$(((({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{z\/}}) $\div$ {\it{w\/}}) $=$ ((({\it{y\/}} $-$ {\it{z\/}}) $\div$ {\it{w\/}}) $+$ ({\it{x\/}} $\div$ {\it{w\/}})))\-
\end{tabbing}

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

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

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


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

\addvspace{18pt}

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

\addvspace{18pt}
			      
\begin{tabbing}{\sc Theorem}:  remainder-sub1 \\ \index{remainder-sub1}
\=\+(({\it{m\/}} $-\;1$) ${}${\bf{mod}}${}$ {\it{n\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{m\/}} $-\;1$ \\ 
{\bf elseif }({\it{m\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\tt{0}} \\ 
{\bf then }\=\+{\bf if }{\it{m\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\it{n\/}} $-\;1$$\;${\bf  endif}\- \\ 
{\bf else }({\it{m\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $-\;1$$\;${\bf  endif}\-\-
\end{tabbing}

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

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

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

\begin{tabbing}{\sc Theorem}:  quotient-add1 \\ \index{quotient-add1}
\=\+(($1\;+$ {\it{m\/}}) $\div$ {\it{n\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{m\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ ({\it{n\/}} $-\;1$)$\;\;${\bf then }$1\;+$ ({\it{m\/}} $\div$ {\it{n\/}}) \\ 
{\bf else }{\it{m\/}} $\div$ {\it{n\/}}$\;${\bf  endif}\-\-
\end{tabbing}
	     
\begin{tabbing}{\sc Theorem}:  times-plus-lessp \\ \index{times-plus-lessp}
({\it{x\/}} $<$ {\it{d\/}}) $\rightarrow$ ((({\it{x\/}} $+$ ({\it{b\/}} $*$ {\it{d\/}})) $<$ ({\it{c\/}} $*$ {\it{d\/}})) $=$ ({\it{b\/}} $<$ {\it{c\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-shrink-fast \\ \index{quotient-shrink-fast}
{\it{x\/}} $\not<$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))
\end{tabbing}

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

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

\begin{tabbing}{\sc Theorem}:  remainder-plus-remainder2 \\ \index{remainder-plus-remainder2}
(({\it{x\/}} $+$ {\it{y\/}} $+$ ({\it{z\/}} ${}${\bf{mod}}${}$ {\it{k\/}})) ${}${\bf{mod}}${}$ {\it{k\/}}) $=$ (({\it{x\/}} $+$ {\it{y\/}} $+$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{k\/}})
\end{tabbing}

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

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

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

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

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


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

\addvspace{18pt}

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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  remainder-distributes-times2-add1 \\ \index{remainder-distributes-times2-ad!d1}
(($1\;+$ ({\tt{2}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ ({\tt{2}} $*$ {\it{z\/}})) $=$ ($1\;+$ ({\tt{2}} $*$ ({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}})))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-distributes-times2-add1 \\ \index{quotient-distributes-times2-add!1}
(($1\;+$ ({\tt{2}} $*$ {\it{y\/}})) $\div$ ({\tt{2}} $*$ {\it{z\/}})) $=$ ({\it{y\/}} $\div$ {\it{z\/}})
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  remainder-exp \\ \index{remainder-exp}
\=\+({\tt{1}} $<$ {\it{i\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\it{i\/}}, {\it{k\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $<$ {\it{k\/}}$\;\;${\bf then }{\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-cancel0 \\ \index{remainder-plus-cancel0}
\=\+((({\it{i\/}} $+$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\it{i\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{j\/}} $\simeq {\tt{0}}$) \\ 
{\bf elseif }{\it{i\/}} $<$ {\it{n\/}}$\;\;${\bf then }({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ {\tt{0}}) \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-plus-cancel \\ \index{remainder-plus-cancel}
((({\it{i\/}} $+$ {\it{j\/}}) ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ (({\it{i\/}} $+$ {\it{k\/}}) ${}${\bf{mod}}${}$ {\it{n\/}})) $=$ (({\it{j\/}} ${}${\bf{mod}}${}$ {\it{n\/}}) $=$ ({\it{k\/}} ${}${\bf{mod}}${}$ {\it{n\/}}))
\end{tabbing}

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

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

\begin{verbatim}; we redefine the distribution law of times and plus, and disable the old one.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  times-distributes-plus-new \\ \index{times-distributes-plus-new}
(({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}})) $=$ ({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}}))
\end{tabbing}


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

\addvspace{18pt}

\begin{verbatim}; an induction hint for the next event.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{quot2-sub12-induct} \\  
\=\+{\rm{quot2-sub12-induct}}\,({\it{x\/}}, {\it{y\/}}, {\it{i\/}}, {\it{j\/}})\index{quot2-sub12-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{quot2-sub12-induct}}\,({\it{x\/}} $\div$ {\tt{2}}, {\it{y\/}} $\div$ {\tt{2}}, {\it{i\/}} $-\;1$, {\it{j\/}} $-\;1$)\index{quot2-sub12-induct}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus-times-exp2 \\ \index{lessp-plus-times-exp2}
\=\+({\it{x\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(({\it{x\/}} $+$ ({\it{y\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp})) $<$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp} \\ 
{\bf else }{\it{y\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}} $-$ {\it{i\/}})\index{exp}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-plus-exp2 \\ \index{lessp-plus-exp2}
({\it{x\/}} $<$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) $\rightarrow$ ((({\it{x\/}} $+$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) $<$ {\rm{exp}}\,({\tt{2}}, {\it{n\/}})\index{exp}) $=$ ({\it{i\/}} $<$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-exp2-1 \\ \index{remainder-times-exp2-1}
(({\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}) $=$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{exp}) $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-exp2-2 \\ \index{remainder-times-exp2-2}
(({\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}) $=$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{exp}) $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp})
\end{tabbing}

\begin{verbatim}; special cases of remainder-times-exp2.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-times-exp2-3 \\ \index{remainder-times-exp2-3}
\=\+(\=\+(({\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) ${}${\bf{mod}}${}$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  remainder-times-exp2-4 \\ \index{remainder-times-exp2-4}
\=\+(\=\+(({\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\tt{2}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{x\/}} $*$ {\it{y\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) ${}${\bf{mod}}${}$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }({\it{x\/}} $*$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\tt{2}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times-exp2-1 \\ \index{quotient-times-exp2-1}
\=\+(({\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) $\div$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}}$\;\;${\bf then }{\it{x\/}} $\div$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{exp} \\ 
{\bf else }{\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}} $-$ {\it{j\/}})\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times-exp2-2 \\ \index{quotient-times-exp2-2}
\=\+(({\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} $*$ {\it{x\/}}) $\div$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}}$\;\;${\bf then }{\it{x\/}} $\div$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}} $-$ {\it{i\/}})\index{exp} \\ 
{\bf else }{\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}} $-$ {\it{j\/}})\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  quotient-times-exp2-3 \\ \index{quotient-times-exp2-3}
\=\+(\=\+(({\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) $\div$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} $\div$ {\tt{2}} \\ 
{\bf else }{\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}} $-\;1$)\index{exp}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} $*$ {\it{x\/}}) $\div$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} $\div$ {\tt{2}} \\ 
{\bf else }{\it{x\/}} $*$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}} $-\;1$)\index{exp}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  remainder-remainder-exp2 \\ \index{remainder-remainder-exp2}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $<$ {\it{j\/}}$\;\;${\bf then }{\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp} \\ 
{\bf else }{\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{j\/}})\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; a lemma for the event add-evenp.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  remainder-remainder-2 \\ \index{remainder-remainder-2}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{exp}}\,({\tt{2}}, {\it{i\/}})\index{exp}) ${}${\bf{mod}}${}$ {\tt{2}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; logarithm is not used in the specification or the lemma library.  It 
; comes in when we'd like to reason about the time complexity of programs. 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  times-lessp \\ \index{times-lessp}
\=\+({\it{x\/}} $\leq$ {\it{z\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{x\/}} $<$ ({\it{y\/}} $*$ {\it{z\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{y\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{z\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{y\/}} $=$ {\tt{1}}$\;\;${\bf then }{\it{x\/}} $<$ {\it{z\/}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  log-of-0 \\ \index{log-of-0}
{\rm{log}}\,({\it{b\/}}, {\tt{0}})\index{log} $=$ {\tt{0}}
\end{tabbing}

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

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

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

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

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

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

\begin{tabbing}{\sc Definition}:\index{quotient2-induct} \\  
\=\+{\rm{quotient2-induct}}\,({\it{b\/}}, {\it{x\/}}, {\it{y\/}})\index{quotient2-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{b\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{b\/}} $=$ {\tt{1}})$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{quotient2-induct}}\,({\it{b\/}}, {\it{x\/}} $\div$ {\it{b\/}}, {\it{y\/}} $\div$ {\it{b\/}})\index{quotient2-induct}$\;${\bf  endif}\-\-
\end{tabbing}
	  
\begin{tabbing}{\sc Theorem}:  log-leq \\ \index{log-leq}
({\it{x\/}} $\leq$ {\it{y\/}}) $\rightarrow$ ({\rm{log}}\,({\it{b\/}}, {\it{y\/}})\index{log} $\not<$ {\rm{log}}\,({\it{b\/}}, {\it{x\/}})\index{log})
\end{tabbing}

\begin{verbatim}; these two lemmas are useful in time analysis.
\end{verbatim}\begin{tabbing}{\sc Theorem}:  ta-lemma-1 \\ \index{ta-lemma-1}
({\it{a\/}} $\leq$ {\it{a1\/}}) $\rightarrow$ (({\it{x\/}} $+$ ({\it{y\/}} $*$ {\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log})) $\leq$ ({\it{x\/}} $+$ ({\it{y\/}} $*$ {\rm{log}}\,({\tt{2}}, {\it{a1\/}})\index{log})))
\end{tabbing}
			  
\begin{tabbing}{\sc Theorem}:  ta-lemma-2 \\ \index{ta-lemma-2}
\=\+(({\it{a\/}} $\leq$ {\it{a1\/}}) $\wedge$ ({\it{b\/}} $\leq$ {\it{b1\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{x\/}} $+$ ({\it{y\/}} $*$ ({\rm{log}}\,({\tt{2}}, {\it{a\/}})\index{log} $+$ {\rm{log}}\,({\tt{2}}, {\it{b\/}})\index{log}))) \\ 
$\leq$$\;\;\;\;$({\it{x\/}} $+$ ({\it{y\/}} $*$ ({\rm{log}}\,({\tt{2}}, {\it{a1\/}})\index{log} $+$ {\rm{log}}\,({\tt{2}}, {\it{b1\/}})\index{log}))))\-\-
\end{tabbing}


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

\addvspace{18pt}
%\end{list}
\printindex
\end{document}
