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

\begin{verbatim}#|

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

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

 NO WARRANTY

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

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

;; Matt Kaufmann

;; Here are some games with "partial functions".....

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

\addvspace{18pt}

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


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

\addvspace{18pt}

\begin{verbatim};; Example 1:  a simple total reflexive function that's actually
;; the identity function on natural numbers.

;; dcls, add-axioms, and rewrite rules for g-cost and g (6 events)

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it g-cost\index{g-cost}\/} of one argument.

\addvspace{18pt}


\noindent{\sc Event}:   Introduce the function symbol {\it g\index{g}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  g-defn \\ \index{g-defn}
\=\+{\rm{g}}\,({\it{x\/}})\index{g} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{g-cost}}\,({\it{x\/}})\index{g-cost} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{g}}\,({\rm{g}}\,({\it{x\/}} $-\;1$)\index{g})\index{g}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{g}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  g-cost-defn \\ \index{g-cost-defn}
\=\+{\rm{g-cost}}\,({\it{x\/}})\index{g-cost} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{s-plus}}\,({\tt{1}}, {\rm{s-plus}}\,({\rm{g-cost}}\,({\it{x\/}} $-\;1$)\index{g-cost}, {\rm{g-cost}}\,({\rm{g}}\,({\it{x\/}} $-\;1$)\index{g})\index{g-cost})\index{s-plus})\index{s-plus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g-cost-opener \\ \index{g-cost-opener}
\=\+(({\it{x\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{g-cost}}\,({\it{x\/}})\index{g-cost} $=$ {\tt{1}})) \\ 
$\wedge$$\;\;\;\;$(\=\+({\it{x\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{g-cost}}\,({\it{x\/}})\index{g-cost} \\ 
$=$$\;\;\;\;${\rm{s-plus}}\,({\tt{1}}, {\rm{s-plus}}\,({\rm{g-cost}}\,({\it{x\/}} $-\;1$)\index{g-cost}, {\rm{g-cost}}\,({\rm{g}}\,({\it{x\/}} $-\;1$)\index{g})\index{g-cost})\index{s-plus})\index{s-plus})\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g-opener \\ \index{g-opener}
\=\+(\=\+({\it{x\/}} $\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{g}}\,({\it{x\/}})\index{g} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{g-cost}}\,({\it{x\/}})\index{g-cost}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{g}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+({\it{x\/}} $\not\simeq {\tt{0}}$) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{g}}\,({\it{x\/}})\index{g} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{g-cost}}\,({\it{x\/}})\index{g-cost}$\;\;${\bf then }$1\;+$ {\rm{g}}\,({\rm{g}}\,({\it{x\/}} $-\;1$)\index{g})\index{g} \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{g}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-)\-)\-\-
\end{tabbing}

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

\begin{verbatim};; Example 2:  Silly factorial

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{isub1} \\  
\=\+{\rm{isub1}}\,({\it{x\/}})\index{isub1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{negativep}}\,({\it{x\/}})$\;\;${\bf then }$-$ ($1\;+$ {\rm{negative-guts}}\,({\it{x\/}})) \\ 
{\bf else }{\it{x\/}} $-\;1$$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; dcls, add-axioms, and rewrite rules for fact-cost and fact (5 events).
;; Note that we don't try to make a rewrite rule for the nonterminating
;; case.  Also, since our function isn't reflexive and we are only interested
;; in termination, we only bother to prove a rewrite rule for opening up
;; fact-cost, not one for opening up fact.

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it fact-cost\index{fact-cost}\/} of one argument.

\addvspace{18pt}


\noindent{\sc Event}:   Introduce the function symbol {\it fact\index{fact}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  fact-defn \\ \index{fact-defn}
\=\+{\rm{fact}}\,({\it{x\/}})\index{fact} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost} \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{fact}}\,({\rm{isub1}}\,({\it{x\/}})\index{isub1})\index{fact}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{fact}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  fact-cost-defn \\ \index{fact-cost-defn}
\=\+{\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $=$ {\tt{0}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{s-plus}}\,({\tt{1}}, {\rm{fact-cost}}\,({\rm{isub1}}\,({\it{x\/}})\index{isub1})\index{fact-cost})\index{s-plus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fact-cost-opener-numberp \\ \index{fact-cost-opener-numberp}
\=\+(({\it{x\/}} $=$ {\tt{0}}) $\rightarrow$ ({\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost} $=$ {\tt{1}})) \\ 
$\wedge$$\;\;\;\;$(({\it{x\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost} $=$ {\rm{s-plus}}\,({\tt{1}}, {\rm{fact-cost}}\,({\it{x\/}} $-\;1$)\index{fact-cost})\index{s-plus}))\-
\end{tabbing}

\begin{verbatim};; Now let's first note when fact IS defined.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  fact-defined-numberp \\ \index{fact-defined-numberp}
({\it{x\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ {\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fact-defined-other \\ \index{fact-defined-other}
(({\it{x\/}} $\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{negativep}}\,({\it{x\/}}))) $\rightarrow$ {\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost}
\end{tabbing}

\begin{verbatim};; Next, let's show that fact is undefined on the negatives by
;; showing that the cost is arbitrarily high (the usual trick
;; used for analogous v&c$ proofs).

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fact-undefined-ind} \\  
\=\+{\rm{fact-undefined-ind}}\,({\it{x\/}}, {\it{n\/}})\index{fact-undefined-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{fact-undefined-ind}}\,($1\;+$ {\it{x\/}}, {\it{n\/}} $-\;1$)\index{fact-undefined-ind}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fact-undefined-numberp-lemma-inductive-step \\ \index{fact-undefined-numberp-lemma-in!ductive-step}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{fact-cost}}\,($-$ {\it{x\/}})\index{fact-cost} \\ 
$\wedge$$\;\;\;\;$({\rm{fact-cost}}\,($-$ ($1\;+$ {\it{x\/}}))\index{fact-cost} $\rightarrow$ (({\it{n\/}} $-\;1$) $\leq$ {\rm{fact-cost}}\,($-$ ($1\;+$ {\it{x\/}}))\index{fact-cost})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{fact-cost}}\,($-$ {\it{x\/}})\index{fact-cost} $<$ {\it{n\/}}) $=$ {\bf{f}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fact-undefined-negativep-lemma \\ \index{fact-undefined-negativep-lemma}
{\rm{fact-cost}}\,($-$ {\it{x\/}})\index{fact-cost} $\rightarrow$ (({\rm{fact-cost}}\,($-$ {\it{x\/}})\index{fact-cost} $<$ {\it{n\/}}) $=$ {\bf{f}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fact-undefined-negativep \\ \index{fact-undefined-negativep}
{\rm{negativep}}\,({\it{z\/}}) $\rightarrow$ ({\rm{fact-cost}}\,({\it{z\/}})\index{fact-cost} $=$ {\bf{f}})
\end{tabbing}

\begin{verbatim};; finally, we put this all together

\end{verbatim}\begin{tabbing}{\sc Theorem}:  fact-domain \\ \index{fact-domain}
{\rm{fact-cost}}\,({\it{x\/}})\index{fact-cost} $\leftrightarrow$ ($\neg$ {\rm{negativep}}\,({\it{x\/}}))
\end{tabbing}

\begin{verbatim};; Example 3:  triple reverse

;; First, ordinary reverse, and proper list recognizer

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{rev} \\  
\=\+{\rm{rev}}\,({\it{x\/}})\index{rev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{append}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev}, {\rm{list}}\,({\rm{car}}\,({\it{x\/}}))) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{plistp} \\  
\=\+{\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{plistp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{plistp} \\ 
{\bf else }{\it{x\/}} $=$ {\bf{nil}}$\;${\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{verbatim};; dcls, add-axioms, and rewrite rules for rev3-cost and rev (6 events)

\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it rev3-cost\index{rev3-cost}\/} of one argument.

\addvspace{18pt}


\noindent{\sc Event}:   Introduce the function symbol {\it rev3\index{rev3}\/} of one argument.

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  rev3-defn \\ \index{rev3-defn}
\=\+{\rm{rev3}}\,({\it{x\/}})\index{rev3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}), \\ 
{\rm{rev3}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{rev3}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3}))\index{rev3})\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{rev3}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Axiom}:  rev3-cost-defn \\ \index{rev3-cost-defn}
\=\+{\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }{\rm{s-plus}}\,(\=\+{\tt{1}}, \\ 
{\rm{s-plus}}\,(\=\+{\rm{rev3-cost}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3-cost}, \\ 
{\rm{s-plus}}\,(\=\+{\rm{rev3-cost}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3-cost}, \\ 
{\rm{rev3-cost}}\,({\rm{cons}}\,(\=\+{\rm{car}}\,({\it{x\/}}), \\ 
{\rm{rev3}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3})\-)\index{rev3-cost})\-\index{s-plus})\-\index{s-plus})\-\index{s-plus} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev3-cost-opener \\ \index{rev3-cost-opener}
\=\+(\=\+{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} \\ 
$=$$\;\;\;\;${\rm{s-plus}}\,(\=\+{\tt{1}}, \\ 
{\rm{s-plus}}\,(\=\+{\rm{rev3-cost}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3-cost}, \\ 
{\rm{s-plus}}\,(\=\+{\rm{rev3-cost}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3-cost}, \\ 
{\rm{rev3-cost}}\,({\rm{cons}}\,(\=\+{\rm{car}}\,({\it{x\/}}), \\ 
{\rm{rev3}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3})\-)\index{rev3-cost})\-\index{s-plus})\-\index{s-plus})\-\index{s-plus})\-)\- \\ 
$\wedge$$\;\;\;\;$(({\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} $=$ {\tt{1}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev3-defn-opener \\ \index{rev3-defn-opener}
\=\+(\=\+{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rev3}}\,({\it{x\/}})\index{rev3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}), \\ 
{\rm{rev3}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{rev3}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3}))\index{rev3})\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{apply}}\,({\tt{'}}{\tt{rev3}}, {\rm{list}}\,({\it{x\/}}))\index{apply}$\;${\bf  endif}\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(({\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{rev3}}\,({\it{x\/}})\index{rev3} $=$ {\it{x\/}}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{rev3-induction} \\  
\=\+{\rm{rev3-induction}}\,({\it{x\/}}, {\it{n\/}})\index{rev3-induction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }({\it{n\/}} $\simeq {\tt{0}}$) $\vee$ (({\it{n\/}} $-\;1$) $\simeq {\tt{0}}$)$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }\=\+{\rm{rev3-induction}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{n\/}} $-\;1$)\index{rev3-induction} \\ 
$\wedge$$\;\;\;\;${\rm{rev3-induction}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}), ({\it{n\/}} $-\;1$) $-\;1$)\index{rev3-induction} \\ 
$\wedge$$\;\;\;\;${\rm{rev3-induction}}\,(\=\+{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{rev3}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev3}))\index{rev3}), \\ 
{\it{n\/}} $-\;1$)\-\index{rev3-induction}\-$\;${\bf  endif}\-\-
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  rev3-length-and-definedness-lemma \\ \index{rev3-length-and-definedness-lem!ma}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{n\/}}) $\rightarrow$ ({\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost} $\wedge$ ({\rm{length}}\,({\rm{rev3}}\,({\it{x\/}})\index{rev3})\index{length} $=$ {\it{n\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev3-defined \\ \index{rev3-defined}
{\rm{rev3-cost}}\,({\it{x\/}})\index{rev3-cost}
\end{tabbing}

\begin{verbatim};; Now, just for fun, we'll show in the rest of these "rev" events
;; that rev3 is rev.  Note that we've already shown that rev3 is
;; "total" in the event just above.

\end{verbatim}
\noindent{\sc Event}:   Disable rev3-cost-opener.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  app-assoc \\ \index{app-assoc}
{\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 Theorem}:  rev-rev \\ \index{rev-rev}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{rev}}\,({\rm{rev}}\,({\it{x\/}})\index{rev})\index{rev} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  plistp-rev \\ \index{plistp-rev}
{\rm{plistp}}\,({\rm{rev}}\,({\it{x\/}})\index{rev})\index{plistp}
\end{tabbing}

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

\begin{tabbing}{\sc Theorem}:  plistp-cdr \\ \index{plistp-cdr}
({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ {\rm{listp}}\,({\it{x\/}})) $\rightarrow$ {\rm{plistp}}\,({\rm{cdr}}\,({\it{x\/}}))\index{plistp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  listp-append \\ \index{listp-append}
{\rm{listp}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}})) $=$ ({\rm{listp}}\,({\it{x\/}}) $\vee$ {\rm{listp}}\,({\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev-prop \\ \index{rev-prop}
\=\+{\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rev}}\,({\it{x\/}})\index{rev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev}), \\ 
{\rm{rev}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{rev}}\,({\rm{cdr}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev}))\index{rev}))\index{rev})\- \\ 
{\bf else }{\it{x\/}}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev-prop-rewrite \\ \index{rev-prop-rewrite}
\=\+{\rm{plistp}}\,({\it{x\/}})\index{plistp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{listp}}\,({\rm{cdr}}\,({\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{rev}}\,({\it{x\/}})\index{rev} \\ 
$=$$\;\;\;\;${\rm{cons}}\,(\=\+{\rm{car}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev}), \\ 
{\rm{rev}}\,({\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\rm{rev}}\,({\rm{cdr}}\,({\rm{rev}}\,({\rm{cdr}}\,({\it{x\/}}))\index{rev}))\index{rev}))\index{rev})\-)\-)\- \\ 
$\wedge$$\;\;\;\;$(({\rm{cdr}}\,({\it{x\/}}) $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{rev}}\,({\it{x\/}})\index{rev} $=$ {\it{x\/}})))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable rev.

\addvspace{18pt}

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

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

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

\begin{tabbing}{\sc Theorem}:  length-cdr-rev3 \\ \index{length-cdr-rev3}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{length}}\,({\rm{cdr}}\,({\rm{rev3}}\,({\it{x\/}})\index{rev3}))\index{length} $=$ ({\rm{length}}\,({\it{x\/}})\index{length} $-\;1$))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev3-rev-lemma \\ \index{rev3-rev-lemma}
({\rm{plistp}}\,({\it{x\/}})\index{plistp} $\wedge$ ({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\it{n\/}})) $\rightarrow$ ({\rm{rev3}}\,({\it{x\/}})\index{rev3} $=$ {\rm{rev}}\,({\it{x\/}})\index{rev})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  rev3-rev \\ \index{rev3-rev}
{\rm{plistp}}\,({\it{x\/}})\index{plistp} $\rightarrow$ ({\rm{rev3}}\,({\it{x\/}})\index{rev3} $=$ {\rm{rev}}\,({\it{x\/}})\index{rev})
\end{tabbing}
%\end{list}
\printindex
\end{document}
