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

\begin{verbatim}#|

 Copyright (C) 1994 by Computational Logic, Inc. and Paolo Pecchiari.  All
 Rights Reserved. 

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

 NO WARRANTY

 Computational Logic, Inc. AND Paolo Pecchiari 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 Computational Logic, Inc. OR Paolo Pecchiari 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.
|#

; Events from CLI Technical Report 100, ``Interaction with the Boyer-Moore
; Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean
; Theorem,'' by Matt Kaufmann and Paolo Pecchiari.

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{sumlist} \\  
\=\+{\rm{sumlist}}\,({\it{lst\/}})\index{sumlist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}})$\;\;${\bf then }{\rm{car}}\,({\it{lst\/}}) $+$ {\rm{sumlist}}\,({\rm{cdr}}\,({\it{lst\/}}))\index{sumlist} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\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 Definition}:\index{maxlist} \\  
\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))$\;\;${\bf then }{\rm{max}}\,({\rm{car}}\,({\it{x\/}}), {\rm{maxlist}}\,({\rm{cdr}}\,({\it{x\/}}))\index{maxlist}) \\ 
{\bf else }{\rm{fix}}\,({\rm{car}}\,({\it{x\/}}))$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Definition}:\index{minlist} \\  
\=\+{\rm{minlist}}\,({\it{x\/}})\index{minlist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}}))$\;\;${\bf then }{\rm{min}}\,({\rm{car}}\,({\it{x\/}}), {\rm{minlist}}\,({\rm{cdr}}\,({\it{x\/}}))\index{minlist})\index{min} \\ 
{\bf else }{\rm{fix}}\,({\rm{car}}\,({\it{x\/}}))$\;${\bf  endif}\- \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{delete1} \\  
\=\+{\rm{delete1}}\,({\it{elt\/}}, {\it{x\/}})\index{delete1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{elt\/}} $=$ {\rm{car}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{x\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{delete1}}\,({\it{elt\/}}, {\rm{cdr}}\,({\it{x\/}}))\index{delete1})$\;${\bf  endif}\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-delete1-rearrange \\ \index{maxlist-delete1-rearrange}
({\it{b\/}} $\in$ {\it{x\/}}) $\rightarrow$ ({\rm{maxlist}}\,({\rm{cons}}\,({\it{b\/}}, {\rm{delete1}}\,({\it{b\/}}, {\it{x\/}})\index{delete1}))\index{maxlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})
\end{tabbing}


\noindent{\sc Event}:   Let us define the theory {\it{induction-fn-disables}} to consist of the following events: sumlist,
times,
length,
minlist,
maxlist,
delete1,
occurrences.\index{induction-fn-disables}

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  max-greater-than-average \\ \index{max-greater-than-average}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\geq$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) $\wedge$ ({\rm{fix}}\,({\it{k\/}}) $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})) \\ 
$\rightarrow$$\;\;\;\;$({\it{k\/}} $<$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  min-less-than-average \\ \index{min-less-than-average}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\leq$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) $\wedge$ ({\rm{fix}}\,({\it{k\/}}) $\not=$ {\rm{minlist}}\,({\it{x\/}})\index{minlist})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $<$ {\it{k\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-monotone-1 \\ \index{times-monotone-1}
({\it{u\/}} $\not<$ {\it{v\/}}) $\rightarrow$ (({\it{u\/}} $*$ {\it{y\/}}) $\not<$ ({\it{v\/}} $*$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-times-preserved-in-first-arg \\ \index{lessp-times-preserved-in-first-!arg}
(({\it{a\/}} $\not<$ ({\it{u\/}} $*$ {\it{y\/}})) $\wedge$ ({\it{u\/}} $\not<$ {\it{v\/}})) $\rightarrow$ ({\it{a\/}} $\not<$ ({\it{v\/}} $*$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-main-property \\ \index{minlist-main-property}
{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\not<$ ({\rm{length}}\,({\it{x\/}})\index{length} $*$ {\rm{minlist}}\,({\it{x\/}})\index{minlist})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-not-maxlist-implies-minlist-lessp-average-lemma \\ \index{minlist-not-maxlist-implies-min!list-lessp-average-lemma}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ (({\rm{minlist}}\,({\it{x\/}})\index{minlist} $*$ {\rm{length}}\,({\it{x\/}})\index{length}) $<$ {\rm{sumlist}}\,({\it{x\/}})\index{sumlist})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-not-maxlist-implies-minlist-lessp-average \\ \index{minlist-not-maxlist-implies-min!list-lessp-average}
\=\+(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $<$ {\rm{fix}}\,({\it{k\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-main-property \\ \index{maxlist-main-property}
({\rm{length}}\,({\it{x\/}})\index{length} $*$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\not<$ {\rm{sumlist}}\,({\it{x\/}})\index{sumlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-not-maxlist-implies-maxlist-greaterp-average-lemma \\ \index{minlist-not-maxlist-implies-max!list-greaterp-average-lemma}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $<$ ({\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $*$ {\rm{length}}\,({\it{x\/}})\index{length}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-not-maxlist-implies-maxlist-greaterp-average \\ \index{minlist-not-maxlist-implies-max!list-greaterp-average}
\=\+(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{fix}}\,({\it{k\/}}) $<$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-less-than-maxlist-minus-1 \\ \index{minlist-less-than-maxlist-minus!-1}
\=\+(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $<$ ({\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-delete1-leq \\ \index{maxlist-delete1-leq}
{\rm{maxlist}}\,({\it{lst\/}})\index{maxlist} $\not<$ {\rm{maxlist}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{lst\/}})\index{delete1})\index{maxlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-implies-maxlist-geq \\ \index{member-implies-maxlist-geq}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ ({\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $\not<$ {\it{a\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete1-preserves-maxlist-when-maxlist-occurs-more-than-once \\ \index{delete1-preserves-maxlist-when-!maxlist-occurs-more-than-once}
\=\+({\tt{1}} $<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{maxlist}}\,({\rm{delete1}}\,({\it{any-element\/}}, {\it{x\/}})\index{delete1})\index{maxlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  delete1-occurrences \\ \index{delete1-occurrences}
\=\+{\rm{occurrences}}\,({\it{a\/}}, {\rm{delete1}}\,({\it{b\/}}, {\it{x\/}})\index{delete1})\index{occurrences} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{a\/}} $=$ {\it{b\/}}) $\wedge$ ({\it{b\/}} $\in$ {\it{x\/}})$\;\;${\bf then }{\rm{occurrences}}\,({\it{a\/}}, {\it{x\/}})\index{occurrences} $-\;1$ \\ 
{\bf else }{\rm{occurrences}}\,({\it{a\/}}, {\it{x\/}})\index{occurrences}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  occurrence-implies-listp \\ \index{occurrence-implies-listp}
({\tt{1}} $<$ {\rm{occurrences}}\,({\it{a\/}}, {\it{x\/}})\index{occurrences}) $\rightarrow$ ({\rm{listp}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1}) $=$ {\bf{t}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-geq-minlist \\ \index{maxlist-geq-minlist}
{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $\not<$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2-max-occurs-twice-lemma-1 \\ \index{induction-fn-help-2-max-occurs-t!wice-lemma-1}
\=\+(\=\+({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{maxlist}}\,({\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-)\index{maxlist} \\ 
$=$$\;\;\;\;${\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-delete1 \\ \index{member-delete1}
\=\+({\it{a\/}} $\in$ {\rm{delete1}}\,({\it{b\/}}, {\it{c\/}})\index{delete1}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $=$ {\it{b\/}}$\;\;${\bf then }{\tt{1}} $<$ {\rm{occurrences}}\,({\it{b\/}}, {\it{c\/}})\index{occurrences} \\ 
{\bf else }{\it{a\/}} $\in$ {\it{c\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-implies-listp \\ \index{member-implies-listp}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2-max-occurs-twice-lemma-2 \\ \index{induction-fn-help-2-max-occurs-t!wice-lemma-2}
\=\+(\=\+({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{occurrences}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, \\ 
{\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-)\-\index{occurrences} \\ 
$<$$\;\;\;\;${\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}


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

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2-max-occurs-twice \\ \index{induction-fn-help-2-max-occurs-t!wice}
\=\+{\bf let }\=\+{\it{x0\/}}{\bf $\;$ be$\;\;$}{\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ord-lessp}}\,(\=\+{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\it{x0\/}})\index{occurrences}), \\ 
{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-not-minlist-implies-listp \\ \index{maxlist-not-minlist-implies-listp}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ {\rm{listp}}\,({\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  minlist-less-than-maxlist-minus-1-better \\ \index{minlist-less-than-maxlist-minus!-1-better}
\=\+(({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) $\wedge$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $<$ ({\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$))\-
\end{tabbing}


\noindent{\sc Event}:   Disable minlist-less-than-maxlist-minus-1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  maxlist-delete1-delete1 \\ \index{maxlist-delete1-delete1}
{\rm{maxlist}}\,({\rm{delete1}}\,({\it{b\/}}, {\it{x\/}})\index{delete1})\index{maxlist} $\not<$ {\rm{maxlist}}\,({\rm{delete1}}\,({\it{b\/}}, {\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{delete1})\index{maxlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-maxlist \\ \index{member-maxlist}
({\rm{maxlist}}\,({\it{z\/}})\index{maxlist} $\not=$ {\tt{0}}) $\rightarrow$ ({\rm{maxlist}}\,({\it{z\/}})\index{maxlist} $\in$ {\it{z\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-maxlist-delete1-maxlist \\ \index{lessp-maxlist-delete1-maxlist}
\=\+(({\tt{0}} $<$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\wedge$ ({\tt{1}} $\not<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{maxlist}}\,({\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{delete1})\index{maxlist} $<$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2-max-occurs-once-main-lemma \\ \index{induction-fn-help-2-max-occurs-!once-main-lemma}
\=\+(\=\+({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $\not<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{maxlist}}\,({\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-)\index{maxlist} \\ 
$<$$\;\;\;\;${\rm{maxlist}}\,({\it{x\/}})\index{maxlist})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2-max-occurs-once \\ \index{induction-fn-help-2-max-occurs-!once}
\=\+{\bf let }\=\+{\it{x0\/}}{\bf $\;$ be$\;\;$}{\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-\- \\ 
{\bf in} \\ 
\=\+(\=\+({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $\not<$ {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{ord-lessp}}\,(\=\+{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\it{x0\/}})\index{occurrences}), \\ 
{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\-\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  induction-fn-help-2 \\ \index{induction-fn-help-2}
\=\+{\bf let }\=\+{\it{x0\/}}{\bf $\;$ be$\;\;$}{\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\index{delete1})\-)\-\- \\ 
{\bf in} \\ 
\=\+(({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) $\wedge$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})) \\ 
$\rightarrow$$\;\;\;\;${\rm{ord-lessp}}\,(\=\+{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x0\/}})\index{maxlist}, {\it{x0\/}})\index{occurrences}), \\ 
{\rm{cons}}\,($1\;+$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\rm{occurrences}}\,({\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, {\it{x\/}})\index{occurrences}))\-\-$\;${\bf  endlet}\-
\end{tabbing}


\noindent{\sc Event}:   Disable theory induction-fn-disables.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{induction-fn} \\  
\=\+{\rm{induction-fn}}\,({\it{x\/}}, {\it{k\/}})\index{induction-fn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\not=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{induction-fn}}\,(\=\+{\rm{cons}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $-\;1$, \\ 
{\rm{cons}}\,(\=\+$1\;+$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}, \\ 
{\rm{delete1}}\,(\=\+{\rm{maxlist}}\,({\it{x\/}})\index{maxlist}, \\ 
{\rm{delete1}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\it{x\/}})\index{delete1})\-\index{delete1})\-)\-, \\ 
{\it{k\/}})\-\index{induction-fn}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Enable theory induction-fn-disablesinduction-fn-disables.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  sumlist-delete1-plus-version \\ \index{sumlist-delete1-plus-version}
\=\+({\it{a\/}} $+$ {\rm{sumlist}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{sumlist}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} \\ 
{\bf else }{\it{a\/}} $+$ {\rm{sumlist}}\,({\it{x\/}})\index{sumlist}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-delete1 \\ \index{sumlist-delete1}
\=\+{\rm{sumlist}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{sumlist} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $-$ {\it{a\/}} \\ 
{\bf else }{\rm{sumlist}}\,({\it{x\/}})\index{sumlist}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  maxlist-0-is-sumlist-0 \\ \index{maxlist-0-is-sumlist-0}
({\rm{maxlist}}\,({\it{x\/}})\index{maxlist} $=$ {\tt{0}}) $=$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-lemma-base-case-lemma-1 \\ \index{main-lemma-base-case-lemma-1}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ ({\rm{exp}}\,({\rm{minlist}}\,({\it{x\/}})\index{minlist}, {\rm{length}}\,({\it{x\/}})\index{length})\index{exp} $=$ {\rm{prodlist}}\,({\it{x\/}})\index{prodlist})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-lemma-base-case-lemma-2-lemma \\ \index{main-lemma-base-case-lemma-2-le!mma}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $*$ {\rm{length}}\,({\it{x\/}})\index{length}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-lemma-base-case-lemma-2-hack \\ \index{main-lemma-base-case-lemma-2-ha!ck}
\=\+((({\it{k\/}} $*$ {\it{n\/}}) $=$ {\it{sumlist\/}}) $\wedge$ ({\it{n\/}} $\not\simeq {\tt{0}}$) $\wedge$ (({\it{n\/}} $*$ {\it{maxlist\/}}) $=$ {\it{sumlist\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{fix}}\,({\it{k\/}}) $=$ {\rm{fix}}\,({\it{maxlist\/}}))\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  main-lemma-base-case-lemma-2 \\ \index{main-lemma-base-case-lemma-2}
\=\+(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\wedge$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{fix}}\,({\it{k\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-lemma-base-case \\ \index{main-lemma-base-case}
\=\+(({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\rm{length}}\,({\it{x\/}})\index{length})) $\wedge$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{exp}}\,({\it{k\/}}, {\rm{length}}\,({\it{x\/}})\index{length})\index{exp} $=$ {\rm{prodlist}}\,({\it{x\/}})\index{prodlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-delete1 \\ \index{length-delete1}
\=\+{\rm{length}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $\in$ {\it{x\/}}$\;\;${\bf then }{\rm{length}}\,({\it{x\/}})\index{length} $-\;1$ \\ 
{\bf else }{\rm{length}}\,({\it{x\/}})\index{length}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{numberp-listp} \\  
\=\+{\rm{numberp-listp}}\,({\it{x\/}})\index{numberp-listp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }({\rm{car}}\,({\it{x\/}}) $\in\;${\bf{N}}${}$) $\wedge$ {\rm{numberp-listp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{numberp-listp} \\ 
{\bf else }{\it{x\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-minlist \\ \index{member-minlist}
({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{numberp-listp}}\,({\it{x\/}})\index{numberp-listp}) $\rightarrow$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\in$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-listp-delete1 \\ \index{numberp-listp-delete1}
{\rm{numberp-listp}}\,({\it{x\/}})\index{numberp-listp} $\rightarrow$ {\rm{numberp-listp}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{numberp-listp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  add1-plus-sub1-second \\ \index{add1-plus-sub1-second}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (($1\;+$ ({\it{x\/}} $+$ ({\it{y\/}} $-\;1$))) $=$ ({\it{x\/}} $+$ {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-geq-maxlist \\ \index{sumlist-geq-maxlist}
{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\not<$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-geq-minlist \\ \index{sumlist-geq-minlist}
{\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\not<$ {\rm{minlist}}\,({\it{x\/}})\index{minlist}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-geq-minlist-plus-maxlist \\ \index{sumlist-geq-minlist-plus-maxlist}
\=\+({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $\not<$ ({\rm{minlist}}\,({\it{x\/}})\index{minlist} $+$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable plus.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  plus-times-sub1-second \\ \index{plus-times-sub1-second}
({\it{y\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ (({\it{x\/}} $+$ ({\it{x\/}} $*$ ({\it{y\/}} $-\;1$))) $=$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable times.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  minlist-not-maxlist-implies-length-at-least-2 \\ \index{minlist-not-maxlist-implies-len!gth-at-least-2}
({\rm{minlist}}\,({\it{x\/}})\index{minlist} $\not=$ {\rm{maxlist}}\,({\it{x\/}})\index{maxlist}) $\rightarrow$ ({\tt{1}} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}


\noindent{\sc Event}:   Disable plus-add1-arg1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable plus-add1-arg2.

\addvspace{18pt}


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

\addvspace{18pt}


\noindent{\sc Event}:   Disable maxlist-0-is-sumlist-0.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  times-prodlist-delete1 \\ \index{times-prodlist-delete1}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ (({\it{a\/}} $*$ {\rm{prodlist}}\,({\rm{delete1}}\,({\it{a\/}}, {\it{x\/}})\index{delete1})\index{prodlist}) $=$ {\rm{prodlist}}\,({\it{x\/}})\index{prodlist})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  product-of-modified-list-lemma \\ \index{product-of-modified-list-lemma}
\=\+(({\it{min\/}} $\not=$ {\it{max\/}}) $\wedge$ ({\it{min\/}} $\in$ {\it{x\/}}) $\wedge$ ({\it{max\/}} $\in$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\it{max\/}} $*$ {\it{min\/}} $*$ {\rm{prodlist}}\,({\rm{delete1}}\,({\it{max\/}}, {\rm{delete1}}\,({\it{min\/}}, {\it{x\/}})\index{delete1})\index{delete1})\index{prodlist}) \\ 
$=$$\;\;\;\;${\rm{prodlist}}\,({\it{x\/}})\index{prodlist})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable times-prodlist-delete1.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  product-of-modified-list-lemma-2 \\ \index{product-of-modified-list-lemma-!2}
\=\+(({\it{min\/}} $<$ {\it{max\/}}) $\wedge$ ({\it{max\/}} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(($1\;+$ {\it{min\/}}) $*$ ({\it{max\/}} $-\;1$) $*$ {\it{rest\/}}) \\ 
$=$$\;\;\;\;$(({\it{min\/}} $*$ {\it{max\/}} $*$ {\it{rest\/}}) $+$ (({\it{max\/}} $-$ ($1\;+$ {\it{min\/}})) $*$ {\it{rest\/}})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  positive-implies-numberp \\ \index{positive-implies-numberp}
({\it{min\/}} $<$ {\it{max\/}}) $\rightarrow$ ({\it{max\/}} $\in\;${\bf{N}}${}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  product-of-modified-list \\ \index{product-of-modified-list}
\=\+(({\it{min\/}} $<$ {\it{max\/}}) $\wedge$ ({\it{min\/}} $\in$ {\it{x\/}}) $\wedge$ ({\it{max\/}} $\in$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf let }\=\+{\it{rest\/}}{\bf $\;$ be$\;\;$}{\rm{prodlist}}\,({\rm{delete1}}\,({\it{max\/}}, {\rm{delete1}}\,({\it{min\/}}, {\it{x\/}})\index{delete1})\index{delete1})\index{prodlist}\- \\ 
{\bf in} \\ 
\=\+(($1\;+$ {\it{min\/}}) $*$ ({\it{max\/}} $-\;1$) $*$ {\it{rest\/}}) \\ 
$=$$\;\;\;\;$({\rm{prodlist}}\,({\it{x\/}})\index{prodlist} $+$ (({\it{max\/}} $-$ ($1\;+$ {\it{min\/}})) $*$ {\it{rest\/}}))\-$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-lemma \\ \index{main-lemma}
\=\+{\bf let }\=\+{\it{n\/}}{\bf $\;$ be$\;\;$}{\rm{length}}\,({\it{x\/}})\index{length}\- \\ 
{\bf in} \\ 
\=\+({\rm{numberp-listp}}\,({\it{x\/}})\index{numberp-listp} $\wedge$ ({\rm{sumlist}}\,({\it{x\/}})\index{sumlist} $=$ ({\it{k\/}} $*$ {\it{n\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{exp}}\,({\it{k\/}}, {\it{n\/}})\index{exp} $\not<$ {\rm{prodlist}}\,({\it{x\/}})\index{prodlist})\-$\;${\bf  endlet}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{scalar-product} \\  
\=\+{\rm{scalar-product}}\,({\it{scalar\/}}, {\it{lst\/}})\index{scalar-product} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{lst\/}}) \\ 
{\bf then }{\rm{cons}}\,({\it{scalar\/}} $*$ {\rm{car}}\,({\it{lst\/}}), {\rm{scalar-product}}\,({\it{scalar\/}}, {\rm{cdr}}\,({\it{lst\/}}))\index{scalar-product}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-scalar-product \\ \index{sumlist-scalar-product}
{\rm{sumlist}}\,({\rm{scalar-product}}\,({\it{scalar\/}}, {\it{lst\/}})\index{scalar-product})\index{sumlist} $=$ ({\it{scalar\/}} $*$ {\rm{sumlist}}\,({\it{lst\/}})\index{sumlist})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prodlist-scalar-product \\ \index{prodlist-scalar-product}
\=\+{\rm{prodlist}}\,({\rm{scalar-product}}\,({\it{scalar\/}}, {\it{lst\/}})\index{scalar-product})\index{prodlist} \\ 
$=$$\;\;\;\;$({\rm{exp}}\,({\it{scalar\/}}, {\rm{length}}\,({\it{lst\/}})\index{length})\index{exp} $*$ {\rm{prodlist}}\,({\it{lst\/}})\index{prodlist})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  length-scalar-product \\ \index{length-scalar-product}
{\rm{length}}\,({\rm{scalar-product}}\,({\it{n\/}}, {\it{a\/}})\index{scalar-product})\index{length} $=$ {\rm{length}}\,({\it{a\/}})\index{length}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  numberp-listp-scalar-product \\ \index{numberp-listp-scalar-product}
{\rm{numberp-listp}}\,({\it{a\/}})\index{numberp-listp} $\rightarrow$ {\rm{numberp-listp}}\,({\rm{scalar-product}}\,({\it{n\/}}, {\it{a\/}})\index{scalar-product})\index{numberp-listp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main \\ \index{main}
\=\+{\rm{numberp-listp}}\,({\it{a\/}})\index{numberp-listp} \\ 
$\rightarrow$$\;\;\;\;$\=\+{\bf let }\=\+{\it{n\/}}{\bf $\;$ be$\;\;$}{\rm{length}}\,({\it{a\/}})\index{length}\- \\ 
{\bf in} \\ 
{\rm{exp}}\,({\rm{sumlist}}\,({\it{a\/}})\index{sumlist}, {\it{n\/}})\index{exp} $\geq$ ({\rm{exp}}\,({\it{n\/}}, {\it{n\/}})\index{exp} $*$ {\rm{prodlist}}\,({\it{a\/}})\index{prodlist})$\;${\bf  endlet}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sumlist-for \\ \index{sumlist-for}
\=\+{\rm{sumlist}}\,({\it{a\/}})\index{sumlist} \\ 
$=$$\;\;\;\;$\=\+{\bf for }{\it{x\/}}{\bf $\;$ in }{\it{a\/}} \\ 
{\bf sum} {\it{x\/}}$\;${{\bf  endfor}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  prodlist-for \\ \index{prodlist-for}
\=\+{\rm{prodlist}}\,({\it{a\/}})\index{prodlist} \\ 
$=$$\;\;\;\;$\=\+{\bf for }{\it{x\/}}{\bf $\;$ in }{\it{a\/}} \\ 
{\bf multiply} {\it{x\/}}$\;${{\bf  endfor}}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  main-again \\ \index{main-again}
\=\+({\rm{numberp-listp}}\,({\it{a\/}})\index{numberp-listp} $\wedge$ ({\it{n\/}} $=$ {\rm{length}}\,({\it{a\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{exp}}\,(\=\+\=\+{\bf for }{\it{x\/}}{\bf $\;$ in }{\it{a\/}} \\ 
{\bf sum} {\it{x\/}}$\;${{\bf  endfor}}\-, \\ 
{\it{n\/}})\-\index{exp} \\ 
$\geq$$\;\;\;\;$(\=\+{\rm{exp}}\,({\it{n\/}}, {\it{n\/}})\index{exp} \\ 
$*$$\;\;\;\;$\=\+{\bf for }{\it{x\/}}{\bf $\;$ in }{\it{a\/}} \\ 
{\bf multiply} {\it{x\/}}$\;${{\bf  endfor}}\-)\-)\-\-
\end{tabbing}

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