\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 Matt Kaufmann, Damir Jamsek, and 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

 Matt Kaufmann, Damir Jamsek, and Computational Logic, Inc. 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 Matt Kaufmann, Damir Jamsek, or 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.''

|#

;; An exercise in reverse Polish notation evaluation suggested
;; by Damir Jamsek.

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

\addvspace{18pt}

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

\begin{tabbing}{\sc Definition}:\index{op1}$\;\;$
{\sc{op1}}\index{op1} $=$ {\tt{'}}{\tt{(}}{\tt{suc}}{\tt{)}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{op2}$\;\;$
{\sc{op2}}\index{op2} $=$ {\tt{'}}{\tt{(}}{\tt{add}}{\tt{ }}{\tt{mul}}{\tt{ }}{\tt{div}}{\tt{ }}{\tt{mod}}{\tt{)}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{op1-form-p} \\  
\=\+{\rm{op1-form-p}}\,({\it{e\/}})\index{op1-form-p} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{e\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cdr}}\,({\it{e\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\it{e\/}}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{e\/}}) $\in$ {\sc{op1}}\index{op1}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{op2-form-p} \\  
\=\+{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{e\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cdr}}\,({\it{e\/}})) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\rm{cddr}}\,({\it{e\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{cdddr}}\,({\it{e\/}}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{e\/}}) $\in$ {\sc{op2}}\index{op2}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{exp-p} \\  
\=\+{\rm{exp-p}}\,({\it{e\/}})\index{exp-p} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{op1-form-p}}\,({\it{e\/}})\index{op1-form-p}$\;\;${\bf then }{\rm{exp-p}}\,({\rm{cadr}}\,({\it{e\/}}))\index{exp-p} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p}$\;\;${\bf then }{\rm{exp-p}}\,({\rm{cadr}}\,({\it{e\/}}))\index{exp-p} $\wedge$ {\rm{exp-p}}\,({\rm{caddr}}\,({\it{e\/}}))\index{exp-p} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{eval-exp} \\  
\=\+{\rm{eval-exp}}\,({\it{e\/}})\index{eval-exp} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\it{e\/}} \\ 
{\bf elseif }{\rm{op1-form-p}}\,({\it{e\/}})\index{op1-form-p} $\wedge$ ({\rm{car}}\,({\it{e\/}}) $=$ {\tt{'}}{\tt{suc}}) \\ 
{\bf then }$1\;+$ {\rm{eval-exp}}\,({\rm{cadr}}\,({\it{e\/}}))\index{eval-exp} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} $\wedge$ ({\rm{car}}\,({\it{e\/}}) $=$ {\tt{'}}{\tt{add}}) \\ 
{\bf then }{\rm{eval-exp}}\,({\rm{cadr}}\,({\it{e\/}}))\index{eval-exp} $+$ {\rm{eval-exp}}\,({\rm{caddr}}\,({\it{e\/}}))\index{eval-exp} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} $\wedge$ ({\rm{car}}\,({\it{e\/}}) $=$ {\tt{'}}{\tt{mul}}) \\ 
{\bf then }{\rm{eval-exp}}\,({\rm{cadr}}\,({\it{e\/}}))\index{eval-exp} $*$ {\rm{eval-exp}}\,({\rm{caddr}}\,({\it{e\/}}))\index{eval-exp} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} $\wedge$ ({\rm{car}}\,({\it{e\/}}) $=$ {\tt{'}}{\tt{div}}) \\ 
{\bf then }{\rm{eval-exp}}\,({\rm{cadr}}\,({\it{e\/}}))\index{eval-exp} $\div$ {\rm{eval-exp}}\,({\rm{caddr}}\,({\it{e\/}}))\index{eval-exp} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} $\wedge$ ({\rm{car}}\,({\it{e\/}}) $=$ {\tt{'}}{\tt{mod}}) \\ 
{\bf then }{\rm{eval-exp}}\,({\rm{cadr}}\,({\it{e\/}}))\index{eval-exp} ${}${\bf{mod}}${}$ {\rm{eval-exp}}\,({\rm{caddr}}\,({\it{e\/}}))\index{eval-exp} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{exp-to-rpn} \\  
\=\+{\rm{exp-to-rpn}}\,({\it{e\/}})\index{exp-to-rpn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\rm{list}}\,({\it{e\/}}) \\ 
{\bf elseif }{\rm{op1-form-p}}\,({\it{e\/}})\index{op1-form-p}$\;\;${\bf then }{\rm{append}}\,({\rm{exp-to-rpn}}\,({\rm{cadr}}\,({\it{e\/}}))\index{exp-to-rpn}, {\rm{list}}\,({\rm{car}}\,({\it{e\/}}))) \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} \\ 
{\bf then }{\rm{append}}\,(\=\+{\rm{exp-to-rpn}}\,({\rm{caddr}}\,({\it{e\/}}))\index{exp-to-rpn}, \\ 
{\rm{append}}\,({\rm{exp-to-rpn}}\,({\rm{cadr}}\,({\it{e\/}}))\index{exp-to-rpn}, {\rm{list}}\,({\rm{car}}\,({\it{e\/}}))))\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{eval-rpn} \\  
\=\+{\rm{eval-rpn}}\,({\it{r\/}}, {\it{s\/}})\index{eval-rpn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{r\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{r\/}}) $\in\;${\bf{N}}${}$$\;\;${\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{r\/}}), {\it{s\/}}))\index{eval-rpn} \\ 
{\bf elseif }{\rm{car}}\,({\it{r\/}}) $=$ {\tt{'}}{\tt{suc}} \\ 
{\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,($1\;+$ {\rm{car}}\,({\it{s\/}}), {\rm{cdr}}\,({\it{s\/}})))\index{eval-rpn} \\ 
{\bf elseif }{\rm{car}}\,({\it{r\/}}) $=$ {\tt{'}}{\tt{add}} \\ 
{\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{s\/}}) $+$ {\rm{cadr}}\,({\it{s\/}}), {\rm{cddr}}\,({\it{s\/}})))\index{eval-rpn} \\ 
{\bf elseif }{\rm{car}}\,({\it{r\/}}) $=$ {\tt{'}}{\tt{mul}} \\ 
{\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{s\/}}) $*$ {\rm{cadr}}\,({\it{s\/}}), {\rm{cddr}}\,({\it{s\/}})))\index{eval-rpn} \\ 
{\bf elseif }{\rm{car}}\,({\it{r\/}}) $=$ {\tt{'}}{\tt{div}} \\ 
{\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{s\/}}) $\div$ {\rm{cadr}}\,({\it{s\/}}), {\rm{cddr}}\,({\it{s\/}})))\index{eval-rpn} \\ 
{\bf elseif }{\rm{car}}\,({\it{r\/}}) $=$ {\tt{'}}{\tt{mod}} \\ 
{\bf then }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{s\/}}) ${}${\bf{mod}}${}$ {\rm{cadr}}\,({\it{s\/}}), {\rm{cddr}}\,({\it{s\/}})))\index{eval-rpn} \\ 
{\bf else }{\rm{eval-rpn}}\,({\rm{cdr}}\,({\it{r\/}}), {\it{s\/}})\index{eval-rpn}$\;${\bf  endif}\- \\ 
{\bf else }{\it{s\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  eval-rpn-append \\ \index{eval-rpn-append}
{\rm{eval-rpn}}\,({\rm{append}}\,({\it{r1\/}}, {\it{r2\/}}), {\it{s\/}})\index{eval-rpn} $=$ {\rm{eval-rpn}}\,({\it{r2\/}}, {\rm{eval-rpn}}\,({\it{r1\/}}, {\it{s\/}})\index{eval-rpn})\index{eval-rpn}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{l1-ind} \\  
\=\+{\rm{l1-ind}}\,({\it{e\/}}, {\it{s\/}})\index{l1-ind} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{e\/}} $\in\;${\bf{N}}${}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{op1-form-p}}\,({\it{e\/}})\index{op1-form-p}$\;\;${\bf then }{\rm{l1-ind}}\,({\rm{cadr}}\,({\it{e\/}}), {\it{s\/}})\index{l1-ind} \\ 
{\bf elseif }{\rm{op2-form-p}}\,({\it{e\/}})\index{op2-form-p} \\ 
{\bf then }\=\+{\rm{l1-ind}}\,({\rm{caddr}}\,({\it{e\/}}), {\it{s\/}})\index{l1-ind} \\ 
$\wedge$$\;\;\;\;${\rm{l1-ind}}\,({\rm{cadr}}\,({\it{e\/}}), {\rm{cons}}\,({\rm{eval-exp}}\,({\rm{caddr}}\,({\it{e\/}}))\index{eval-exp}, {\it{s\/}}))\index{l1-ind}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  l1 \\ \index{l1}
{\rm{exp-p}}\,({\it{e\/}})\index{exp-p} $\rightarrow$ ({\rm{cons}}\,({\rm{eval-exp}}\,({\it{e\/}})\index{eval-exp}, {\it{s\/}}) $=$ {\rm{eval-rpn}}\,({\rm{exp-to-rpn}}\,({\it{e\/}})\index{exp-to-rpn}, {\it{s\/}})\index{eval-rpn})
\end{tabbing}

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