\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

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

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
 EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
 OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
 THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
 PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
 CORRECTION.

 IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
 DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
 CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
 (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
 OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
 POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

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

\addvspace{18pt}

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

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{from-to} \\  
\=\+{\rm{from-to}}\,({\it{i\/}}, {\it{j\/}})\index{from-to} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $<$ {\it{i\/}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{fix}}\,({\it{i\/}}) $=$ {\rm{fix}}\,({\it{j\/}})$\;\;${\bf then }{\rm{list}}\,({\rm{fix}}\,({\it{j\/}})) \\ 
{\bf else }{\rm{append}}\,({\rm{from-to}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)\index{from-to}, {\rm{list}}\,({\it{j\/}}))$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-right-id2 \\ \index{plus-right-id2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $+$ {\it{y\/}}) $=$ {\rm{fix}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
\=\+({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }$1\;+$ ({\it{x\/}} $+$ {\it{y\/}}) \\ 
{\bf else }$1\;+$ {\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity2-of-plus \\ \index{commutativity2-of-plus}
({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $+$ ({\it{x\/}} $+$ {\it{z\/}}))
\end{tabbing} 
\begin{tabbing}{\sc Theorem}:  commutativity-of-plus \\ \index{commutativity-of-plus}
({\it{x\/}} $+$ {\it{y\/}}) $=$ ({\it{y\/}} $+$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-plus \\ \index{associativity-of-plus}
(({\it{x\/}} $+$ {\it{y\/}}) $+$ {\it{z\/}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $+$ {\it{z\/}}))
\end{tabbing} 
\begin{tabbing}{\sc Theorem}:  plus-equal-0 \\ \index{plus-equal-0}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ {\tt{0}}) $=$ (({\it{a\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{b\/}} $\simeq {\tt{0}}$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-x-x \\ \index{difference-x-x}
({\it{x\/}} $-$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-plus \\ \index{difference-plus}
((({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})) $\wedge$ ((({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-cancellation \\ \index{plus-cancellation}
(({\it{a\/}} $+$ {\it{b\/}}) $=$ ({\it{a\/}} $+$ {\it{c\/}})) $=$ ({\rm{fix}}\,({\it{b\/}}) $=$ {\rm{fix}}\,({\it{c\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-0 \\ \index{difference-0}
({\it{y\/}} $\not<$ {\it{x\/}}) $\rightarrow$ (({\it{x\/}} $-$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-difference-0 \\ \index{equal-difference-0}
({\tt{0}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ ({\it{y\/}} $\not<$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-cancellation-0 \\ \index{difference-cancellation-0}
({\it{x\/}} $=$ ({\it{x\/}} $-$ {\it{y\/}})) $=$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$)))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-cancellation-1 \\ \index{difference-cancellation-1}
\=\+(({\it{x\/}} $-$ {\it{y\/}}) $=$ ({\it{z\/}} $-$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{z\/}} \\ 
{\bf elseif }{\it{z\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\it{y\/}} $\not<$ {\it{x\/}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{z\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc 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{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{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{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}:  commutativity-of-delete \\ \index{commutativity-of-delete}
{\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{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 Definition}:\index{cancel} \\  
\=\+{\rm{cancel}}\,({\it{x\/}})\index{cancel} \\ 
$=$$\;\;\;\;$\=\+{\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}

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

\addvspace{18pt}
\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}
\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-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}
\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-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}
\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{tabbing}{\sc Theorem}:  correctness-of-cancel \\ \index{correctness-of-cancel}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{cancel}}\,({\it{x\/}})\index{cancel}, {\it{a\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{reverse} \\  
\=\+{\rm{reverse}}\,({\it{x\/}})\index{reverse} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{reverse}}\,({\rm{cdr}}\,({\it{x\/}}))\index{reverse}, {\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\bf{nil}})) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-append \\ \index{associativity-of-append}
{\rm{append}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{z\/}}) $=$ {\rm{append}}\,({\it{x\/}}, {\rm{append}}\,({\it{y\/}}, {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{plistp} \\  
\=\+{\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{x\/}} $=$ {\bf{nil}} \\ 
{\bf else }{\rm{plistp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{plistp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  append-right-id \\ \index{append-right-id}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{append}}\,({\it{x\/}}, {\bf{nil}}) $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plistp-reverse \\ \index{plistp-reverse}
{\rm{plistp}}\,({\rm{reverse}}\,({\it{x\/}})\index{reverse})\index{plistp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  append-reverse \\ \index{append-reverse}
{\rm{reverse}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{reverse} $=$ {\rm{append}}\,({\rm{reverse}}\,({\it{b\/}})\index{reverse}, {\rm{reverse}}\,({\it{a\/}})\index{reverse})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-zero2 \\ \index{times-zero2}
({\it{y\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  distributivity-of-times-over-plus \\ \index{distributivity-of-times-over-pl!us}
({\it{x\/}} $*$ ({\it{y\/}} $+$ {\it{z\/}})) $=$ (({\it{x\/}} $*$ {\it{y\/}}) $+$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
\=\+({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}) \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity-of-times \\ \index{commutativity-of-times}
({\it{x\/}} $*$ {\it{y\/}}) $=$ ({\it{y\/}} $*$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity2-of-times \\ \index{commutativity2-of-times}
({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ ({\it{y\/}} $*$ ({\it{x\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-times \\ \index{associativity-of-times}
(({\it{x\/}} $*$ {\it{y\/}}) $*$ {\it{z\/}}) $=$ ({\it{x\/}} $*$ ({\it{y\/}} $*$ {\it{z\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-times-0 \\ \index{equal-times-0}
(({\it{x\/}} $*$ {\it{y\/}}) $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}

\noindent{\sc Event}:   Add the shell {\it{push\/}}\index{push}, with recognizer function symbol {\it{stackp\/}} and 2 accessors: {\it{top\/}}, with type restriction (none-of) and default value zero; {\it{pop\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}

\begin{tabbing}{\sc Conservative Axiom}:  numberp-call \\ \index{numberp-call}
{\rm{call}}\,({\it{fn\/}}, {\it{x\/}}, {\it{y\/}})\index{call} $\in\;${\bf{N}}${}$
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it call\/} and {\it getvalue\/}.
\begin{tabbing}{\sc Definition}:\index{expressionp} \\  
\=\+{\rm{expressionp}}\,({\it{x\/}})\index{expressionp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{x\/}}))$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cddr}}\,({\it{x\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{expressionp}}\,({\rm{cadr}}\,({\it{x\/}}))\index{expressionp}$\;\;${\bf then }{\rm{expressionp}}\,({\rm{caddr}}\,({\it{x\/}}))\index{expressionp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cadr-crock \\ \index{cadr-crock}
{\rm{listp}}\,({\rm{cddr}}\,({\it{x\/}})) $\rightarrow$ ({\rm{count}}\,({\rm{cadr}}\,({\it{x\/}})) $<$ {\rm{count}}\,({\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{term-eval} \\  
\=\+{\rm{term-eval}}\,({\it{form\/}}, {\it{envrn\/}})\index{term-eval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{form\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{form\/}} \\ 
{\bf elseif }{\rm{listp}}\,({\rm{cddr}}\,({\it{form\/}})) \\ 
{\bf then }{\rm{call}}\,(\=\+{\rm{car}}\,({\it{form\/}}), \\ 
{\rm{term-eval}}\,({\rm{cadr}}\,({\it{form\/}}), {\it{envrn\/}})\index{term-eval}, \\ 
{\rm{term-eval}}\,({\rm{caddr}}\,({\it{form\/}}), {\it{envrn\/}})\index{term-eval})\-\index{call} \\ 
{\bf else }{\rm{getvalue}}\,({\it{form\/}}, {\it{envrn\/}})\index{getvalue}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{optimize} \\  
\=\+{\rm{optimize}}\,({\it{form\/}})\index{optimize} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\rm{cddr}}\,({\it{form\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{optimize}}\,({\rm{cadr}}\,({\it{form\/}}))\index{optimize} $\in\;${\bf{N}}${}$ \\ 
{\bf then }\=\+{\bf if }{\rm{optimize}}\,({\rm{caddr}}\,({\it{form\/}}))\index{optimize} $\in\;${\bf{N}}${}$ \\ 
{\bf then }{\rm{call}}\,(\=\+{\rm{car}}\,({\it{form\/}}), \\ 
{\rm{optimize}}\,({\rm{cadr}}\,({\it{form\/}}))\index{optimize}, \\ 
{\rm{optimize}}\,({\rm{caddr}}\,({\it{form\/}}))\index{optimize})\-\index{call} \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{car}}\,({\it{form\/}}), \\ 
{\rm{optimize}}\,({\rm{cadr}}\,({\it{form\/}}))\index{optimize}, \\ 
{\rm{optimize}}\,({\rm{caddr}}\,({\it{form\/}}))\index{optimize})\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{list}}\,(\=\+{\rm{car}}\,({\it{form\/}}), \\ 
{\rm{optimize}}\,({\rm{cadr}}\,({\it{form\/}}))\index{optimize}, \\ 
{\rm{optimize}}\,({\rm{caddr}}\,({\it{form\/}}))\index{optimize})\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{form\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{codegen} \\  
\=\+{\rm{codegen}}\,({\it{form\/}}, {\it{ins\/}})\index{codegen} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{form\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{pushi}}, {\it{form\/}}), {\it{ins\/}}) \\ 
{\bf elseif }{\rm{listp}}\,({\rm{cddr}}\,({\it{form\/}})) \\ 
{\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{form\/}}), {\rm{codegen}}\,({\rm{caddr}}\,({\it{form\/}}), {\rm{codegen}}\,({\rm{cadr}}\,({\it{form\/}}), {\it{ins\/}})\index{codegen})\index{codegen}) \\ 
{\bf else }{\rm{cons}}\,({\rm{list}}\,({\tt{'}}{\tt{pushv}}, {\it{form\/}}), {\it{ins\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{compile} \\  
{\rm{compile}}\,({\it{form\/}})\index{compile} $=$ {\rm{reverse}}\,({\rm{codegen}}\,({\rm{optimize}}\,({\it{form\/}})\index{optimize}, {\bf{nil}})\index{codegen})\index{reverse}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  formp-optimize \\ \index{formp-optimize}
{\rm{expressionp}}\,({\it{x\/}})\index{expressionp} $\rightarrow$ {\rm{expressionp}}\,({\rm{optimize}}\,({\it{x\/}})\index{optimize})\index{expressionp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-optimize \\ \index{correctness-of-optimize}
{\rm{expressionp}}\,({\it{x\/}})\index{expressionp} $\rightarrow$ ({\rm{term-eval}}\,({\rm{optimize}}\,({\it{x\/}})\index{optimize}, {\it{envrn\/}})\index{term-eval} $=$ {\rm{term-eval}}\,({\it{x\/}}, {\it{envrn\/}})\index{term-eval})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{exec} \\  
\=\+{\rm{exec}}\,({\it{pc\/}}, {\it{pds\/}}, {\it{envrn\/}})\index{exec} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{pc\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{pds\/}} \\ 
{\bf elseif }{\rm{listp}}\,({\rm{car}}\,({\it{pc\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{caar}}\,({\it{pc\/}}) $=$ {\tt{'}}{\tt{pushi}} \\ 
{\bf then }{\rm{exec}}\,({\rm{cdr}}\,({\it{pc\/}}), {\rm{push}}\,({\rm{cadar}}\,({\it{pc\/}}), {\it{pds\/}})\index{push}, {\it{envrn\/}})\index{exec} \\ 
{\bf else }{\rm{exec}}\,(\=\+{\rm{cdr}}\,({\it{pc\/}}), \\ 
{\rm{push}}\,({\rm{getvalue}}\,({\rm{cadar}}\,({\it{pc\/}}), {\it{envrn\/}})\index{getvalue}, {\it{pds\/}})\index{push}, \\ 
{\it{envrn\/}})\-\index{exec}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{exec}}\,(\=\+{\rm{cdr}}\,({\it{pc\/}}), \\ 
{\rm{push}}\,(\=\+{\rm{call}}\,({\rm{car}}\,({\it{pc\/}}), {\rm{top}}\,({\rm{pop}}\,({\it{pds\/}})\index{pop})\index{top}, {\rm{top}}\,({\it{pds\/}})\index{top})\index{call}, \\ 
{\rm{pop}}\,({\rm{pop}}\,({\it{pds\/}})\index{pop})\index{pop})\-\index{push}, \\ 
{\it{envrn\/}})\-\index{exec}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sequential-execution \\ \index{sequential-execution}
{\rm{exec}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}), {\it{pds\/}}, {\it{envrn\/}})\index{exec} $=$ {\rm{exec}}\,({\it{y\/}}, {\rm{exec}}\,({\it{x\/}}, {\it{pds\/}}, {\it{envrn\/}})\index{exec}, {\it{envrn\/}})\index{exec}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-codegen \\ \index{correctness-of-codegen}
\=\+{\rm{expressionp}}\,({\it{x\/}})\index{expressionp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{exec}}\,({\rm{reverse}}\,({\rm{codegen}}\,({\it{x\/}}, {\it{ins\/}})\index{codegen})\index{reverse}, {\it{pds\/}}, {\it{envrn\/}})\index{exec} \\ 
$=$$\;\;\;\;${\rm{push}}\,({\rm{term-eval}}\,({\it{x\/}}, {\it{envrn\/}})\index{term-eval}, {\rm{exec}}\,({\rm{reverse}}\,({\it{ins\/}})\index{reverse}, {\it{pds\/}}, {\it{envrn\/}})\index{exec})\index{push})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-optimizing-compiler \\ \index{correctness-of-optimizing-compi!ler}
\=\+{\rm{expressionp}}\,({\it{x\/}})\index{expressionp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{exec}}\,({\rm{compile}}\,({\it{x\/}})\index{compile}, {\it{pds\/}}, {\it{envrn\/}})\index{exec} $=$ {\rm{push}}\,({\rm{term-eval}}\,({\it{x\/}}, {\it{envrn\/}})\index{term-eval}, {\it{pds\/}})\index{push})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  transitivity-of-lessp \\ \index{transitivity-of-lessp}
(({\it{x\/}} $<$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $<$ {\it{z\/}})) $\rightarrow$ ({\it{x\/}} $<$ {\it{z\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-not-reflexive \\ \index{lessp-not-reflexive}
{\it{x\/}} $\not<$ {\it{x\/}}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{eqp}$\;\;$
{\rm{eqp}}\,({\it{x\/}}, {\it{y\/}})\index{eqp} $=$ ({\rm{fix}}\,({\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  trichotomy-of-lessp \\ \index{trichotomy-of-lessp}
(($\neg$ {\rm{eqp}}\,({\it{x\/}}, {\it{y\/}})\index{eqp}) $\wedge$ ({\it{y\/}} $\not<$ {\it{x\/}})) $\rightarrow$ ({\it{x\/}} $<$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reverse-reverse \\ \index{reverse-reverse}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{reverse}}\,({\rm{reverse}}\,({\it{x\/}})\index{reverse})\index{reverse} $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{flatten} \\  
\=\+{\rm{flatten}}\,({\it{x\/}})\index{flatten} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{flatten}}\,({\rm{car}}\,({\it{x\/}}))\index{flatten}, {\rm{flatten}}\,({\rm{cdr}}\,({\it{x\/}}))\index{flatten}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{mc-flatten} \\  
\=\+{\rm{mc-flatten}}\,({\it{x\/}}, {\it{y\/}})\index{mc-flatten} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{mc-flatten}}\,({\rm{car}}\,({\it{x\/}}), {\rm{mc-flatten}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{mc-flatten})\index{mc-flatten} \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\it{y\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  flatten-mc-flatten \\ \index{flatten-mc-flatten}
{\rm{mc-flatten}}\,({\it{x\/}}, {\it{y\/}})\index{mc-flatten} $=$ {\rm{append}}\,({\rm{flatten}}\,({\it{x\/}})\index{flatten}, {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-append \\ \index{member-append}
({\it{x\/}} $\in$ {\rm{append}}\,({\it{a\/}}, {\it{b\/}})) $=$ (({\it{x\/}} $\in$ {\it{a\/}}) $\vee$ ({\it{x\/}} $\in$ {\it{b\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-reverse \\ \index{member-reverse}
({\it{x\/}} $\in$ {\rm{reverse}}\,({\it{y\/}})\index{reverse}) $=$ ({\it{x\/}} $\in$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{x\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{x\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-reverse \\ \index{length-reverse}
{\rm{length}}\,({\rm{reverse}}\,({\it{x\/}})\index{reverse})\index{length} $=$ {\rm{length}}\,({\it{x\/}})\index{length}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{intersect} \\  
\=\+{\rm{intersect}}\,({\it{x\/}}, {\it{y\/}})\index{intersect} \\ 
$=$$\;\;\;\;$\=\+{\bf for }{\it{x1\/}}{\bf $\;$ in }{\it{x\/}} \\ 
{\bf when }{\it{x1\/}} $\in$ {\it{y\/}} \\ 
{\bf collect} {\it{x1\/}}$\;${{\bf  endfor}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-intersect \\ \index{member-intersect}
\=\+{\rm{litatom}}\,({\it{v\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{a\/}} $\in$ {\rm{for}}\,(\=\+{\it{v\/}}, \\ 
{\it{lst\/}}, \\ 
{\it{p\/}}, \\ 
{\tt{'}}{\tt{collect}}, \\ 
{\it{v\/}}, \\ 
{\it{alist\/}})\-) \\ 
$=$$\;\;\;\;$(({\it{a\/}} $\in$ {\it{lst\/}}) $\wedge$ {\rm{eval\$}}\,({\bf{t}}, {\it{p\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{v\/}}, {\it{a\/}}), {\it{alist\/}}))))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-union \\ \index{member-union}
({\it{a\/}} $\in$ ({\it{b\/}} $\cup$ {\it{c\/}})) $=$ (({\it{a\/}} $\in$ {\it{b\/}}) $\vee$ ({\it{a\/}} $\in$ {\it{c\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subsetp} \\  
\=\+{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subsetp}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subsetp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-union \\ \index{subsetp-union}
{\rm{subsetp}}\,({\it{a\/}}, {\it{b\/}})\index{subsetp} $\rightarrow$ (({\it{a\/}} $\cup$ {\it{b\/}}) $=$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-intersect \\ \index{subsetp-intersect}
({\rm{plistp}}\,({\it{a\/}})\index{plistp} $\wedge$ {\rm{subsetp}}\,({\it{a\/}}, {\it{b\/}})\index{subsetp}) $\rightarrow$ ({\rm{intersect}}\,({\it{a\/}}, {\it{b\/}})\index{intersect} $=$ {\it{a\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{nth} \\  
\=\+{\rm{nth}}\,({\it{x\/}}, {\it{n\/}})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{nth}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{n\/}} $-\;1$)\index{nth}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{greatereqp}$\;\;$
{\rm{greatereqp}}\,({\it{x\/}}, {\it{y\/}})\index{greatereqp} $=$ ({\it{x\/}} $\not<$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  transitivity-of-leq \\ \index{transitivity-of-leq}
(({\it{x\/}} $\leq$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $\leq$ {\it{z\/}})) $\rightarrow$ ({\it{x\/}} $\leq$ {\it{z\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ordered} \\  
\=\+{\rm{ordered}}\,({\it{l\/}})\index{ordered} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\it{l\/}}) $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{ordered}}\,({\rm{cdr}}\,({\it{l\/}}))\index{ordered}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{addtolist} \\  
\=\+{\rm{addtolist}}\,({\it{x\/}}, {\it{l\/}})\index{addtolist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\it{l\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{addtolist}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{addtolist})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sort} \\  
\=\+{\rm{sort}}\,({\it{l\/}})\index{sort} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\rm{addtolist}}\,({\rm{car}}\,({\it{l\/}}), {\rm{sort}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sort})\index{addtolist} \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{boolean}$\;\;$
{\rm{boolean}}\,({\it{x\/}})\index{boolean} $=$ (({\it{x\/}} $=$ {\bf{t}}) $\vee$ ({\it{x\/}} $=$ {\bf{f}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  iff-equal-equal \\ \index{iff-equal-equal}
({\rm{boolean}}\,({\it{p\/}})\index{boolean} $\wedge$ {\rm{boolean}}\,({\it{q\/}})\index{boolean}) $\rightarrow$ (({\it{p\/}} $\leftrightarrow$ {\it{q\/}}) $=$ ({\it{p\/}} $=$ {\it{q\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nth-0 \\ \index{nth-0}
{\rm{nth}}\,({\tt{0}}, {\it{i\/}})\index{nth} $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nth-nil \\ \index{nth-nil}
\=\+{\rm{nth}}\,({\bf{nil}}, {\it{i\/}})\index{nth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nth-append1 \\ \index{nth-append1}
{\rm{nth}}\,({\it{a\/}}, {\it{i\/}} $+$ {\it{j\/}})\index{nth} $=$ {\rm{nth}}\,({\rm{nth}}\,({\it{a\/}}, {\it{i\/}})\index{nth}, {\it{j\/}})\index{nth}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  associativity-of-equal \\ \index{associativity-of-equal}
\=\+({\rm{boolean}}\,({\it{a\/}})\index{boolean} $\wedge$ ({\rm{boolean}}\,({\it{b\/}})\index{boolean} $\wedge$ {\rm{boolean}}\,({\it{c\/}})\index{boolean})) \\ 
$\rightarrow$$\;\;\;\;$((({\it{a\/}} $=$ {\it{b\/}}) $=$ {\it{c\/}}) $=$ ({\it{a\/}} $=$ ({\it{b\/}} $=$ {\it{c\/}})))\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{odd} \\  
\=\+{\rm{odd}}\,({\it{x\/}})\index{odd} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }({\it{x\/}} $-\;1$) $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{odd}}\,(({\it{x\/}} $-\;1$) $-\;1$)\index{odd}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{even1} \\  
\=\+{\rm{even1}}\,({\it{x\/}})\index{even1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{odd}}\,({\it{x\/}} $-\;1$)\index{odd}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{even2} \\  
\=\+{\rm{even2}}\,({\it{x\/}})\index{even2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }({\it{x\/}} $-\;1$) $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{even2}}\,(({\it{x\/}} $-\;1$) $-\;1$)\index{even2}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{double} \\  
\=\+{\rm{double}}\,({\it{i\/}})\index{double} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ ($1\;+$ {\rm{double}}\,({\it{i\/}} $-\;1$)\index{double})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even1-double \\ \index{even1-double}
{\rm{even1}}\,({\rm{double}}\,({\it{i\/}})\index{double})\index{even1}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{half} \\  
\=\+{\rm{half}}\,({\it{i\/}})\index{half} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }({\it{i\/}} $-\;1$) $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{half}}\,(({\it{i\/}} $-\;1$) $-\;1$)\index{half}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  half-double \\ \index{half-double}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{half}}\,({\rm{double}}\,({\it{i\/}})\index{double})\index{half} $=$ {\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  double-half \\ \index{double-half}
(({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{even1}}\,({\it{i\/}})\index{even1}) $\rightarrow$ ({\rm{double}}\,({\rm{half}}\,({\it{i\/}})\index{half})\index{double} $=$ {\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  double-times-2 \\ \index{double-times-2}
{\rm{double}}\,({\it{i\/}})\index{double} $=$ ({\tt{2}} $*$ {\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subsetp-cons \\ \index{subsetp-cons}
{\rm{subsetp}}\,({\it{x\/}}, {\it{y\/}})\index{subsetp} $\rightarrow$ {\rm{subsetp}}\,({\it{x\/}}, {\rm{cons}}\,({\it{z\/}}, {\it{y\/}}))\index{subsetp}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{last} \\  
\=\+{\rm{last}}\,({\it{x\/}})\index{last} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))$\;\;${\bf then }{\rm{last}}\,({\rm{cdr}}\,({\it{x\/}}))\index{last} \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  last-append \\ \index{last-append}
\=\+{\rm{last}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{last} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{b\/}})$\;\;${\bf then }{\rm{last}}\,({\it{b\/}})\index{last} \\ 
{\bf elseif }{\rm{listp}}\,({\it{a\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\rm{last}}\,({\it{a\/}})\index{last}), {\it{b\/}}) \\ 
{\bf else }{\it{b\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  last-reverse \\ \index{last-reverse}
{\rm{listp}}\,({\it{a\/}}) $\rightarrow$ ({\rm{last}}\,({\rm{reverse}}\,({\it{a\/}})\index{reverse})\index{last} $=$ {\rm{cons}}\,({\rm{car}}\,({\it{a\/}}), {\bf{nil}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{exp} \\  
\=\+{\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{j\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{i\/}} $*$ {\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $-\;1$)\index{exp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-plus \\ \index{exp-plus}
{\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $+$ {\it{k\/}})\index{exp} $=$ ({\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp} $*$ {\rm{exp}}\,({\it{i\/}}, {\it{k\/}})\index{exp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  even1-even2 \\ \index{even1-even2}
{\rm{even1}}\,({\it{x\/}})\index{even1} $=$ {\rm{even2}}\,({\it{x\/}})\index{even2}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-nth \\ \index{leq-nth}
{\rm{length}}\,({\rm{nth}}\,({\it{l\/}}, {\it{i\/}})\index{nth})\index{length} $\leq$ {\rm{length}}\,({\it{l\/}})\index{length}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-sort \\ \index{member-sort}
({\it{a\/}} $\in$ {\rm{sort}}\,({\it{b\/}})\index{sort}) $=$ ({\it{a\/}} $\in$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-sort \\ \index{length-sort}
{\rm{length}}\,({\rm{sort}}\,({\it{a\/}})\index{sort})\index{length} $=$ {\rm{length}}\,({\it{a\/}})\index{length}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{count-list} \\  
\=\+{\rm{count-list}}\,({\it{a\/}}, {\it{l\/}})\index{count-list} \\ 
$=$$\;\;\;\;$\=\+{\bf for }{\it{x\/}}{\bf $\;$ in }{\it{l\/}} \\ 
{\bf count} {\it{a\/}} $=$ {\it{x\/}}$\;${{\bf  endfor}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  count-list-sort \\ \index{count-list-sort}
{\rm{count-list}}\,({\it{a\/}}, {\rm{sort}}\,({\it{l\/}})\index{sort})\index{count-list} $=$ {\rm{count-list}}\,({\it{a\/}}, {\it{l\/}})\index{count-list}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ordered-append \\ \index{ordered-append}
{\rm{ordered}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{ordered} $\rightarrow$ {\rm{ordered}}\,({\it{a\/}})\index{ordered}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  leq-half \\ \index{leq-half}
{\rm{half}}\,({\it{i\/}})\index{half} $\leq$ {\it{i\/}}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{number-listp} \\  
\=\+{\rm{number-listp}}\,({\it{l\/}})\index{number-listp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }({\rm{car}}\,({\it{l\/}}) $\in\;${\bf{N}}${}$) $\wedge$ {\rm{number-listp}}\,({\rm{cdr}}\,({\it{l\/}}))\index{number-listp} \\ 
{\bf else }{\it{l\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ordered-sort \\ \index{ordered-sort}
{\rm{ordered}}\,({\rm{sort}}\,({\it{x\/}})\index{sort})\index{ordered}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  addtolist-of-ordered-number-list \\ \index{addtolist-of-ordered-number-list}
\=\+({\rm{ordered}}\,({\it{x\/}})\index{ordered} $\wedge$ {\rm{number-listp}}\,({\it{x\/}})\index{number-listp} $\wedge$ ({\it{i\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{car}}\,({\it{x\/}}) $\not<$ {\it{i\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{addtolist}}\,({\it{i\/}}, {\it{x\/}})\index{addtolist} $=$ {\rm{cons}}\,({\it{i\/}}, {\it{x\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort-of-ordered-number-list \\ \index{sort-of-ordered-number-list}
({\rm{ordered}}\,({\it{x\/}})\index{ordered} $\wedge$ {\rm{number-listp}}\,({\it{x\/}})\index{number-listp}) $\rightarrow$ ({\rm{sort}}\,({\it{x\/}})\index{sort} $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{xor} \\  
\=\+{\rm{xor}}\,({\it{p\/}}, {\it{q\/}})\index{xor} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{q\/}} \\ 
{\bf then }\=\+{\bf if }{\it{p\/}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\it{p\/}} $=$ {\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crock-due-to-lack-of-bounce \\ \index{crock-due-to-lack-of-bounce}
({\it{x\/}} $=$ {\rm{sort}}\,({\it{l\/}})\index{sort}) $\rightarrow$ {\rm{ordered}}\,({\it{x\/}})\index{ordered}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort-ordered \\ \index{sort-ordered}
{\rm{number-listp}}\,({\it{l\/}})\index{number-listp} $\rightarrow$ (({\rm{sort}}\,({\it{l\/}})\index{sort} $=$ {\it{l\/}}) $=$ {\rm{ordered}}\,({\it{l\/}})\index{ordered})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subst} \\  
\=\+{\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\it{z\/}})\index{subst} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $=$ {\it{z\/}}$\;\;${\bf then }{\it{x\/}} \\ 
{\bf elseif }{\rm{listp}}\,({\it{z\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\rm{car}}\,({\it{z\/}}))\index{subst}, {\rm{subst}}\,({\it{x\/}}, {\it{y\/}}, {\rm{cdr}}\,({\it{z\/}}))\index{subst}) \\ 
{\bf else }{\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst-a-a \\ \index{subst-a-a}
{\rm{subst}}\,({\it{a\/}}, {\it{a\/}}, {\it{b\/}})\index{subst} $=$ {\it{b\/}}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{occur} \\  
\=\+{\rm{occur}}\,({\it{x\/}}, {\it{y\/}})\index{occur} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{occur}}\,({\it{x\/}}, {\rm{car}}\,({\it{y\/}}))\index{occur}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{occur}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{y\/}}))\index{occur}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  occur-subst \\ \index{occur-subst}
($\neg$ {\rm{occur}}\,({\it{a\/}}, {\it{b\/}})\index{occur}) $\rightarrow$ ({\rm{subst}}\,({\it{c\/}}, {\it{a\/}}, {\it{b\/}})\index{subst} $=$ {\it{b\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{countps-loop} \\  
\=\+{\rm{countps-loop}}\,({\it{l\/}}, {\it{pred\/}}, {\it{ans\/}})\index{countps-loop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{apply\$}}\,({\it{pred\/}}, {\rm{list}}\,({\rm{car}}\,({\it{l\/}}))) \\ 
{\bf then }{\rm{countps-loop}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{pred\/}}, $1\;+$ {\it{ans\/}})\index{countps-loop} \\ 
{\bf else }{\rm{countps-loop}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{pred\/}}, {\it{ans\/}})\index{countps-loop}$\;${\bf  endif}\- \\ 
{\bf else }{\it{ans\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{countps-}$\;\;$
{\rm{countps-}}\,({\it{l\/}}, {\it{pred\/}})\index{countps-} $=$ {\rm{countps-loop}}\,({\it{l\/}}, {\it{pred\/}}, {\tt{0}})\index{countps-loop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  countps-countps \\ \index{countps-countps}
\=\+(({\it{n\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{litatom}}\,({\it{x\/}}) $\wedge$ ({\it{pred\/}} $\not=$ {\tt{'}}{\tt{quote}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{countps-loop}}\,({\it{l\/}}, {\it{pred\/}}, {\it{n\/}})\index{countps-loop} \\ 
$=$$\;\;\;\;$({\it{n\/}} $+$ {\rm{for}}\,(\=\+{\it{x\/}}, \\ 
{\it{l\/}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\bf{t}}), \\ 
{\tt{'}}{\tt{count}}, \\ 
{\rm{list}}\,({\it{pred\/}}, {\it{x\/}}), \\ 
{\bf{nil}})\-))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{fact} \\  
\=\+{\rm{fact}}\,({\it{i\/}})\index{fact} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\it{i\/}} $*$ {\rm{fact}}\,({\it{i\/}} $-\;1$)\index{fact}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{fact-loop} \\  
\=\+{\rm{fact-loop}}\,({\it{i\/}}, {\it{ans\/}})\index{fact-loop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{ans\/}} \\ 
{\bf else }{\rm{fact-loop}}\,({\it{i\/}} $-\;1$, {\it{i\/}} $*$ {\it{ans\/}})\index{fact-loop}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{fact-}$\;\;$
{\rm{fact-}}\,({\it{i\/}})\index{fact-} $=$ {\rm{fact-loop}}\,({\it{i\/}}, {\tt{1}})\index{fact-loop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  fact-loop-fact \\ \index{fact-loop-fact}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{fact-loop}}\,({\it{j\/}}, {\it{i\/}})\index{fact-loop} $=$ ({\it{i\/}} $*$ {\rm{fact}}\,({\it{j\/}})\index{fact}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  fact-fact \\ \index{fact-fact}
{\rm{fact-}}\,({\it{i\/}})\index{fact-} $=$ {\rm{fact}}\,({\it{i\/}})\index{fact}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  fact-from-to \\ \index{fact-from-to}
\=\+{\rm{fact}}\,({\it{n\/}})\index{fact} \\ 
$=$$\;\;\;\;$\=\+{\bf for }{\it{i\/}}{\bf $\;$ in }{\rm{from-to}}\,({\tt{1}}, {\it{n\/}})\index{from-to} \\ 
{\bf multiply} {\it{i\/}}$\;${{\bf  endfor}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{reverse-loop} \\  
\=\+{\rm{reverse-loop}}\,({\it{x\/}}, {\it{ans\/}})\index{reverse-loop} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{reverse-loop}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\it{ans\/}}))\index{reverse-loop} \\ 
{\bf else }{\it{ans\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{reverse-}$\;\;$
{\rm{reverse-}}\,({\it{x\/}})\index{reverse-} $=$ {\rm{reverse-loop}}\,({\it{x\/}}, {\bf{nil}})\index{reverse-loop}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reverse-loop-append-reverse \\ \index{reverse-loop-append-reverse}
{\rm{reverse-loop}}\,({\it{x\/}}, {\it{y\/}})\index{reverse-loop} $=$ {\rm{append}}\,({\rm{reverse}}\,({\it{x\/}})\index{reverse}, {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reverse-loop-reverse \\ \index{reverse-loop-reverse}
{\rm{reverse-loop}}\,({\it{x\/}}, {\bf{nil}})\index{reverse-loop} $=$ {\rm{reverse}}\,({\it{x\/}})\index{reverse}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reverse-append \\ \index{reverse-append}
{\rm{reverse-}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{reverse-} $=$ {\rm{append}}\,({\rm{reverse-}}\,({\it{b\/}})\index{reverse-}, {\rm{reverse-}}\,({\it{a\/}})\index{reverse-})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  reverse-reverse- \\ \index{reverse-reverse-}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{reverse-}}\,({\rm{reverse-}}\,({\it{x\/}})\index{reverse-})\index{reverse-} $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sort-lp} \\  
\=\+{\rm{sort-lp}}\,({\it{x\/}}, {\it{y\/}})\index{sort-lp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{sort-lp}}\,({\rm{cdr}}\,({\it{x\/}}), {\rm{addtolist}}\,({\rm{car}}\,({\it{x\/}}), {\it{y\/}})\index{addtolist})\index{sort-lp} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ordered-addtolist \\ \index{ordered-addtolist}
{\rm{ordered}}\,({\it{y\/}})\index{ordered} $\rightarrow$ {\rm{ordered}}\,({\rm{addtolist}}\,({\it{x\/}}, {\it{y\/}})\index{addtolist})\index{ordered}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ordered-sort-lp \\ \index{ordered-sort-lp}
{\rm{ordered}}\,({\it{y\/}})\index{ordered} $\rightarrow$ {\rm{ordered}}\,({\rm{sort-lp}}\,({\it{x\/}}, {\it{y\/}})\index{sort-lp})\index{ordered}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  numberp-count \\ \index{numberp-count}
{\rm{for}}\,(\=\+{\it{x\/}}, \\ 
{\it{l\/}}, \\ 
{\it{p\/}}, \\ 
{\tt{'}}{\tt{count}}, \\ 
{\it{b\/}}, \\ 
{\it{a\/}})\- $\in\;${\bf{N}}${}$
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  count-sort-lp \\ \index{count-sort-lp}
{\rm{count-list}}\,({\it{z\/}}, {\rm{sort-lp}}\,({\it{x\/}}, {\it{y\/}})\index{sort-lp})\index{count-list} $=$ ({\rm{count-list}}\,({\it{z\/}}, {\it{x\/}})\index{count-list} $+$ {\rm{count-list}}\,({\it{z\/}}, {\it{y\/}})\index{count-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  append-cancellation \\ \index{append-cancellation}
({\rm{append}}\,({\it{a\/}}, {\it{b\/}}) $=$ {\rm{append}}\,({\it{a\/}}, {\it{c\/}})) $=$ ({\it{b\/}} $=$ {\it{c\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-lessp \\ \index{equal-lessp}
\=\+(({\it{x\/}} $<$ {\it{y\/}}) $=$ {\it{z\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }{\bf{t}} $=$ {\it{z\/}} \\ 
{\bf else }{\bf{f}} $=$ {\it{z\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-elim \\ \index{difference-elim}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not<$ {\it{x\/}})) $\rightarrow$ (({\it{x\/}} $+$ ({\it{y\/}} $-$ {\it{x\/}})) $=$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{power-eval} \\  
\=\+{\rm{power-eval}}\,({\it{l\/}}, {\it{base\/}})\index{power-eval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}})$\;\;${\bf then }{\rm{car}}\,({\it{l\/}}) $+$ ({\it{base\/}} $*$ {\rm{power-eval}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{base\/}})\index{power-eval}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{big-plus1} \\  
\=\+{\rm{big-plus1}}\,({\it{l\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{l\/}} \\ 
{\bf else }{\rm{cons}}\,(\=\+({\rm{car}}\,({\it{l\/}}) $+$ {\it{i\/}}) ${}${\bf{mod}}${}$ {\it{base\/}}, \\ 
{\rm{big-plus1}}\,({\rm{cdr}}\,({\it{l\/}}), ({\rm{car}}\,({\it{l\/}}) $+$ {\it{i\/}}) $\div$ {\it{base\/}}, {\it{base\/}})\index{big-plus1})\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-quotient \\ \index{remainder-quotient}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  power-eval-big-plus1 \\ \index{power-eval-big-plus1}
{\rm{power-eval}}\,({\rm{big-plus1}}\,({\it{l\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus1}, {\it{base\/}})\index{power-eval} $=$ ({\rm{power-eval}}\,({\it{l\/}}, {\it{base\/}})\index{power-eval} $+$ {\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{big-plus} \\  
\=\+{\rm{big-plus}}\,({\it{x\/}}, {\it{y\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\it{y\/}}) \\ 
{\bf then }{\rm{cons}}\,(\=\+({\it{i\/}} $+$ ({\rm{car}}\,({\it{x\/}}) $+$ {\rm{car}}\,({\it{y\/}}))) ${}${\bf{mod}}${}$ {\it{base\/}}, \\ 
{\rm{big-plus}}\,(\=\+{\rm{cdr}}\,({\it{x\/}}), \\ 
{\rm{cdr}}\,({\it{y\/}}), \\ 
({\it{i\/}} $+$ ({\rm{car}}\,({\it{x\/}}) $+$ {\rm{car}}\,({\it{y\/}}))) $\div$ {\it{base\/}}, \\ 
{\it{base\/}})\-\index{big-plus})\- \\ 
{\bf else }{\rm{big-plus1}}\,({\it{x\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus1}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{big-plus1}}\,({\it{y\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus1}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  power-eval-big-plus \\ \index{power-eval-big-plus}
\=\+{\rm{power-eval}}\,({\rm{big-plus}}\,({\it{x\/}}, {\it{y\/}}, {\it{i\/}}, {\it{base\/}})\index{big-plus}, {\it{base\/}})\index{power-eval} \\ 
$=$$\;\;\;\;$({\it{i\/}} $+$ ({\rm{power-eval}}\,({\it{x\/}}, {\it{base\/}})\index{power-eval} $+$ {\rm{power-eval}}\,({\it{y\/}}, {\it{base\/}})\index{power-eval}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-wrt-1 \\ \index{remainder-wrt-1}
({\it{y\/}} ${}${\bf{mod}}${}$ {\tt{1}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-wrt-12 \\ \index{remainder-wrt-12}
({\it{x\/}} $\not\in\;${\bf{N}}${}$) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-remainder2 \\ \index{lessp-remainder2}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}}) $=$ ({\it{y\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-x-x \\ \index{remainder-x-x}
({\it{x\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-quotient-elim \\ \index{remainder-quotient-elim}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ ((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $+$ ({\it{y\/}} $*$ ({\it{x\/}} $\div$ {\it{y\/}}))) $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-times-1 \\ \index{lessp-times-1}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{i\/}} $*$ {\it{j\/}}) $\not<$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-times-2 \\ \index{lessp-times-2}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{j\/}} $*$ {\it{i\/}}) $\not<$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-quotient1 \\ \index{lessp-quotient1}
(({\it{i\/}} $\div$ {\it{j\/}}) $<$ {\it{i\/}}) $=$ (({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{j\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{j\/}} $\not=$ {\tt{1}})))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-remainder1 \\ \index{lessp-remainder1}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{x\/}}) $=$ (({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not<$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{power-rep} \\  
\=\+{\rm{power-rep}}\,({\it{i\/}}, {\it{base\/}})\index{power-rep} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\it{base\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{i\/}}, {\bf{nil}}) \\ 
{\bf elseif }{\it{base\/}} $=$ {\tt{1}}$\;\;${\bf then }{\rm{cons}}\,({\it{i\/}}, {\bf{nil}}) \\ 
{\bf else }{\rm{cons}}\,({\it{i\/}} ${}${\bf{mod}}${}$ {\it{base\/}}, {\rm{power-rep}}\,({\it{i\/}} $\div$ {\it{base\/}}, {\it{base\/}})\index{power-rep})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  power-eval-power-rep \\ \index{power-eval-power-rep}
{\rm{power-eval}}\,({\rm{power-rep}}\,({\it{i\/}}, {\it{base\/}})\index{power-rep}, {\it{base\/}})\index{power-eval} $=$ {\rm{fix}}\,({\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-big-plus \\ \index{correctness-of-big-plus}
\=\+{\rm{power-eval}}\,({\rm{big-plus}}\,({\rm{power-rep}}\,({\it{i\/}}, {\it{base\/}})\index{power-rep}, {\rm{power-rep}}\,({\it{j\/}}, {\it{base\/}})\index{power-rep}, {\tt{0}}, {\it{base\/}})\index{big-plus}, {\it{base\/}})\index{power-eval} \\ 
$=$$\;\;\;\;$({\it{i\/}} $+$ {\it{j\/}})\-
\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}:  numberp-gcd \\ \index{numberp-gcd}
{\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} $\in\;${\bf{N}}${}$
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gcd-equal-0 \\ \index{gcd-equal-0}
({\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} $=$ {\tt{0}}) $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gcd-0 \\ \index{gcd-0}
{\rm{gcd}}\,({\tt{0}}, {\it{y\/}})\index{gcd} $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  commutativity-of-gcd \\ \index{commutativity-of-gcd}
{\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd} $=$ {\rm{gcd}}\,({\it{y\/}}, {\it{x\/}})\index{gcd}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nth-append \\ \index{nth-append}
{\rm{nth}}\,({\rm{append}}\,({\it{a\/}}, {\it{b\/}}), {\it{i\/}})\index{nth} $=$ {\rm{append}}\,({\rm{nth}}\,({\it{a\/}}, {\it{i\/}})\index{nth}, {\rm{nth}}\,({\it{b\/}}, {\it{i\/}} $-$ {\rm{length}}\,({\it{a\/}})\index{length})\index{nth})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-plus1 \\ \index{difference-plus1}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-plus2 \\ \index{difference-plus2}
(({\it{y\/}} $+$ {\it{x\/}}) $-$ {\it{x\/}}) $=$ {\rm{fix}}\,({\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-plus-cancelation \\ \index{difference-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $-$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $-$ {\it{z\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-difference \\ \index{times-difference}
({\it{x\/}} $*$ ({\it{c\/}} $-$ {\it{w\/}})) $=$ (({\it{c\/}} $*$ {\it{x\/}}) $-$ ({\it{w\/}} $*$ {\it{x\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{divides}$\;\;$
{\rm{divides}}\,({\it{x\/}}, {\it{y\/}})\index{divides} $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-times \\ \index{divides-times}
(({\it{x\/}} $*$ {\it{z\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-plus3 \\ \index{difference-plus3}
(({\it{b\/}} $+$ ({\it{a\/}} $+$ {\it{c\/}})) $-$ {\it{a\/}}) $=$ ({\it{b\/}} $+$ {\it{c\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-add1-cancellation \\ \index{difference-add1-cancellation}
(($1\;+$ ({\it{y\/}} $+$ {\it{z\/}})) $-$ {\it{z\/}}) $=$ ($1\;+$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-add1 \\ \index{remainder-add1}
(({\it{y\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}})) $\rightarrow$ ((($1\;+$ ({\it{x\/}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{y\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite1 \\ \index{divides-plus-rewrite1}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite2 \\ \index{divides-plus-rewrite2}
((({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})) $\rightarrow$ ((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite \\ \index{divides-plus-rewrite}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{x\/}} $+$ {\it{y\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-plus-cancelation \\ \index{lessp-plus-cancelation}
(({\it{x\/}} $+$ {\it{y\/}}) $<$ ({\it{x\/}} $+$ {\it{z\/}})) $=$ ({\it{y\/}} $<$ {\it{z\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-plus-rewrite-commuted \\ \index{divides-plus-rewrite-commuted}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $\rightarrow$ (((({\it{y\/}} $+$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) $=$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  euclid \\ \index{euclid}
\=\+(({\it{x\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{y\/}} $-$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $<$ {\it{y\/}}$\;\;${\bf then }({\it{y\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-times-cancellation \\ \index{lessp-times-cancellation}
(({\it{x\/}} $*$ {\it{z\/}}) $<$ ({\it{y\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-plus-cancellation3 \\ \index{lessp-plus-cancellation3}
({\it{y\/}} $<$ ({\it{x\/}} $+$ {\it{y\/}})) $=$ ({\it{x\/}} $\not\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  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})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gcd-divides-both \\ \index{gcd-divides-both}
(({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $=$ {\tt{0}}) $\wedge$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd}) $=$ {\tt{0}})
\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$ {\rm{divides}}\,({\it{z\/}}, {\it{x\/}})\index{divides} $\wedge$ {\rm{divides}}\,({\it{z\/}}, {\it{y\/}})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$({\it{z\/}} $\leq$ {\rm{gcd}}\,({\it{x\/}}, {\it{y\/}})\index{gcd})\-
\end{tabbing}

\noindent{\sc Event}:   Add the shell {\it{cons-if\/}}\index{cons-if}, with recognizer function symbol {\it{if-exprp\/}} and 3 accessors: {\it{test\/}}, with type restriction (none-of) and default value zero; {\it{left-branch\/}}, with type restriction (none-of) and default value zero; {\it{right-branch\/}}, with type restriction (none-of) and default value zero.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{assignment} \\  
\=\+{\rm{assignment}}\,({\it{var\/}}, {\it{alist\/}})\index{assignment} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{var\/}} $=$ {\bf{t}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{var\/}} $=$ {\bf{f}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{var\/}} $=$ {\rm{caar}}\,({\it{alist\/}})$\;\;${\bf then }{\rm{cdar}}\,({\it{alist\/}}) \\ 
{\bf else }{\rm{assignment}}\,({\it{var\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{assignment}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{value} \\  
\=\+{\rm{value}}\,({\it{x\/}}, {\it{alist\/}})\index{value} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+{\bf if }{\rm{value}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{value}$\;\;${\bf then }{\rm{value}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\it{alist\/}})\index{value} \\ 
{\bf else }{\rm{value}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch}, {\it{alist\/}})\index{value}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{assignment}}\,({\it{x\/}}, {\it{alist\/}})\index{assignment}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{if-depth} \\  
\=\+{\rm{if-depth}}\,({\it{x\/}})\index{if-depth} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp}$\;\;${\bf then }$1\;+$ {\rm{if-depth}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{if-depth} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{if-complexity} \\  
\=\+{\rm{if-complexity}}\,({\it{x\/}})\index{if-complexity} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+{\rm{if-complexity}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{if-complexity} \\ 
$*$$\;\;\;\;$(\=\+{\rm{if-complexity}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch})\index{if-complexity} \\ 
$+$$\;\;\;\;${\rm{if-complexity}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\index{if-complexity})\-\- \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  if-complexity-not-0 \\ \index{if-complexity-not-0}
{\rm{if-complexity}}\,({\it{x\/}})\index{if-complexity} $\not=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  if-complexity-goes-down1 \\ \index{if-complexity-goes-down1}
{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} $\rightarrow$ ({\rm{if-complexity}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch})\index{if-complexity} $<$ {\rm{if-complexity}}\,({\it{x\/}})\index{if-complexity})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  if-complexity-goes-down2 \\ \index{if-complexity-goes-down2}
{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} $\rightarrow$ ({\rm{if-complexity}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\index{if-complexity} $<$ {\rm{if-complexity}}\,({\it{x\/}})\index{if-complexity})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{normalize} \\  
\=\+{\rm{normalize}}\,({\it{x\/}})\index{normalize} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+{\bf if }{\rm{if-exprp}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{if-exprp} \\ 
{\bf then }{\rm{normalize}}\,({\rm{cons-if}}\,(\=\+{\rm{test}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{test}, \\ 
{\rm{cons-if}}\,(\=\+{\rm{left-branch}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{left-branch}, \\ 
{\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, \\ 
{\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\-\index{cons-if}, \\ 
{\rm{cons-if}}\,(\=\+{\rm{right-branch}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{right-branch}, \\ 
{\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, \\ 
{\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\-\index{cons-if})\-\index{cons-if})\index{normalize} \\ 
{\bf else }{\rm{cons-if}}\,(\=\+{\rm{test}}\,({\it{x\/}})\index{test}, \\ 
{\rm{normalize}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch})\index{normalize}, \\ 
{\rm{normalize}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\index{normalize})\-\index{cons-if}$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{normalized-if-exprp} \\  
\=\+{\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+($\neg$ {\rm{if-exprp}}\,({\rm{test}}\,({\it{x\/}})\index{test})\index{if-exprp}) \\ 
$\wedge$$\;\;\;\;${\rm{normalized-if-exprp}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch})\index{normalized-if-exprp} \\ 
$\wedge$$\;\;\;\;${\rm{normalized-if-exprp}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch})\index{normalized-if-exprp}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{assignedp} \\  
\=\+{\rm{assignedp}}\,({\it{var\/}}, {\it{alist\/}})\index{assignedp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{var\/}} $=$ {\bf{t}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{var\/}} $=$ {\bf{f}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{alist\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{var\/}} $=$ {\rm{caar}}\,({\it{alist\/}})$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{assignedp}}\,({\it{var\/}}, {\rm{cdr}}\,({\it{alist\/}}))\index{assignedp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{assume-true}$\;\;$
{\rm{assume-true}}\,({\it{var\/}}, {\it{alist\/}})\index{assume-true} $=$ {\rm{cons}}\,({\rm{cons}}\,({\it{var\/}}, {\bf{t}}), {\it{alist\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{assume-false}$\;\;$
{\rm{assume-false}}\,({\it{var\/}}, {\it{alist\/}})\index{assume-false} $=$ {\rm{cons}}\,({\rm{cons}}\,({\it{var\/}}, {\bf{f}}), {\it{alist\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tautologyp} \\  
\=\+{\rm{tautologyp}}\,({\it{x\/}}, {\it{alist\/}})\index{tautologyp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+{\bf if }{\rm{assignedp}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assignedp} \\ 
{\bf then }\=\+{\bf if }{\rm{assignment}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assignment} \\ 
{\bf then }{\rm{tautologyp}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\it{alist\/}})\index{tautologyp} \\ 
{\bf else }{\rm{tautologyp}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch}, {\it{alist\/}})\index{tautologyp}$\;${\bf  endif}\- \\ 
{\bf else }\=\+{\rm{tautologyp}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\rm{assume-true}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assume-true})\index{tautologyp} \\ 
$\wedge$$\;\;\;\;${\rm{tautologyp}}\,(\=\+{\rm{right-branch}}\,({\it{x\/}})\index{right-branch}, \\ 
{\rm{assume-false}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assume-false})\-\index{tautologyp}\-$\;${\bf  endif}\- \\ 
{\bf else }{\rm{assignment}}\,({\it{x\/}}, {\it{alist\/}})\index{assignment}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  assignment-append \\ \index{assignment-append}
\=\+{\rm{assignment}}\,({\it{x\/}}, {\rm{append}}\,({\it{a\/}}, {\it{b\/}}))\index{assignment} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{assignedp}}\,({\it{x\/}}, {\it{a\/}})\index{assignedp}$\;\;${\bf then }{\rm{assignment}}\,({\it{x\/}}, {\it{a\/}})\index{assignment} \\ 
{\bf else }{\rm{assignment}}\,({\it{x\/}}, {\it{b\/}})\index{assignment}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  value-can-ignore-redundant-assignments \\ \index{value-can-ignore-redundant-assi!gnments}
\=\+(\=\+(({\it{val\/}} $\leftrightarrow$ {\rm{assignment}}\,({\it{var\/}}, {\it{a\/}})\index{assignment}) $\wedge$ {\rm{value}}\,({\it{x\/}}, {\it{a\/}})\index{value}) \\ 
$\rightarrow$$\;\;\;\;${\rm{value}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{var\/}}, {\it{val\/}}), {\it{a\/}}))\index{value})\- \\ 
$\wedge$$\;\;\;\;$(\=\+(({\it{val\/}} $\leftrightarrow$ {\rm{assignment}}\,({\it{var\/}}, {\it{a\/}})\index{assignment}) $\wedge$ ($\neg$ {\rm{value}}\,({\it{x\/}}, {\it{a\/}})\index{value})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{value}}\,({\it{x\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{var\/}}, {\it{val\/}}), {\it{a\/}}))\index{value}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  value-short-cut \\ \index{value-short-cut}
\=\+({\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} $\wedge$ {\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{a\/}})\index{value} $=$ {\rm{assignment}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{a\/}})\index{assignment})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  assignment-implies-assigned \\ \index{assignment-implies-assigned}
{\rm{assignment}}\,({\it{x\/}}, {\it{a\/}})\index{assignment} $\rightarrow$ {\rm{assignedp}}\,({\it{x\/}}, {\it{a\/}})\index{assignedp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautologyp-is-sound \\ \index{tautologyp-is-sound}
({\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp} $\wedge$ {\rm{tautologyp}}\,({\it{x\/}}, {\it{a1\/}})\index{tautologyp}) $\rightarrow$ {\rm{value}}\,({\it{x\/}}, {\rm{append}}\,({\it{a1\/}}, {\it{a2\/}}))\index{value}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tautology-checker}$\;\;$
{\rm{tautology-checker}}\,({\it{x\/}})\index{tautology-checker} $=$ {\rm{tautologyp}}\,({\rm{normalize}}\,({\it{x\/}})\index{normalize}, {\bf{nil}})\index{tautologyp}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{falsify1} \\  
\=\+{\rm{falsify1}}\,({\it{x\/}}, {\it{alist\/}})\index{falsify1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{if-exprp}}\,({\it{x\/}})\index{if-exprp} \\ 
{\bf then }\=\+{\bf if }{\rm{assignedp}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assignedp} \\ 
{\bf then }\=\+{\bf if }{\rm{assignment}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assignment} \\ 
{\bf then }{\rm{falsify1}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\it{alist\/}})\index{falsify1} \\ 
{\bf else }{\rm{falsify1}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch}, {\it{alist\/}})\index{falsify1}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{falsify1}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\rm{assume-true}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assume-true})\index{falsify1} \\ 
{\bf then }{\rm{falsify1}}\,({\rm{left-branch}}\,({\it{x\/}})\index{left-branch}, {\rm{assume-true}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assume-true})\index{falsify1} \\ 
{\bf else }{\rm{falsify1}}\,({\rm{right-branch}}\,({\it{x\/}})\index{right-branch}, {\rm{assume-false}}\,({\rm{test}}\,({\it{x\/}})\index{test}, {\it{alist\/}})\index{assume-false})\index{falsify1}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{assignedp}}\,({\it{x\/}}, {\it{alist\/}})\index{assignedp} \\ 
{\bf then }\=\+{\bf if }{\rm{assignment}}\,({\it{x\/}}, {\it{alist\/}})\index{assignment}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{alist\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\rm{cons}}\,({\it{x\/}}, {\bf{f}}), {\it{alist\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{falsify}$\;\;$
{\rm{falsify}}\,({\it{x\/}})\index{falsify} $=$ {\rm{falsify1}}\,({\rm{normalize}}\,({\it{x\/}})\index{normalize}, {\bf{nil}})\index{falsify1}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  falsify1-extends-models \\ \index{falsify1-extends-models}
\=\+{\rm{assignedp}}\,({\it{x\/}}, {\it{a\/}})\index{assignedp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{assignment}}\,({\it{x\/}}, {\rm{falsify1}}\,({\it{y\/}}, {\it{a\/}})\index{falsify1})\index{assignment} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{falsify1}}\,({\it{y\/}}, {\it{a\/}})\index{falsify1}$\;\;${\bf then }{\rm{assignment}}\,({\it{x\/}}, {\it{a\/}})\index{assignment} \\ 
{\bf else }{\it{x\/}} $=$ {\bf{t}}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  falsify1-falsifies \\ \index{falsify1-falsifies}
\=\+({\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp} $\wedge$ {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{x\/}}, {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1})\index{value} $=$ {\bf{f}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautologyp-fails-means-falsify1-wins \\ \index{tautologyp-fails-means-falsify1!-wins}
({\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp} $\wedge$ ($\neg$ {\rm{tautologyp}}\,({\it{x\/}}, {\it{a\/}})\index{tautologyp}) $\wedge$ {\it{a\/}}) $\rightarrow$ {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  normalize-is-sound \\ \index{normalize-is-sound}
{\rm{value}}\,({\rm{normalize}}\,({\it{x\/}})\index{normalize}, {\it{a\/}})\index{value} $=$ {\rm{value}}\,({\it{x\/}}, {\it{a\/}})\index{value}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  normalize-normalizes \\ \index{normalize-normalizes}
{\rm{normalized-if-exprp}}\,({\rm{normalize}}\,({\it{x\/}})\index{normalize})\index{normalized-if-exprp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautology-checker-completeness-bridge \\ \index{tautology-checker-completeness-!bridge}
\=\+(\=\+({\rm{value}}\,({\it{y\/}}, {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1})\index{value} $=$ {\rm{value}}\,({\it{x\/}}, {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1})\index{value}) \\ 
$\wedge$$\;\;\;\;${\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1} \\ 
$\wedge$$\;\;\;\;${\rm{normalized-if-exprp}}\,({\it{x\/}})\index{normalized-if-exprp})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{value}}\,({\it{y\/}}, {\rm{falsify1}}\,({\it{x\/}}, {\it{a\/}})\index{falsify1})\index{value} $=$ {\bf{f}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautology-checker-is-complete \\ \index{tautology-checker-is-complete}
($\neg$ {\rm{tautology-checker}}\,({\it{x\/}})\index{tautology-checker}) $\rightarrow$ ({\rm{value}}\,({\it{x\/}}, {\rm{falsify}}\,({\it{x\/}})\index{falsify})\index{value} $=$ {\bf{f}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautology-checker-soundness-bridge \\ \index{tautology-checker-soundness-bri!dge}
\=\+(\=\+{\rm{tautologyp}}\,({\it{y\/}}, {\it{a1\/}})\index{tautologyp} \\ 
$\wedge$$\;\;\;\;${\rm{normalized-if-exprp}}\,({\it{y\/}})\index{normalized-if-exprp} \\ 
$\wedge$$\;\;\;\;$({\rm{value}}\,({\it{x\/}}, {\it{a2\/}})\index{value} $=$ {\rm{value}}\,({\it{y\/}}, {\rm{append}}\,({\it{a1\/}}, {\it{a2\/}}))\index{value}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{value}}\,({\it{x\/}}, {\it{a2\/}})\index{value}\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tautology-checker-is-sound \\ \index{tautology-checker-is-sound}
{\rm{tautology-checker}}\,({\it{x\/}})\index{tautology-checker} $\rightarrow$ {\rm{value}}\,({\it{x\/}}, {\it{a\/}})\index{value}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  flatten-singleton \\ \index{flatten-singleton}
({\rm{flatten}}\,({\it{x\/}})\index{flatten} $=$ {\rm{cons}}\,({\it{y\/}}, {\bf{nil}})) $=$ (({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\wedge$ ({\it{x\/}} $=$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{leftcount} \\  
\=\+{\rm{leftcount}}\,({\it{x\/}})\index{leftcount} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{leftcount}}\,({\rm{car}}\,({\it{x\/}}))\index{leftcount}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{gopher} \\  
\=\+{\rm{gopher}}\,({\it{x\/}})\index{gopher} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\rm{car}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$)$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{gopher}}\,({\rm{cons}}\,({\rm{caar}}\,({\it{x\/}}), {\rm{cons}}\,({\rm{cdar}}\,({\it{x\/}}), {\rm{cdr}}\,({\it{x\/}}))))\index{gopher}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gopher-preserves-count \\ \index{gopher-preserves-count}
{\rm{count}}\,({\it{x\/}}) $\not<$ {\rm{count}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  listp-gopher \\ \index{listp-gopher}
{\rm{listp}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher}) $=$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{samefringe} \\  
\=\+{\rm{samefringe}}\,({\it{x\/}}, {\it{y\/}})\index{samefringe} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$) $\vee$ ({\it{y\/}} $\simeq\;${{\bf{nil}}}${}$)$\;\;${\bf then }{\it{x\/}} $=$ {\it{y\/}} \\ 
{\bf else }\=\+({\rm{car}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher}) $=$ {\rm{car}}\,({\rm{gopher}}\,({\it{y\/}})\index{gopher})) \\ 
$\wedge$$\;\;\;\;${\rm{samefringe}}\,({\rm{cdr}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher}), {\rm{cdr}}\,({\rm{gopher}}\,({\it{y\/}})\index{gopher}))\index{samefringe}\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gopher-returns-leftmost-atom \\ \index{gopher-returns-leftmost-atom}
\=\+{\rm{car}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{car}}\,({\rm{flatten}}\,({\it{x\/}})\index{flatten}) \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gopher-returns-correct-state \\ \index{gopher-returns-correct-state}
\=\+{\rm{flatten}}\,({\rm{cdr}}\,({\rm{gopher}}\,({\it{x\/}})\index{gopher}))\index{flatten} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cdr}}\,({\rm{flatten}}\,({\it{x\/}})\index{flatten}) \\ 
{\bf else }{\rm{cons}}\,({\tt{0}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-samefringe \\ \index{correctness-of-samefringe}
{\rm{samefringe}}\,({\it{x\/}}, {\it{y\/}})\index{samefringe} $=$ ({\rm{flatten}}\,({\it{x\/}})\index{flatten} $=$ {\rm{flatten}}\,({\it{y\/}})\index{flatten})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prime1} \\  
\=\+{\rm{prime1}}\,({\it{x\/}}, {\it{y\/}})\index{prime1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{y\/}} $=$ {\tt{1}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }($\neg$ {\rm{divides}}\,({\it{y\/}}, {\it{x\/}})\index{divides}) $\wedge$ {\rm{prime1}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{prime1}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prime} \\  
{\rm{prime}}\,({\it{x\/}})\index{prime} $=$ (({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ {\rm{prime1}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{prime1})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{greatest-factor} \\  
\=\+{\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{y\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $=$ {\tt{1}})$\;\;${\bf then }{\it{x\/}} \\ 
{\bf elseif }{\rm{divides}}\,({\it{y\/}}, {\it{x\/}})\index{divides}$\;\;${\bf then }{\it{y\/}} \\ 
{\bf else }{\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{greatest-factor}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatest-factor-lessp \\ \index{greatest-factor-lessp}
\=\+(\=\+({\it{y\/}} $<$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{prime1}}\,({\it{x\/}}, {\it{y\/}})\index{prime1}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $-\;1$) $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\not\simeq {\tt{0}}$))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor} $<$ {\it{x\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatest-factor-divides \\ \index{greatest-factor-divides}
\=\+(({\it{y\/}} $<$ {\it{x\/}}) $\wedge$ ($\neg$ {\rm{prime1}}\,({\it{x\/}}, {\it{y\/}})\index{prime1}) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{y\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} ${}${\bf{mod}}${}$ {\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor}) $=$ {\tt{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatest-factor-0 \\ \index{greatest-factor-0}
({\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor} $=$ {\tt{0}}) $=$ ((({\it{y\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $=$ {\tt{1}})) $\wedge$ ({\it{x\/}} $=$ {\tt{0}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-0-crock \\ \index{remainder-0-crock}
({\tt{0}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatest-factor-1 \\ \index{greatest-factor-1}
({\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor} $=$ {\tt{1}}) $=$ ({\it{x\/}} $=$ {\tt{1}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  numberp-greatest-factor \\ \index{numberp-greatest-factor}
({\rm{greatest-factor}}\,({\it{x\/}}, {\it{y\/}})\index{greatest-factor} $\in\;${\bf{N}}${}$) $=$ ($\neg$ ((({\it{y\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $=$ {\tt{1}})) $\wedge$ ({\it{x\/}} $\not\in\;${\bf{N}}${}$)))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prime-factors} \\  
\=\+{\rm{prime-factors}}\,({\it{x\/}})\index{prime-factors} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ (({\it{x\/}} $-\;1$) $=$ {\tt{0}})$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{prime1}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{prime1}$\;\;${\bf then }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}}) \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{prime-factors}}\,({\rm{greatest-factor}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{greatest-factor})\index{prime-factors}, \\ 
{\rm{prime-factors}}\,({\it{x\/}} $\div$ {\rm{greatest-factor}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{greatest-factor})\index{prime-factors})\-$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prime-list} \\  
\=\+{\rm{prime-list}}\,({\it{l\/}})\index{prime-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{prime}}\,({\rm{car}}\,({\it{l\/}}))\index{prime} $\wedge$ {\rm{prime-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{prime-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{times-list} \\  
\=\+{\rm{times-list}}\,({\it{l\/}})\index{times-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{car}}\,({\it{l\/}}) $*$ {\rm{times-list}}\,({\rm{cdr}}\,({\it{l\/}}))\index{times-list}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-list-append \\ \index{times-list-append}
{\rm{times-list}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{times-list} $=$ ({\rm{times-list}}\,({\it{x\/}})\index{times-list} $*$ {\rm{times-list}}\,({\it{y\/}})\index{times-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-list-append \\ \index{prime-list-append}
{\rm{prime-list}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{prime-list} $=$ ({\rm{prime-list}}\,({\it{x\/}})\index{prime-list} $\wedge$ {\rm{prime-list}}\,({\it{y\/}})\index{prime-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-list-prime-factors \\ \index{prime-list-prime-factors}
{\rm{prime-list}}\,({\rm{prime-factors}}\,({\it{x\/}})\index{prime-factors})\index{prime-list}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  quotient-times1 \\ \index{quotient-times1}
\=\+(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) $\wedge$ {\rm{divides}}\,({\it{x\/}}, {\it{y\/}})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $=$ {\it{y\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  quotient-lessp \\ \index{quotient-lessp}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} $\div$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  enough-factors \\ \index{enough-factors}
({\it{x\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{times-list}}\,({\rm{prime-factors}}\,({\it{x\/}})\index{prime-factors})\index{times-list} $=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-factorization-existence \\ \index{prime-factorization-existence}
\=\+({\it{x\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{times-list}}\,({\rm{prime-factors}}\,({\it{x\/}})\index{prime-factors})\index{times-list} $=$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{prime-list}}\,({\rm{prime-factors}}\,({\it{x\/}})\index{prime-factors})\index{prime-list})\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{greatereqpr} \\  
\=\+{\rm{greatereqpr}}\,({\it{w\/}}, {\it{z\/}})\index{greatereqpr} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{w\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{z\/}} $\simeq {\tt{0}}$ \\ 
{\bf elseif }{\it{w\/}} $=$ {\it{z\/}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{greatereqpr}}\,({\it{w\/}} $-\;1$, {\it{z\/}})\index{greatereqpr}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-id-iff-1 \\ \index{times-id-iff-1}
({\it{z\/}} $=$ ({\it{w\/}} $*$ {\it{z\/}})) $=$ (({\it{z\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{z\/}} $=$ {\tt{0}}) $\vee$ ({\it{w\/}} $=$ {\tt{1}})))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime1-basic \\ \index{prime1-basic}
\=\+(({\it{z\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{z\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{z\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{greatereqpr}}\,({\it{u\/}}, {\it{z\/}})\index{greatereqpr}) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{prime1}}\,({\it{w\/}} $*$ {\it{z\/}}, {\it{u\/}})\index{prime1})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatereqpr-lessp \\ \index{greatereqpr-lessp}
{\rm{greatereqpr}}\,({\it{x\/}}, {\it{y\/}})\index{greatereqpr} $=$ ({\it{x\/}} $\not<$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  greatereqpr-remainder \\ \index{greatereqpr-remainder}
(({\it{z\/}} $\not=$ ($1\;+$ {\it{v\/}})) $\wedge$ {\rm{divides}}\,({\it{z\/}}, $1\;+$ {\it{v\/}})\index{divides}) $\rightarrow$ {\rm{greatereqpr}}\,({\it{v\/}}, {\it{z\/}})\index{greatereqpr}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-basic \\ \index{prime-basic}
\=\+(({\it{z\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{z\/}} $\not=$ {\it{x\/}}) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}}) $\wedge$ {\rm{divides}}\,({\it{z\/}}, {\it{x\/}})\index{divides}) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{prime1}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{prime1})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-gcd \\ \index{remainder-gcd}
({\rm{gcd}}\,({\it{b\/}}, {\it{x\/}})\index{gcd} $=$ {\it{y\/}}) $\rightarrow$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-gcd-1 \\ \index{remainder-gcd-1}
(({\it{b\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\not=$ {\tt{0}}) $\rightarrow$ ({\rm{gcd}}\,({\it{b\/}}, {\it{x\/}})\index{gcd} $\not=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-times1 \\ \index{divides-times1}
({\it{a\/}} $=$ ({\it{z\/}} $*$ {\it{y\/}})) $\rightarrow$ (({\it{a\/}} ${}${\bf{mod}}${}$ {\it{z\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-identity1 \\ \index{times-identity1}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{y\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}})) $\rightarrow$ ({\it{x\/}} $\not=$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-identity \\ \index{times-identity}
({\it{x\/}} $=$ ({\it{x\/}} $*$ {\it{y\/}})) $=$ (({\it{x\/}} $=$ {\tt{0}}) $\vee$ (({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $=$ {\tt{1}})))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  kludge-bridge \\ \index{kludge-bridge}
({\it{y\/}} $=$ ({\it{k\/}} $*$ {\it{x\/}})) $\rightarrow$ ({\rm{gcd}}\,({\it{y\/}}, {\it{a\/}} $*$ {\it{x\/}})\index{gcd} $=$ ({\it{x\/}} $*$ {\rm{gcd}}\,({\it{a\/}}, {\it{k\/}})\index{gcd}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  hack1 \\ \index{hack1}
\=\+(($\neg$ {\rm{divides}}\,({\it{x\/}}, {\it{a\/}})\index{divides}) $\wedge$ ({\it{a\/}} $=$ {\rm{gcd}}\,({\it{x\/}} $*$ {\it{a\/}}, {\it{b\/}} $*$ {\it{a\/}})\index{gcd})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{k\/}} $*$ {\it{x\/}}) $\not=$ ({\it{b\/}} $*$ {\it{a\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-gcd \\ \index{prime-gcd}
\=\+(($\neg$ {\rm{divides}}\,({\it{x\/}}, {\it{b\/}})\index{divides}) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{x\/}} $-\;1$) $\not=$ {\tt{0}}) $\wedge$ {\rm{prime1}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{prime1}) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{gcd}}\,({\it{b\/}}, {\it{x\/}})\index{gcd} $=$ {\tt{1}}) $=$ {\bf{t}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  gcd-distributes-over-an-opened-up-times \\ \index{gcd-distributes-over-an-opened-!up-times}
\=\+(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{0}}) $\wedge$ ({\it{free\/}} $=$ ({\it{x\/}} $*$ {\it{z\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{gcd}}\,({\it{b\/}} $*$ {\it{z\/}}, {\it{free\/}})\index{gcd} $=$ ({\it{z\/}} $*$ {\rm{gcd}}\,({\it{b\/}}, {\it{x\/}})\index{gcd}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-key \\ \index{prime-key}
\=\+(({\it{z\/}} $\in\;${\bf{N}}${}$) $\wedge$ {\rm{prime}}\,({\it{x\/}})\index{prime} $\wedge$ ($\neg$ {\rm{divides}}\,({\it{x\/}}, {\it{z\/}})\index{divides}) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{x\/}}, {\it{b\/}})\index{divides})) \\ 
$\rightarrow$$\;\;\;\;$(({\it{x\/}} $*$ {\it{k\/}}) $\not=$ ({\it{b\/}} $*$ {\it{z\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  quotient-divides \\ \index{quotient-divides}
(({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{x\/}} $*$ ({\it{y\/}} $\div$ {\it{x\/}})) $\not=$ {\it{y\/}})) $\rightarrow$ (({\it{y\/}} ${}${\bf{mod}}${}$ {\it{x\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  little-step \\ \index{little-step}
({\rm{prime}}\,({\it{x\/}})\index{prime} $\wedge$ ({\it{y\/}} $\not=$ {\tt{1}}) $\wedge$ ({\it{x\/}} $\not=$ {\it{y\/}})) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $\not=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-count-delete \\ \index{lessp-count-delete}
({\it{n\/}} $\in$ {\it{l\/}}) $\rightarrow$ ({\rm{count}}\,({\rm{delete}}\,({\it{n\/}}, {\it{l\/}})\index{delete}) $<$ {\rm{count}}\,({\it{l\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{perm} \\  
\=\+{\rm{perm}}\,({\it{a\/}}, {\it{b\/}})\index{perm} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{b\/}} $\simeq\;${{\bf{nil}}}${}$ \\ 
{\bf elseif }{\rm{car}}\,({\it{a\/}}) $\in$ {\it{b\/}}$\;\;${\bf then }{\rm{perm}}\,({\rm{cdr}}\,({\it{a\/}}), {\rm{delete}}\,({\rm{car}}\,({\it{a\/}}), {\it{b\/}})\index{delete})\index{perm} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-times \\ \index{remainder-times}
(({\it{y\/}} $*$ {\it{x\/}}) ${}${\bf{mod}}${}$ {\it{y\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-list-delete \\ \index{prime-list-delete}
{\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\rightarrow$ {\rm{prime-list}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l2\/}})\index{delete})\index{prime-list}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-times-list \\ \index{divides-times-list}
(({\it{c\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{c\/}} $\in$ {\it{l\/}})) $\rightarrow$ (({\rm{times-list}}\,({\it{l\/}})\index{times-list} ${}${\bf{mod}}${}$ {\it{c\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  quotient-times \\ \index{quotient-times}
\=\+(({\it{y\/}} $*$ {\it{x\/}}) $\div$ {\it{y\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{fix}}\,({\it{x\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  distributivity-of-divides \\ \index{distributivity-of-divides}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{divides}}\,({\it{a\/}}, {\it{w\/}})\index{divides}) $\rightarrow$ (({\it{c\/}} $*$ ({\it{w\/}} $\div$ {\it{a\/}})) $=$ (({\it{c\/}} $*$ {\it{w\/}}) $\div$ {\it{a\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-list-delete \\ \index{times-list-delete}
\=\+(({\it{c\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{c\/}} $\in$ {\it{l\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{times-list}}\,({\rm{delete}}\,({\it{c\/}}, {\it{l\/}})\index{delete})\index{times-list} $=$ ({\rm{times-list}}\,({\it{l\/}})\index{times-list} $\div$ {\it{c\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-list-times-list \\ \index{prime-list-times-list}
\=\+({\rm{prime}}\,({\it{c\/}})\index{prime} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\wedge$ ({\it{c\/}} $\not\in$ {\it{l2\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{times-list}}\,({\it{l2\/}})\index{times-list} ${}${\bf{mod}}${}$ {\it{c\/}}) $\not=$ {\tt{0}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  if-times-then-divides \\ \index{if-times-then-divides}
(({\it{c\/}} $\not\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{divides}}\,({\it{c\/}}, {\it{x\/}})\index{divides})) $\rightarrow$ (({\it{c\/}} $*$ {\it{y\/}}) $\not=$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-equal-1 \\ \index{times-equal-1}
\=\+(({\it{a\/}} $*$ {\it{b\/}}) $=$ {\tt{1}}) \\ 
$=$$\;\;\;\;$(\=\+({\it{a\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\not=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{b\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$(({\it{a\/}} $-\;1$) $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$(({\it{b\/}} $-\;1$) $=$ {\tt{0}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-member \\ \index{prime-member}
\=\+((({\it{c\/}} $*$ {\rm{times-list}}\,({\it{l1\/}})\index{times-list}) $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list}) $\wedge$ {\rm{prime}}\,({\it{c\/}})\index{prime} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list}) \\ 
$\rightarrow$$\;\;\;\;$({\it{c\/}} $\in$ {\it{l2\/}})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  divides-implies-times \\ \index{divides-implies-times}
(({\it{a\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{c\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{a\/}} $*$ {\it{c\/}}) $=$ {\it{b\/}})) $\rightarrow$ (({\it{c\/}} $=$ ({\it{b\/}} $\div$ {\it{a\/}})) $=$ {\bf{t}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-factorization-uniqueness \\ \index{prime-factorization-uniqueness}
\=\+({\rm{prime-list}}\,({\it{l1\/}})\index{prime-list} $\wedge$ {\rm{prime-list}}\,({\it{l2\/}})\index{prime-list} $\wedge$ ({\rm{times-list}}\,({\it{l1\/}})\index{times-list} $=$ {\rm{times-list}}\,({\it{l2\/}})\index{times-list})) \\ 
$\rightarrow$$\;\;\;\;${\rm{perm}}\,({\it{l1\/}}, {\it{l2\/}})\index{perm}\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{maximum} \\  
\=\+{\rm{maximum}}\,({\it{l\/}})\index{maximum} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{car}}\,({\it{l\/}}) $<$ {\rm{maximum}}\,({\rm{cdr}}\,({\it{l\/}}))\index{maximum}$\;\;${\bf then }{\rm{maximum}}\,({\rm{cdr}}\,({\it{l\/}}))\index{maximum} \\ 
{\bf else }{\rm{car}}\,({\it{l\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  member-maximum \\ \index{member-maximum}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{maximum}}\,({\it{x\/}})\index{maximum} $\in$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-delete-rewrite \\ \index{lessp-delete-rewrite}
({\rm{count}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete}) $<$ {\rm{count}}\,({\it{l\/}})) $=$ ({\it{x\/}} $\in$ {\it{l\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ordered2} \\  
\=\+{\rm{ordered2}}\,({\it{l\/}})\index{ordered2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{l\/}})) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{l\/}}) $<$ {\rm{cadr}}\,({\it{l\/}})$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\rm{ordered2}}\,({\rm{cdr}}\,({\it{l\/}}))\index{ordered2}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{dsort} \\  
\=\+{\rm{dsort}}\,({\it{l\/}})\index{dsort} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,({\rm{maximum}}\,({\it{l\/}})\index{maximum}, {\rm{dsort}}\,({\rm{delete}}\,({\rm{maximum}}\,({\it{l\/}})\index{maximum}, {\it{l\/}})\index{delete})\index{dsort})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{addtolist2} \\  
\=\+{\rm{addtolist2}}\,({\it{x\/}}, {\it{l\/}})\index{addtolist2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{l\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $<$ {\rm{car}}\,({\it{l\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{l\/}}), {\rm{addtolist2}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{l\/}}))\index{addtolist2}) \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\it{l\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\rm{cons}}\,({\it{x\/}}, {\bf{nil}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{sort2} \\  
\=\+{\rm{sort2}}\,({\it{l\/}})\index{sort2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{addtolist2}}\,({\rm{car}}\,({\it{l\/}}), {\rm{sort2}}\,({\rm{cdr}}\,({\it{l\/}}))\index{sort2})\index{addtolist2}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort2-gen-1 \\ \index{sort2-gen-1}
{\rm{plistp}}\,({\rm{sort2}}\,({\it{x\/}})\index{sort2})\index{plistp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort2-gen-2 \\ \index{sort2-gen-2}
{\rm{ordered2}}\,({\rm{sort2}}\,({\it{x\/}})\index{sort2})\index{ordered2}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort2-gen \\ \index{sort2-gen}
{\rm{plistp}}\,({\rm{sort2}}\,({\it{x\/}})\index{sort2})\index{plistp} $\wedge$ {\rm{ordered2}}\,({\rm{sort2}}\,({\it{x\/}})\index{sort2})\index{ordered2}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  addtolist2-delete \\ \index{addtolist2-delete}
\=\+({\rm{plistp}}\,({\it{y\/}})\index{plistp} $\wedge$ {\rm{ordered2}}\,({\it{y\/}})\index{ordered2} $\wedge$ ({\it{x\/}} $\not=$ {\it{v\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{addtolist2}}\,({\it{v\/}}, {\rm{delete}}\,({\it{x\/}}, {\it{y\/}})\index{delete})\index{addtolist2} $=$ {\rm{delete}}\,({\it{x\/}}, {\rm{addtolist2}}\,({\it{v\/}}, {\it{y\/}})\index{addtolist2})\index{delete})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  delete-addtolist2 \\ \index{delete-addtolist2}
{\rm{plistp}}\,({\it{y\/}})\index{plistp} $\rightarrow$ ({\rm{delete}}\,({\it{v\/}}, {\rm{addtolist2}}\,({\it{v\/}}, {\it{y\/}})\index{addtolist2})\index{delete} $=$ {\it{y\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  addtolist2-kludge \\ \index{addtolist2-kludge}
\=\+(({\it{v\/}} $\not<$ {\it{w\/}}) $\wedge$ ({\rm{addtolist2}}\,({\it{v\/}}, {\it{y\/}})\index{addtolist2} $=$ {\rm{cons}}\,({\it{v\/}}, {\it{y\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{addtolist2}}\,({\it{v\/}}, {\rm{addtolist2}}\,({\it{w\/}}, {\it{y\/}})\index{addtolist2})\index{addtolist2} $=$ {\rm{cons}}\,({\it{v\/}}, {\rm{addtolist2}}\,({\it{w\/}}, {\it{y\/}})\index{addtolist2}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-maximum-addtolist2 \\ \index{lessp-maximum-addtolist2}
({\it{v\/}} $\not<$ {\rm{maximum}}\,({\it{z\/}})\index{maximum}) $\rightarrow$ ({\rm{addtolist2}}\,({\it{v\/}}, {\rm{sort2}}\,({\it{z\/}})\index{sort2})\index{addtolist2} $=$ {\rm{cons}}\,({\it{v\/}}, {\rm{sort2}}\,({\it{z\/}})\index{sort2}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort2-delete-cons \\ \index{sort2-delete-cons}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{cons}}\,({\rm{maximum}}\,({\it{x\/}})\index{maximum}, {\rm{delete}}\,({\rm{maximum}}\,({\it{x\/}})\index{maximum}, {\rm{sort2}}\,({\it{x\/}})\index{sort2})\index{delete}) $=$ {\rm{sort2}}\,({\it{x\/}})\index{sort2})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sort2-delete \\ \index{sort2-delete}
{\rm{sort2}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{sort2} $=$ {\rm{delete}}\,({\it{x\/}}, {\rm{sort2}}\,({\it{l\/}})\index{sort2})\index{delete}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  dsort-sort2 \\ \index{dsort-sort2}
{\rm{dsort}}\,({\it{x\/}})\index{dsort} $=$ {\rm{sort2}}\,({\it{x\/}})\index{sort2}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  count-list-sort2 \\ \index{count-list-sort2}
{\rm{count-list}}\,({\it{a\/}}, {\rm{sort2}}\,({\it{l\/}})\index{sort2})\index{count-list} $=$ {\rm{count-list}}\,({\it{a\/}}, {\it{l\/}})\index{count-list}
\end{tabbing}

\begin{verbatim};   The next segment of this XXX illustrates three different program
;   verification methods:  the functional approach, the inductive assertion
;   approach, and the interpreter approach.  The program considered is a simple
;   loop for summing the numbers from I down to 0

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{sigma} \\  
\=\+{\rm{sigma}}\,({\it{m\/}}, {\it{n\/}})\index{sigma} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{m\/}} $<$ {\it{n\/}}$\;\;${\bf then }{\it{n\/}} $+$ {\rm{sigma}}\,({\it{m\/}}, {\it{n\/}} $-\;1$)\index{sigma} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-1 \\ \index{difference-1}
({\it{x\/}} $-$ {\tt{1}}) $=$ ({\it{x\/}} $-\;1$)
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{prog-trans-of-sigma} \\  
\=\+{\rm{prog-trans-of-sigma}}\,({\it{i\/}}, {\it{ac\/}})\index{prog-trans-of-sigma} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{ac\/}} \\ 
{\bf else }{\rm{prog-trans-of-sigma}}\,({\it{i\/}} $-$ {\tt{1}}, {\it{ac\/}} $+$ {\it{i\/}})\index{prog-trans-of-sigma}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  functional-loop-invrt \\ \index{functional-loop-invrt}
({\it{ac\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{prog-trans-of-sigma}}\,({\it{i\/}}, {\it{ac\/}})\index{prog-trans-of-sigma} $=$ ({\it{ac\/}} $+$ {\rm{sigma}}\,({\tt{0}}, {\it{i\/}})\index{sigma}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-functional-sigma \\ \index{correctness-of-functional-sigma}
{\rm{prog-trans-of-sigma}}\,({\it{i\/}}, {\tt{0}})\index{prog-trans-of-sigma} $=$ {\rm{sigma}}\,({\tt{0}}, {\it{i\/}})\index{sigma}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sigma-input-path \\ \index{sigma-input-path}
({\tt{0}} $=$ {\rm{sigma}}\,({\it{k\/}}, {\it{k\/}})\index{sigma}) $\wedge$ ({\it{k\/}} $\leq$ {\it{k\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sigma-loop-invrt \\ \index{sigma-loop-invrt}
\=\+(({\it{i\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{i\/}} $\leq$ {\it{k\/}})) \\ 
$\rightarrow$$\;\;\;\;$((({\rm{sigma}}\,({\it{i\/}}, {\it{k\/}})\index{sigma} $+$ {\it{i\/}}) $=$ {\rm{sigma}}\,({\it{i\/}} $-\;1$, {\it{k\/}})\index{sigma}) $\wedge$ (({\it{i\/}} $-\;1$) $\leq$ {\it{k\/}}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sigma-output-path \\ \index{sigma-output-path}
(({\it{i\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{i\/}} $\leq$ {\it{k\/}})) $\rightarrow$ ({\rm{sigma}}\,({\it{i\/}}, {\it{k\/}})\index{sigma} $=$ {\rm{sigma}}\,({\tt{0}}, {\it{k\/}})\index{sigma})
\end{tabbing}

\begin{verbatim};   The interpreter we consider fetches instructions out of the same memory
;   being modified by the execution.  Earlier we proved a simpler version in
;   which the program was in read-only memory.  The new approach is almost
;   identical but we have to force the opening up of certain functions because
;   instead of doing CDR recursion the interpreter EXECUTE1 has to count the PC
;   up and the theorem prover doesn't handle counting up very well yet.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{set} \\  
\=\+{\rm{set}}\,({\it{addr\/}}, {\it{val\/}}, {\it{mem\/}})\index{set} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{addr\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cons}}\,({\it{val\/}}, {\rm{cdr}}\,({\it{mem\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{mem\/}}), {\rm{set}}\,({\it{addr\/}} $-\;1$, {\it{val\/}}, {\rm{cdr}}\,({\it{mem\/}}))\index{set})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{get} \\  
\=\+{\rm{get}}\,({\it{addr\/}}, {\it{mem\/}})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{addr\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{car}}\,({\it{mem\/}}) \\ 
{\bf else }{\rm{get}}\,({\it{addr\/}} $-\;1$, {\rm{cdr}}\,({\it{mem\/}}))\index{get}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  get-set \\ \index{get-set}
\=\+{\rm{get}}\,({\it{j\/}}, {\rm{set}}\,({\it{i\/}}, {\it{val\/}}, {\it{mem\/}})\index{set})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{eqp}}\,({\it{j\/}}, {\it{i\/}})\index{eqp}$\;\;${\bf then }{\it{val\/}} \\ 
{\bf else }{\rm{get}}\,({\it{j\/}}, {\it{mem\/}})\index{get}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{execute1} \\  
\=\+{\rm{execute1}}\,({\it{pc\/}}, {\it{mem\/}}, {\it{max\/}})\index{execute1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{pc\/}} $\not<$ {\it{max\/}}$\;\;${\bf then }{\rm{list}}\,({\bf{f}}, {\it{mem\/}}) \\ 
{\bf elseif }{\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get} $=$ {\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}$\;\;${\bf then }{\rm{list}}\,({\bf{f}}, {\it{mem\/}}) \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{jumpa}}$\;\;${\bf then }{\rm{list}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}}) \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{skipne}} \\ 
{\bf then }\=\+{\bf if }{\rm{get}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{get} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{execute1}}\,($1\;+$ {\it{pc\/}}, {\it{mem\/}}, {\it{max\/}})\index{execute1} \\ 
{\bf else }{\rm{execute1}}\,($1\;+$ ($1\;+$ {\it{pc\/}}), {\it{mem\/}}, {\it{max\/}})\index{execute1}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{subi}} \\ 
{\bf then }{\rm{execute1}}\,(\=\+$1\;+$ {\it{pc\/}}, \\ 
{\rm{set}}\,(\=\+{\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), \\ 
{\rm{get}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{get} $-$ {\rm{caddr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), \\ 
{\it{mem\/}})\-\index{set}, \\ 
{\it{max\/}})\-\index{execute1} \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{addi}} \\ 
{\bf then }{\rm{execute1}}\,(\=\+$1\;+$ {\it{pc\/}}, \\ 
{\rm{set}}\,(\=\+{\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), \\ 
{\rm{caddr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $+$ {\rm{get}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{get}, \\ 
{\it{mem\/}})\-\index{set}, \\ 
{\it{max\/}})\-\index{execute1} \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{add}} \\ 
{\bf then }{\rm{execute1}}\,(\=\+$1\;+$ {\it{pc\/}}, \\ 
{\rm{set}}\,(\=\+{\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), \\ 
\=\+{\rm{get}}\,({\rm{caddr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{get} \\ 
$+$$\;\;\;\;${\rm{get}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{get}\-, \\ 
{\it{mem\/}})\-\index{set}, \\ 
{\it{max\/}})\-\index{execute1} \\ 
{\bf elseif }{\rm{car}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}) $=$ {\tt{'}}{\tt{movei}} \\ 
{\bf then }{\rm{execute1}}\,(\=\+$1\;+$ {\it{pc\/}}, \\ 
{\rm{set}}\,({\rm{cadr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\rm{caddr}}\,({\rm{get}}\,({\it{pc\/}}, {\it{mem\/}})\index{get}), {\it{mem\/}})\index{set}, \\ 
{\it{max\/}})\-\index{execute1} \\ 
{\bf else }{\rm{list}}\,({\bf{f}}, {\it{mem\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{execute} \\  
\=\+{\rm{execute}}\,({\it{pc\/}}, {\it{mem\/}}, {\it{clk\/}})\index{execute} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clk\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{mem\/}} \\ 
{\bf elseif }{\it{pc\/}} $\in\;${\bf{N}}${}$ \\ 
{\bf then }{\rm{execute}}\,(\=\+{\rm{car}}\,({\rm{execute1}}\,({\it{pc\/}}, {\it{mem\/}}, {\rm{length}}\,({\it{mem\/}})\index{length})\index{execute1}), \\ 
{\rm{cadr}}\,({\rm{execute1}}\,({\it{pc\/}}, {\it{mem\/}}, {\rm{length}}\,({\it{mem\/}})\index{length})\index{execute1}), \\ 
{\it{clk\/}} $-\;1$)\-\index{execute} \\ 
{\bf else }{\it{mem\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{get-simplifier} \\  
\=\+{\rm{get-simplifier}}\,({\it{x\/}})\index{get-simplifier} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{get}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{cadr}}\,({\it{x\/}})) $=$ {\tt{'}}{\tt{quote}})\- \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\rm{cadr}}\,({\it{x\/}})) $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{list}}\,({\tt{'}}{\tt{car}}, {\rm{caddr}}\,({\it{x\/}})) \\ 
{\bf else }{\rm{list}}\,(\=\+{\tt{'}}{\tt{get}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\rm{cadr}}\,({\rm{cadr}}\,({\it{x\/}})) $-\;1$), \\ 
{\rm{list}}\,({\tt{'}}{\tt{cdr}}, {\rm{caddr}}\,({\it{x\/}})))\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-get-simplifier \\ \index{correctness-of-get-simplifier}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{get-simplifier}}\,({\it{x\/}})\index{get-simplifier}, {\it{a\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{set-simplifier} \\  
\=\+{\rm{set-simplifier}}\,({\it{x\/}})\index{set-simplifier} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{set}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cadr}}\,({\it{x\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{cadr}}\,({\it{x\/}})) $=$ {\tt{'}}{\tt{quote}})\- \\ 
{\bf then }\=\+{\bf if }{\rm{cadr}}\,({\rm{cadr}}\,({\it{x\/}})) $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{list}}\,({\tt{'}}{\tt{cons}}, {\rm{caddr}}\,({\it{x\/}}), {\rm{list}}\,({\tt{'}}{\tt{cdr}}, {\rm{cadddr}}\,({\it{x\/}}))) \\ 
{\bf else }{\rm{list}}\,(\=\+{\tt{'}}{\tt{cons}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{car}}, {\rm{cadddr}}\,({\it{x\/}})), \\ 
{\rm{list}}\,(\=\+{\tt{'}}{\tt{set}}, \\ 
{\rm{list}}\,({\tt{'}}{\tt{quote}}, {\rm{cadr}}\,({\rm{cadr}}\,({\it{x\/}})) $-\;1$), \\ 
{\rm{caddr}}\,({\it{x\/}}), \\ 
{\rm{list}}\,({\tt{'}}{\tt{cdr}}, {\rm{cadddr}}\,({\it{x\/}})))\-)\-$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-set-simplifier \\ \index{correctness-of-set-simplifier}
{\rm{eval\$}}\,({\bf{t}}, {\it{x\/}}, {\it{a\/}}) $=$ {\rm{eval\$}}\,({\bf{t}}, {\rm{set-simplifier}}\,({\it{x\/}})\index{set-simplifier}, {\it{a\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-5 \\ \index{length-5}
\=\+({\rm{caddddr}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{length}}\,({\it{x\/}})\index{length} $=$ ({\tt{5}} $+$ {\rm{length}}\,({\rm{cdddddr}}\,({\it{x\/}}))\index{length}))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-cons6 \\ \index{length-cons6}
\=\+{\rm{length}}\,({\rm{cons}}\,({\it{x1\/}}, {\rm{cons}}\,({\it{x2\/}}, {\rm{cons}}\,({\it{x3\/}}, {\rm{cons}}\,({\it{x4\/}}, {\rm{cons}}\,({\it{x5\/}}, {\rm{cons}}\,({\it{x6\/}}, {\it{x7\/}})))))))\index{length} \\ 
$=$$\;\;\;\;$({\tt{6}} $+$ {\rm{length}}\,({\it{x7\/}})\index{length})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  execute1-1 \\ \index{execute1-1}
\=\+({\it{max\/}} $\not<$ {\tt{6}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{execute1}}\,(\=\+{\tt{1}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{l\/}}))\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{car}}\,({\it{l\/}}) $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{execute1}}\,(\=\+{\tt{2}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{l\/}}))\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1} \\ 
{\bf else }{\rm{execute1}}\,(\=\+{\tt{3}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}\-, \\ 
{\it{l\/}})\-)\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  execute1-3 \\ \index{execute1-3}
\=\+({\it{max\/}} $\not<$ {\tt{6}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{execute1}}\,(\=\+{\tt{3}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{l\/}}))\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1} \\ 
$=$$\;\;\;\;${\rm{execute1}}\,(\=\+{\tt{4}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{l\/}}), \\ 
{\rm{cons}}\,(\=\+\=\+{\rm{car}}\,({\it{l\/}}) \\ 
$+$$\;\;\;\;${\rm{cadr}}\,({\it{l\/}})\-, \\ 
{\rm{cddr}}\,({\it{l\/}}))\-)\-)\-)\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  execute1-4 \\ \index{execute1-4}
\=\+({\it{max\/}} $\not<$ {\tt{6}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{execute1}}\,(\=\+{\tt{4}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{l\/}}))\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1} \\ 
$=$$\;\;\;\;${\rm{execute1}}\,(\=\+{\tt{5}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{l\/}}) $-$ {\tt{1}}, \\ 
{\rm{cdr}}\,({\it{l\/}}))\-)\-)\-)\-)\-)\-)\-, \\ 
{\it{max\/}})\-\index{execute1})\-\-
\end{tabbing}
%\item 
\begin{verbatim}

(PROVE-LEMMA
  EXECUTE1-OPENED-UP
  (REWRITE)
  (IMPLIES
    (AND (NOT (LESSP MAX 6))
         (EQUAL (CAR MEM)
                (QUOTE (MOVEI 7 0)))
         (EQUAL (CADR MEM)
                (QUOTE (SKIPNE 6)))
         (EQUAL (CADDR MEM)
                (QUOTE (STOP)))
         (EQUAL (CADDDR MEM)
                (QUOTE (ADD 7 6)))
         (EQUAL (CADDDDR MEM)
                (QUOTE (SUBI 6 1)))
         (EQUAL (CADDDDDR MEM)
                (QUOTE (JUMPA 1))))
    (EQUAL
      (EXECUTE1 1 MEM MAX)
      (IF
        (ZEROP (CADDDDDDR MEM))
        (LIST
          F
          (CONS
            (QUOTE (MOVEI 7 0))
            (CONS
              (QUOTE (SKIPNE 6))
              (CONS (QUOTE (STOP))
                    (CONS (QUOTE (ADD 7 6))
                          (CONS (QUOTE (SUBI 6 1))
                                (CONS (QUOTE (JUMPA 1))
                                      (CDDDDDDR MEM))))))))
        (LIST
          1
          (CONS
            (QUOTE (MOVEI 7 0))
            (CONS
              (QUOTE (SKIPNE 6))
              (CONS
                (QUOTE (STOP))
                (CONS
                  (QUOTE (ADD 7 6))
                  (CONS
                    (QUOTE (SUBI 6 1))
                    (CONS
                      (QUOTE (JUMPA 1))
                      (CONS (SUB1 (CADDDDDDR MEM))
                            (CONS (PLUS (CADDDDDDR MEM)
                                        (CADDDDDDDR MEM))
                                  (CDDDDDDDDR MEM))))))))))))))
\end{verbatim}

\begin{tabbing}{\sc Theorem}:  execute-opened-up \\ \index{execute-opened-up}
\=\+(({\it{pc\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{clk\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{execute}}\,({\it{pc\/}}, {\it{mem\/}}, {\it{clk\/}})\index{execute} \\ 
$=$$\;\;\;\;${\rm{execute}}\,(\=\+{\rm{car}}\,({\rm{execute1}}\,({\it{pc\/}}, {\it{mem\/}}, {\rm{length}}\,({\it{mem\/}})\index{length})\index{execute1}), \\ 
{\rm{cadr}}\,({\rm{execute1}}\,({\it{pc\/}}, {\it{mem\/}}, {\rm{length}}\,({\it{mem\/}})\index{length})\index{execute1}), \\ 
{\it{clk\/}} $-\;1$)\-\index{execute})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  interpreter-loop-invrt \\ \index{interpreter-loop-invrt}
\=\+(\=\+({\it{clk\/}} $\not<$ {\rm{caddddddr}}\,({\it{mem\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddr}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadddr}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{caddddr}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cadddddr}}\,({\it{mem\/}}) $=$ {\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{cadddddddr}}\,({\rm{execute}}\,({\tt{1}}, {\it{mem\/}}, {\it{clk\/}})\index{execute}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{caddddddr}}\,({\it{mem\/}}) $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{cadddddddr}}\,({\it{mem\/}}) \\ 
{\bf else }{\rm{cadddddddr}}\,({\it{mem\/}}) $+$ {\rm{sigma}}\,({\tt{0}}, {\rm{caddddddr}}\,({\it{mem\/}}))\index{sigma}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  interpreter-input-path \\ \index{interpreter-input-path}
\=\+{\rm{execute}}\,(\=\+{\tt{0}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, {\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{mem\/}})))\-)\-)\-)\-, \\ 
{\it{clk\/}})\-\index{execute} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clk\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, {\rm{cons}}\,({\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, {\it{mem\/}})))\-)\-)\-)\- \\ 
{\bf else }{\rm{execute}}\,(\=\+{\tt{1}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{stop}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}, \\ 
{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{mem\/}}), \\ 
{\rm{cons}}\,(\=\+{\tt{0}}, \\ 
{\rm{cddr}}\,({\it{mem\/}}))\-)\-)\-)\-)\-)\-)\-)\-, \\ 
{\it{clk\/}})\-\index{execute}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  correctness-of-interpreted-sigma \\ \index{correctness-of-interpreted-sigm!a}
\=\+(\=\+({\it{mem\/}} $=$ {\rm{append}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{movei}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{0}}{\tt{)}} \\ 
{\tt{(}}{\tt{skipne}}{\tt{ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{stop}}{\tt{)}} \\ 
{\tt{(}}{\tt{add}}{\tt{ }}{\tt{7}}{\tt{ }}{\tt{6}}{\tt{)}} \\ 
{\tt{(}}{\tt{subi}}{\tt{ }}{\tt{6}}{\tt{ }}{\tt{1}}{\tt{)}} \\ 
{\tt{(}}{\tt{jumpa}}{\tt{ }}{\tt{1}}{\tt{)}}{\tt{)}}\-, \\ 
{\it{tl\/}})\-) \\ 
$\wedge$$\;\;\;\;$({\it{i\/}} $=$ {\rm{get}}\,({\tt{6}}, {\it{mem\/}})\index{get}) \\ 
$\wedge$$\;\;\;\;$({\it{clk\/}} $\not<$ {\it{i\/}}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{get}}\,({\tt{7}}, {\rm{execute}}\,({\tt{0}}, {\it{mem\/}}, {\it{clk\/}})\index{execute})\index{get} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{clk\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{get}}\,({\tt{7}}, {\it{mem\/}})\index{get} \\ 
{\bf else }{\rm{sigma}}\,({\tt{0}}, {\it{i\/}})\index{sigma}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-2 \\ \index{difference-2}
(($1\;+$ ($1\;+$ {\it{x\/}})) $-$ {\tt{2}}) $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  half-plus \\ \index{half-plus}
(({\it{x\/}} $+$ ({\it{x\/}} $+$ {\it{y\/}})) $\div$ {\tt{2}}) $=$ ({\it{x\/}} $+$ ({\it{y\/}} $\div$ {\tt{2}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  sigma-is-half-product \\ \index{sigma-is-half-product}
{\rm{sigma}}\,({\tt{0}}, {\it{i\/}})\index{sigma} $=$ (({\it{i\/}} $*$ ($1\;+$ {\it{i\/}})) $\div$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  h-commutivity2 \\ \index{h-commutivity2}
{\rm{h}}\,({\it{x\/}}, {\rm{h}}\,({\it{y\/}}, {\it{z\/}})\index{h})\index{h} $=$ {\rm{h}}\,({\it{y\/}}, {\rm{h}}\,({\it{x\/}}, {\it{z\/}})\index{h})\index{h}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it h\/}.

\begin{tabbing}{\sc Definition}:\index{h-pr} \\  
\=\+{\rm{h-pr}}\,({\it{l\/}}, {\it{ac\/}})\index{h-pr} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{ac\/}} \\ 
{\bf else }{\rm{h}}\,({\rm{car}}\,({\it{l\/}}), {\rm{h-pr}}\,({\rm{cdr}}\,({\it{l\/}}), {\it{ac\/}})\index{h-pr})\index{h}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{h-ac} \\  
\=\+{\rm{h-ac}}\,({\it{l\/}}, {\it{ac\/}})\index{h-ac} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{l\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{ac\/}} \\ 
{\bf else }{\rm{h-ac}}\,({\rm{cdr}}\,({\it{l\/}}), {\rm{h}}\,({\rm{car}}\,({\it{l\/}}), {\it{ac\/}})\index{h})\index{h-ac}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  h-lemma \\ \index{h-lemma}
{\rm{h-pr}}\,({\it{x\/}}, {\rm{h}}\,({\it{z\/}}, {\it{a\/}})\index{h})\index{h-pr} $=$ {\rm{h}}\,({\it{z\/}}, {\rm{h-pr}}\,({\it{x\/}}, {\it{a\/}})\index{h-pr})\index{h}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  h-eq \\ \index{h-eq}
{\rm{h-ac}}\,({\it{l\/}}, {\it{ac\/}})\index{h-ac} $=$ {\rm{h-pr}}\,({\it{l\/}}, {\it{ac\/}})\index{h-pr}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{f0} \\  
\=\+{\rm{f0}}\,({\it{x\/}})\index{f0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\tt{100}} $<$ {\it{x\/}}$\;\;${\bf then }{\it{x\/}} $-$ {\tt{10}} \\ 
{\bf else }{\tt{91}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{verbatim}#|
(COMMENT
 (DEFN F91 (X)
       (EVAL$ T '(IF (LESSP 100 X)
                   (DIFFERENCE X 10)
                   (F91 (F91 (PLUS X 11))))
              (LIST (CONS 'X X))))

 (REFLECT F91 F0-SATISFIES-F91-EQUATION
          ((LESSP (DIFFERENCE 101 X))))

 (DEFN FOO (A) (IF (LESSP 100 (CDR (ASSOC 'X A)))
                 T
                 (FOO A)))

 (DEFN F91-INDUCTION-HINT (X A)
       (IF (LESSP 100 (CDR (ASSOC 'X A)))
         T
         (AND (F91-INDUCTION-HINT '(PLUS X 11) A)
              (F91-INDUCTION-HINT '(F0 (PLUS X 11)) A)))
       ((LESSP (DIFFERENCE 101 (EVAL$ T X A)))))

 (PROVE-LEMMA F91-TERMINATES ()
              (IMPLIES (V&C$ T X A)
                       (AND  (V&C$ T (LIST 'F91 X) A)
                             (EQUAL (CAR (V&C$ T (LIST 'F91 X) A))
                                    (F0 (CAR (V&C$ T X A))))))
              ((INDUCT (F91-INDUCTION-HINT X A))))
 (PROVE-LEMMA F91-IS-F0 ()
              (EQUAL (F91 X) (F0 X))))

|#
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{even}$\;\;$
{\rm{even}}\,({\it{x\/}})\index{even} $=$ ({\tt{0}} $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\tt{2}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{square}$\;\;$
{\rm{square}}\,({\it{x\/}})\index{square} $=$ ({\it{x\/}} $*$ {\it{x\/}})
\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-2 \\ \index{times-2}
({\tt{2}} $*$ {\it{x\/}}) $=$ ({\it{x\/}} $+$ {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-of-0 \\ \index{exp-of-0}
\=\+{\rm{exp}}\,({\tt{0}}, {\it{k\/}})\index{exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{k\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-of-1 \\ \index{exp-of-1}
{\rm{exp}}\,({\tt{1}}, {\it{k\/}})\index{exp} $=$ {\tt{1}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-by-0 \\ \index{exp-by-0}
{\rm{exp}}\,({\it{x\/}}, {\tt{0}})\index{exp} $=$ {\tt{1}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-times \\ \index{exp-times}
{\rm{exp}}\,({\it{i\/}} $*$ {\it{j\/}}, {\it{k\/}})\index{exp} $=$ ({\rm{exp}}\,({\it{i\/}}, {\it{k\/}})\index{exp} $*$ {\rm{exp}}\,({\it{j\/}}, {\it{k\/}})\index{exp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exp-exp \\ \index{exp-exp}
{\rm{exp}}\,({\rm{exp}}\,({\it{i\/}}, {\it{j\/}})\index{exp}, {\it{k\/}})\index{exp} $=$ {\rm{exp}}\,({\it{i\/}}, {\it{j\/}} $*$ {\it{k\/}})\index{exp}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-plus-times-1 \\ \index{remainder-plus-times-1}
(({\it{x\/}} $+$ ({\it{i\/}} $*$ {\it{j\/}})) ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-plus-times-2 \\ \index{remainder-plus-times-2}
(({\it{x\/}} $+$ ({\it{j\/}} $*$ {\it{i\/}})) ${}${\bf{mod}}${}$ {\it{j\/}}) $=$ ({\it{x\/}} ${}${\bf{mod}}${}$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-times-1 \\ \index{remainder-times-1}
(({\it{b\/}} $*$ ({\it{a\/}} $*$ {\it{c\/}})) ${}${\bf{mod}}${}$ {\it{a\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-of-1 \\ \index{remainder-of-1}
\=\+({\tt{1}} ${}${\bf{mod}}${}$ {\it{x\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  equal-length-0 \\ \index{equal-length-0}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}}) $=$ ({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-delete \\ \index{length-delete}
\=\+{\rm{length}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\in$ {\it{l\/}}$\;\;${\bf then }{\rm{length}}\,({\rm{cdr}}\,({\it{l\/}}))\index{length} \\ 
{\bf else }{\rm{length}}\,({\it{l\/}})\index{length}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  remainder-difference-times \\ \index{remainder-difference-times}
((({\it{p\/}} $*$ {\it{x\/}}) $-$ ({\it{p\/}} $*$ {\it{y\/}})) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  prime-key-rewrite \\ \index{prime-key-rewrite}
\=\+{\rm{prime}}\,({\it{p\/}})\index{prime} \\ 
$\rightarrow$$\;\;\;\;$(\=\+((({\it{a\/}} $*$ {\it{b\/}}) ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) \\ 
$=$$\;\;\;\;$((({\it{a\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}}) $\vee$ (({\it{b\/}} ${}${\bf{mod}}${}$ {\it{p\/}}) $=$ {\tt{0}})))\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-times-list-delete \\ \index{times-times-list-delete}
({\it{x\/}} $\in$ {\it{l\/}}) $\rightarrow$ (({\it{x\/}} $*$ {\rm{times-list}}\,({\rm{delete}}\,({\it{x\/}}, {\it{l\/}})\index{delete})\index{times-list}) $=$ {\rm{times-list}}\,({\it{l\/}})\index{times-list})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-remainder-divisor \\ \index{lessp-remainder-divisor}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} ${}${\bf{mod}}${}$ {\it{y\/}}) $<$ {\it{y\/}})
\end{tabbing}

\noindent{\sc Event}:   Introduce the function symbol {\it apply2\index{apply2}\/} of 3 arguments.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{eval2} \\  
\=\+{\rm{eval2}}\,({\it{form\/}}, {\it{envrn\/}})\index{eval2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{form\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{form\/}} \\ 
{\bf elseif }{\rm{litatom}}\,({\it{form\/}})$\;\;${\bf then }{\rm{cdr}}\,({\rm{assoc}}\,({\it{form\/}}, {\it{envrn\/}})) \\ 
{\bf elseif }{\rm{listp}}\,({\it{form\/}}) \\ 
{\bf then }{\rm{apply2}}\,(\=\+{\rm{car}}\,({\it{form\/}}), \\ 
{\rm{eval2}}\,({\rm{cadr}}\,({\it{form\/}}), {\it{envrn\/}})\index{eval2}, \\ 
{\rm{eval2}}\,({\rm{caddr}}\,({\it{form\/}}), {\it{envrn\/}})\index{eval2})\-\index{apply2} \\ 
{\bf else }{\it{form\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{subst2} \\  
\=\+{\rm{subst2}}\,({\it{new\/}}, {\it{old\/}}, {\it{term\/}})\index{subst2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{term\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{term\/}} \\ 
{\bf elseif }{\rm{litatom}}\,({\it{term\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{old\/}} $=$ {\it{term\/}}$\;\;${\bf then }{\it{new\/}} \\ 
{\bf else }{\it{term\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{listp}}\,({\it{term\/}}) \\ 
{\bf then }{\rm{list}}\,(\=\+{\rm{car}}\,({\it{term\/}}), \\ 
{\rm{subst2}}\,({\it{new\/}}, {\it{old\/}}, {\rm{cadr}}\,({\it{term\/}}))\index{subst2}, \\ 
{\rm{subst2}}\,({\it{new\/}}, {\it{old\/}}, {\rm{caddr}}\,({\it{term\/}}))\index{subst2})\- \\ 
{\bf else }{\it{term\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  subst2-ok \\ \index{subst2-ok}
\=\+{\rm{eval2}}\,({\rm{subst2}}\,({\it{new\/}}, {\it{old\/}}, {\it{term\/}})\index{subst2}, {\it{a\/}})\index{eval2} \\ 
$=$$\;\;\;\;${\rm{eval2}}\,({\it{term\/}}, {\rm{cons}}\,({\rm{cons}}\,({\it{old\/}}, {\rm{eval2}}\,({\it{new\/}}, {\it{a\/}})\index{eval2}), {\it{a\/}}))\index{eval2}\-
\end{tabbing}


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

\addvspace{18pt}

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