\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 library {\tt{"unsolv"}} using the compiled version.

\addvspace{18pt}

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

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{symbol}$\;\;$
{\rm{symbol}}\,({\it{x\/}})\index{symbol} $=$ ({\it{x\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{)}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{half-tape} \\  
\=\+{\rm{half-tape}}\,({\it{x\/}})\index{half-tape} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{x\/}} $=$ {\tt{0}} \\ 
{\bf else }{\rm{symbol}}\,({\rm{car}}\,({\it{x\/}}))\index{symbol} $\wedge$ {\rm{half-tape}}\,({\rm{cdr}}\,({\it{x\/}}))\index{half-tape}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tape} \\  
{\rm{tape}}\,({\it{x\/}})\index{tape} $=$ ({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{half-tape}}\,({\rm{car}}\,({\it{x\/}}))\index{half-tape} $\wedge$ {\rm{half-tape}}\,({\rm{cdr}}\,({\it{x\/}}))\index{half-tape})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{operation}$\;\;$
{\rm{operation}}\,({\it{x\/}})\index{operation} $=$ ({\it{x\/}} $\in$ {\tt{'}}{\tt{(}}{\tt{l}}{\tt{ }}{\tt{r}}{\tt{ }}{\tt{0}}{\tt{ }}{\tt{1}}{\tt{)}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{state}$\;\;$
{\rm{state}}\,({\it{x\/}})\index{state} $=$ {\rm{litatom}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{turing-4tuple} \\  
\=\+{\rm{turing-4tuple}}\,({\it{x\/}})\index{turing-4tuple} \\ 
$=$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{state}}\,({\rm{car}}\,({\it{x\/}}))\index{state} \\ 
$\wedge$$\;\;\;\;${\rm{symbol}}\,({\rm{cadr}}\,({\it{x\/}}))\index{symbol} \\ 
$\wedge$$\;\;\;\;${\rm{operation}}\,({\rm{caddr}}\,({\it{x\/}}))\index{operation} \\ 
$\wedge$$\;\;\;\;${\rm{state}}\,({\rm{cadddr}}\,({\it{x\/}}))\index{state} \\ 
$\wedge$$\;\;\;\;$({\rm{cddddr}}\,({\it{x\/}}) $=$ {\bf{nil}}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{turing-machine} \\  
\=\+{\rm{turing-machine}}\,({\it{x\/}})\index{turing-machine} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\it{x\/}} $=$ {\bf{nil}} \\ 
{\bf else }{\rm{turing-4tuple}}\,({\rm{car}}\,({\it{x\/}}))\index{turing-4tuple} $\wedge$ {\rm{turing-machine}}\,({\rm{cdr}}\,({\it{x\/}}))\index{turing-machine}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{instr} \\  
\=\+{\rm{instr}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}})\index{instr} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{tm\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{st\/}} $=$ {\rm{car}}\,({\rm{car}}\,({\it{tm\/}})) \\ 
{\bf then }\=\+{\bf if }{\it{sym\/}} $=$ {\rm{car}}\,({\rm{cdr}}\,({\rm{car}}\,({\it{tm\/}})))$\;\;${\bf then }{\rm{cdr}}\,({\rm{cdr}}\,({\rm{car}}\,({\it{tm\/}}))) \\ 
{\bf else }{\rm{instr}}\,({\it{st\/}}, {\it{sym\/}}, {\rm{cdr}}\,({\it{tm\/}}))\index{instr}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{instr}}\,({\it{st\/}}, {\it{sym\/}}, {\rm{cdr}}\,({\it{tm\/}}))\index{instr}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{new-tape} \\  
\=\+{\rm{new-tape}}\,({\it{op\/}}, {\it{tape\/}})\index{new-tape} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{op\/}} $=$ {\tt{'}}{\tt{l}} \\ 
{\bf then }{\rm{cons}}\,({\rm{cdr}}\,({\rm{car}}\,({\it{tape\/}})), {\rm{cons}}\,({\rm{car}}\,({\rm{car}}\,({\it{tape\/}})), {\rm{cdr}}\,({\it{tape\/}}))) \\ 
{\bf elseif }{\it{op\/}} $=$ {\tt{'}}{\tt{r}} \\ 
{\bf then }{\rm{cons}}\,({\rm{cons}}\,({\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\rm{car}}\,({\it{tape\/}})), {\rm{cdr}}\,({\rm{cdr}}\,({\it{tape\/}}))) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{tape\/}}), {\rm{cons}}\,({\it{op\/}}, {\rm{cdr}}\,({\rm{cdr}}\,({\it{tape\/}}))))$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi} \\  
\=\+{\rm{tmi}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmi} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{instr}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}})\index{instr} \\ 
{\bf then }{\rm{tmi}}\,(\=\+{\rm{car}}\,({\rm{cdr}}\,({\rm{instr}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}})\index{instr})), \\ 
{\rm{new-tape}}\,({\rm{car}}\,({\rm{instr}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}})\index{instr}), {\it{tape\/}})\index{new-tape}, \\ 
{\it{tm\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{tmi} \\ 
{\bf else }{\it{tape\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{instr-defn} \\  
\=\+{\sc{instr-defn}}\index{instr-defn} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{st}}{\tt{ }}{\tt{sym}}{\tt{ }}{\tt{tm}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{listp}}{\tt{ }}{\tt{tm}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{sym}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{instr}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{sym}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{instr}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{sym}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{f}}{\tt{)}}\-{\tt{)}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{new-tape-defn} \\  
\=\+{\sc{new-tape-defn}}\index{new-tape-defn} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{op}}{\tt{ }}{\tt{tape}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{op}}{\tt{ }}{\tt{'}}{\tt{l}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{cons}} \\ 
{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{equal}}{\tt{ }}{\tt{op}}{\tt{ }}{\tt{'}}{\tt{r}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{cons}} \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{)}}\- \\ 
{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{cons}}{\tt{ }}{\tt{op}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi-defn} \\  
\=\+{\sc{tmi-defn}}\index{tmi-defn} \\ 
$=$$\;\;\;\;${\tt{'}}{\tt{(}}\=\+{\tt{(}}{\tt{st}}{\tt{ }}{\tt{tape}}{\tt{ }}{\tt{tm}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{instr}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{tm}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{tmi}} \\ 
{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{(}}{\tt{instr}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}}{\tt{)}} \\ 
{\tt{(}}\=\+{\tt{new-tape}} \\ 
{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{instr}}{\tt{ }}{\tt{st}}{\tt{ }}{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{tm}}{\tt{)}}{\tt{)}} \\ 
{\tt{tape}}{\tt{)}}\- \\ 
{\tt{tm}}{\tt{)}}\- \\ 
{\tt{tape}}{\tt{)}}\-{\tt{)}}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{kwote}$\;\;$
{\rm{kwote}}\,({\it{x\/}})\index{kwote} $=$ {\rm{list}}\,({\tt{'}}{\tt{quote}}, {\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi-fa} \\  
\=\+{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa} \\ 
$=$$\;\;\;\;${\rm{list}}\,(\=\+{\rm{list}}\,({\tt{'}}{\tt{tm}}, {\bf{nil}}, {\rm{kwote}}\,({\it{tm\/}})\index{kwote}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{instr}}, {\sc{instr-defn}}\index{instr-defn}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{new-tape}}, {\sc{new-tape-defn}}\index{new-tape-defn}), \\ 
{\rm{cons}}\,({\tt{'}}{\tt{tmi}}, {\sc{tmi-defn}}\index{tmi-defn}))\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi-x} \\  
{\rm{tmi-x}}\,({\it{st\/}}, {\it{tape\/}})\index{tmi-x} $=$ {\rm{list}}\,({\tt{'}}{\tt{tmi}}, {\rm{kwote}}\,({\it{st\/}})\index{kwote}, {\rm{kwote}}\,({\it{tape\/}})\index{kwote}, {\tt{'}}{\tt{(}}{\tt{tm}}{\tt{)}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{x\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{x\/}}))\index{length}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi-k}$\;\;$
{\rm{tmi-k}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmi-k} $=$ ({\it{n\/}} $-$ ($1\;+$ {\rm{length}}\,({\it{tm\/}})\index{length}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{tmi-n}$\;\;$
{\rm{tmi-n}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}})\index{tmi-n} $=$ ({\it{k\/}} $+$ ($1\;+$ {\rm{length}}\,({\it{tm\/}})\index{length}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  length-0 \\ \index{length-0}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{0}}) $=$ ({\it{x\/}} $\simeq\;${{\bf{nil}}}${}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-equal-0 \\ \index{plus-equal-0}
(({\it{i\/}} $+$ {\it{j\/}}) $=$ {\tt{0}}) $=$ (({\it{i\/}} $\simeq {\tt{0}}$) $\wedge$ ({\it{j\/}} $\simeq {\tt{0}}$))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-difference \\ \index{plus-difference}
\=\+(({\it{i\/}} $-$ {\it{j\/}}) $+$ {\it{j\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\leq$ {\it{j\/}}$\;\;${\bf then }{\rm{fix}}\,({\it{j\/}}) \\ 
{\bf else }{\it{i\/}}$\;${\bf  endif}\-\-
\end{tabbing}

\noindent{\sc Event}:   Enable difference; name this event `difference-off'.\index{difference-off}

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  pr-eval-fn-0 \\ \index{pr-eval-fn-0}
\=\+(\=\+({\it{n\/}} $\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) \\ 
$\wedge$$\;\;\;\;$({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{unsolv-subrp}}\,({\it{fn\/}})\index{unsolv-subrp}) \\ 
$\wedge$$\;\;\;\;$({\it{vargs\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} $=$ {\sc{btm}}\index{btm})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-fn-1 \\ \index{pr-eval-fn-1}
\=\+(\=\+({\it{n\/}} $\not\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;$({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) \\ 
$\wedge$$\;\;\;\;$({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{unsolv-subrp}}\,({\it{fn\/}})\index{unsolv-subrp}) \\ 
$\wedge$$\;\;\;\;$({\it{vargs\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{btmp}}\,({\it{vargs\/}})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{btmp}}\,({\rm{get}}\,({\it{fn\/}}, {\it{fa\/}})\index{get})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf else }{\rm{ev}}\,(\=\+{\tt{'}}{\tt{al}}, \\ 
{\rm{cadr}}\,({\rm{get}}\,({\it{fn\/}}, {\it{fa\/}})\index{get}), \\ 
{\rm{pairlist}}\,({\rm{car}}\,({\rm{get}}\,({\it{fn\/}}, {\it{fa\/}})\index{get}), {\it{vargs\/}}), \\ 
{\it{fa\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{ev}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-unsolv-subrp \\ \index{pr-eval-unsolv-subrp}
\=\+({\rm{unsolv-subrp}}\,({\it{fn\/}})\index{unsolv-subrp} $\wedge$ ({\it{vargs\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{btmp}}\,({\it{vargs\/}})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf else }{\rm{unsolv-apply-subr}}\,({\it{fn\/}}, {\it{vargs\/}})\index{unsolv-apply-subr}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-if \\ \index{pr-eval-if}
\=\+({\it{vx1\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{x1\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{list}}\,({\tt{'}}{\tt{if}}, {\it{x1\/}}, {\it{x2\/}}, {\it{x3\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{btmp}}\,({\it{vx1\/}})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\it{vx1\/}}$\;\;${\bf then }{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{x2\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
{\bf else }{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{x3\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-quote \\ \index{pr-eval-quote}
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{list}}\,({\tt{'}}{\tt{quote}}, {\it{x\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} $=$ {\it{x\/}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-nlistp \\ \index{pr-eval-nlistp}
\=\+({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\tt{0}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} $=$ {\tt{0}}) \\ 
$\wedge$$\;\;\;\;$({\rm{ev}}\,({\tt{'}}{\tt{al}}, $1\;+$ {\it{n\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} $=$ ($1\;+$ {\it{n\/}})) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{pack}}\,({\it{x\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{pack}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{t}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{pack}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{f}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{pack}}\,({\it{x\/}}) $=$ {\tt{'}}{\tt{nil}}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{get}}\,({\rm{pack}}\,({\it{x\/}}), {\it{va\/}})\index{get}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  evlist-nil \\ \index{evlist-nil}
{\rm{ev}}\,({\tt{'}}{\tt{list}}, {\bf{nil}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} $=$ {\bf{nil}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  evlist-cons \\ \index{evlist-cons}
\=\+(({\it{vx\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{x\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev}) $\wedge$ ({\it{vl\/}} $=$ {\rm{ev}}\,({\tt{'}}{\tt{list}}, {\it{l\/}}, {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{list}}, {\rm{cons}}\,({\it{x\/}}, {\it{l\/}}), {\it{va\/}}, {\it{fa\/}}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{btmp}}\,({\it{vx\/}})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{btmp}}\,({\it{vl\/}})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf else }{\rm{cons}}\,({\it{vx\/}}, {\it{vl\/}})$\;${\bf  endif}\-)\-\-
\end{tabbing}

\noindent{\sc Event}:   Enable unsolv-subrp; name this event `unsolv-subrp-off'.\index{unsolv-subrp-off}

\addvspace{18pt}

\noindent{\sc Event}:   Enable ev; name this event `ev-off'.\index{ev-off}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{cnb} \\  
\=\+{\rm{cnb}}\,({\it{x\/}})\index{cnb} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }{\rm{cnb}}\,({\rm{car}}\,({\it{x\/}}))\index{cnb} $\wedge$ {\rm{cnb}}\,({\rm{cdr}}\,({\it{x\/}}))\index{cnb} \\ 
{\bf else }$\neg$ {\rm{btmp}}\,({\it{x\/}})\index{btmp}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-nbtm \\ \index{cnb-nbtm}
{\rm{cnb}}\,({\it{x\/}})\index{cnb} $\rightarrow$ ({\rm{btmp}}\,({\it{x\/}})\index{btmp} $=$ {\bf{f}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-cons \\ \index{cnb-cons}
\=\+({\rm{cnb}}\,({\rm{cons}}\,({\it{a\/}}, {\it{b\/}}))\index{cnb} $=$ ({\rm{cnb}}\,({\it{a\/}})\index{cnb} $\wedge$ {\rm{cnb}}\,({\it{b\/}})\index{cnb})) \\ 
$\wedge$$\;\;\;\;$({\rm{cnb}}\,({\it{x\/}})\index{cnb} $\rightarrow$ {\rm{cnb}}\,({\rm{car}}\,({\it{x\/}}))\index{cnb}) \\ 
$\wedge$$\;\;\;\;$({\rm{cnb}}\,({\it{x\/}})\index{cnb} $\rightarrow$ {\rm{cnb}}\,({\rm{cdr}}\,({\it{x\/}}))\index{cnb})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-litatom \\ \index{cnb-litatom}
{\rm{litatom}}\,({\it{x\/}}) $\rightarrow$ {\rm{cnb}}\,({\it{x\/}})\index{cnb}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-numberp \\ \index{cnb-numberp}
({\it{x\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ {\rm{cnb}}\,({\it{x\/}})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable cnb; name this event `cnb-off'.\index{cnb-off}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  get-tmi-fa \\ \index{get-tmi-fa}
\=\+({\rm{get}}\,({\tt{'}}{\tt{tm}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa})\index{get} $=$ {\rm{list}}\,({\bf{nil}}, {\rm{kwote}}\,({\it{tm\/}})\index{kwote})) \\ 
$\wedge$$\;\;\;\;$({\rm{get}}\,({\tt{'}}{\tt{instr}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa})\index{get} $=$ {\sc{instr-defn}}\index{instr-defn}) \\ 
$\wedge$$\;\;\;\;$({\rm{get}}\,({\tt{'}}{\tt{new-tape}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa})\index{get} $=$ {\sc{new-tape-defn}}\index{new-tape-defn}) \\ 
$\wedge$$\;\;\;\;$({\rm{get}}\,({\tt{'}}{\tt{tmi}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa})\index{get} $=$ {\sc{tmi-defn}}\index{tmi-defn})\-
\end{tabbing}

\noindent{\sc Event}:   Enable tmi-fa; name this event `tmi-fa-off'.\index{tmi-fa-off}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{instrn} \\  
\=\+{\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}}, {\it{n\/}})\index{instrn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{listp}}\,({\it{tm\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{st\/}} $=$ {\rm{car}}\,({\rm{car}}\,({\it{tm\/}})) \\ 
{\bf then }\=\+{\bf if }{\it{sym\/}} $=$ {\rm{car}}\,({\rm{cdr}}\,({\rm{car}}\,({\it{tm\/}})))$\;\;${\bf then }{\rm{cdr}}\,({\rm{cdr}}\,({\rm{car}}\,({\it{tm\/}}))) \\ 
{\bf else }{\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\rm{cdr}}\,({\it{tm\/}}), {\it{n\/}} $-\;1$)\index{instrn}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\rm{cdr}}\,({\it{tm\/}}), {\it{n\/}} $-\;1$)\index{instrn}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pr-eval-instr-induction-scheme} \\  
\=\+{\rm{pr-eval-instr-induction-scheme}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm--\/}}, {\it{va\/}}, {\it{tm\/}}, {\it{n\/}})\index{pr-eval-instr-induction-scheme} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{pr-eval-instr-induction-scheme}}\,(\=\+{\tt{'}}{\tt{st}}, \\ 
{\tt{'}}{\tt{sym}}, \\ 
{\tt{'}}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tm}}{\tt{)}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{st}}, \\ 
{\rm{pr-eval}}\,(\=\+{\it{st\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{pr-eval})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{sym}}, \\ 
{\rm{pr-eval}}\,(\=\+{\it{sym\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{pr-eval})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{tm}}, \\ 
{\rm{pr-eval}}\,(\=\+{\it{tm--\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{pr-eval})\-)\-, \\ 
{\it{tm\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{pr-eval-instr-induction-scheme}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-instr \\ \index{pr-eval-instr}
\=\+(\=\+{\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{st\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb} \\ 
$\wedge$$\;\;\;\;${\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{sym\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb} \\ 
$\wedge$$\;\;\;\;${\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tm--\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{list}}\,({\tt{'}}{\tt{instr}}, {\it{st\/}}, {\it{sym\/}}, {\it{tm--\/}}), {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;${\rm{instrn}}\,(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{st\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{sym\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tm--\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\it{n\/}})\-\index{instrn})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-new-tape \\ \index{pr-eval-new-tape}
\=\+({\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{op\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb} $\wedge$ {\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tape\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{list}}\,({\tt{'}}{\tt{new-tape}}, {\it{op\/}}, {\it{tape\/}}), {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf else }{\rm{new-tape}}\,(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{op\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tape\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\-\index{new-tape}$\;${\bf  endif}\-)\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-instrn \\ \index{cnb-instrn}
(($\neg$ {\rm{btmp}}\,({\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}}, {\it{n\/}})\index{instrn})\index{btmp}) $\wedge$ {\rm{cnb}}\,({\it{tm\/}})\index{cnb}) $\rightarrow$ {\rm{cnb}}\,({\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}}, {\it{n\/}})\index{instrn})\index{cnb}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  cnb-new-tape \\ \index{cnb-new-tape}
({\rm{cnb}}\,({\it{op\/}})\index{cnb} $\wedge$ {\rm{cnb}}\,({\it{tape\/}})\index{cnb}) $\rightarrow$ {\rm{cnb}}\,({\rm{new-tape}}\,({\it{op\/}}, {\it{tape\/}})\index{new-tape})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable new-tape; name this event `new-tape-off'.\index{new-tape-off}

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{tmin} \\  
\=\+{\rm{tmin}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmin} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{btmp}}\,({\rm{instrn}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}}, {\it{n\/}} $-\;1$)\index{instrn})\index{btmp}$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf elseif }{\rm{instrn}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}}, {\it{n\/}} $-\;1$)\index{instrn} \\ 
{\bf then }{\rm{tmin}}\,(\=\+{\rm{car}}\,({\rm{cdr}}\,({\rm{instrn}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}}, {\it{n\/}} $-\;1$)\index{instrn})), \\ 
{\rm{new-tape}}\,({\rm{car}}\,({\rm{instrn}}\,({\it{st\/}}, {\rm{car}}\,({\rm{cdr}}\,({\it{tape\/}})), {\it{tm\/}}, {\it{n\/}} $-\;1$)\index{instrn}), {\it{tape\/}})\index{new-tape}, \\ 
{\it{tm\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{tmin} \\ 
{\bf else }{\it{tape\/}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{pr-eval-tmi-induction-scheme} \\  
\=\+{\rm{pr-eval-tmi-induction-scheme}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm--\/}}, {\it{va\/}}, {\it{tm\/}}, {\it{n\/}})\index{pr-eval-tmi-induction-scheme} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{pr-eval-tmi-induction-scheme}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{car}} \\ 
{\tt{(}}\=\+{\tt{cdr}} \\ 
{\tt{(}}\=\+{\tt{instr}}{\tt{ }}{\tt{st}} \\ 
{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}} \\ 
{\tt{tm}}{\tt{)}}\-{\tt{)}}\-{\tt{)}}\-, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{new-tape}} \\ 
{\tt{(}}\=\+{\tt{car}} \\ 
{\tt{(}}\=\+{\tt{instr}}{\tt{ }}{\tt{st}} \\ 
{\tt{(}}{\tt{car}}{\tt{ }}{\tt{(}}{\tt{cdr}}{\tt{ }}{\tt{tape}}{\tt{)}}{\tt{)}} \\ 
{\tt{tm}}{\tt{)}}\-{\tt{)}}\- \\ 
{\tt{tape}}{\tt{)}}\-, \\ 
{\tt{'}}{\tt{tm}}, \\ 
{\rm{list}}\,(\=\+{\rm{cons}}\,(\=\+{\tt{'}}{\tt{st}}, \\ 
{\rm{ev}}\,(\=\+{\tt{'}}{\tt{al}}, \\ 
{\it{st\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{ev})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{tape}}, \\ 
{\rm{ev}}\,(\=\+{\tt{'}}{\tt{al}}, \\ 
{\it{tape\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{ev})\-, \\ 
{\rm{cons}}\,(\=\+{\tt{'}}{\tt{tm}}, \\ 
{\rm{ev}}\,(\=\+{\tt{'}}{\tt{al}}, \\ 
{\it{tm--\/}}, \\ 
{\it{va\/}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\it{n\/}})\-\index{ev})\-)\-, \\ 
{\it{tm\/}}, \\ 
{\it{n\/}} $-\;1$)\-\index{pr-eval-tmi-induction-scheme}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-tmi \\ \index{pr-eval-tmi}
\=\+(\=\+{\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{st\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb} \\ 
$\wedge$$\;\;\;\;${\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tape\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb} \\ 
$\wedge$$\;\;\;\;${\rm{cnb}}\,({\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tm--\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev})\index{cnb})\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{list}}\,({\tt{'}}{\tt{tmi}}, {\it{st\/}}, {\it{tape\/}}, {\it{tm--\/}}), {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;${\rm{tmin}}\,(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{st\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tape\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\it{tm--\/}}, {\it{va\/}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev}, \\ 
{\it{n\/}})\-\index{tmin})\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  pr-eval-tmi-x \\ \index{pr-eval-tmi-x}
\=\+({\rm{cnb}}\,({\it{st\/}})\index{cnb} $\wedge$ {\rm{cnb}}\,({\it{tape\/}})\index{cnb} $\wedge$ {\rm{cnb}}\,({\it{tm\/}})\index{cnb}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{ev}}\,({\tt{'}}{\tt{al}}, {\rm{tmi-x}}\,({\it{st\/}}, {\it{tape\/}})\index{tmi-x}, {\bf{nil}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{ev} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\sc{btm}}\index{btm} \\ 
{\bf else }{\rm{tmin}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmin}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\noindent{\sc Event}:   Enable tmi-x; name this event `tmi-x-off'.\index{tmi-x-off}

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  instrn-instr \\ \index{instrn-instr}
({\rm{length}}\,({\it{tm\/}})\index{length} $<$ {\it{n\/}}) $\rightarrow$ ({\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}}, {\it{n\/}})\index{instrn} $=$ {\rm{instr}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}})\index{instr})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  nbtmp-instr \\ \index{nbtmp-instr}
{\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine} $\rightarrow$ ($\neg$ {\rm{btmp}}\,({\rm{instr}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}})\index{instr})\index{btmp})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  instrn-non-f \\ \index{instrn-non-f}
({\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{tm\/}})\index{length})) $\rightarrow$ {\rm{instrn}}\,({\it{st\/}}, {\it{sym\/}}, {\it{tm\/}}, {\it{n\/}})\index{instrn}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tmin-btm \\ \index{tmin-btm}
\=\+({\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine} $\wedge$ ({\it{n\/}} $\leq$ {\rm{length}}\,({\it{tm\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{tmin}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmin} $=$ {\sc{btm}}\index{btm})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tmin-tmi \\ \index{tmin-tmi}
\=\+{\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine} \\ 
$\rightarrow$$\;\;\;\;$({\rm{tmi}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}})\index{tmi} $=$ {\rm{tmin}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}} $+$ ($1\;+$ {\rm{length}}\,({\it{tm\/}})\index{length}))\index{tmin})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  symbol-cnb \\ \index{symbol-cnb}
{\rm{symbol}}\,({\it{sym\/}})\index{symbol} $\rightarrow$ {\rm{cnb}}\,({\it{sym\/}})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable symbol; name this event `symbol-off'.\index{symbol-off}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  half-tape-cnb \\ \index{half-tape-cnb}
{\rm{half-tape}}\,({\it{x\/}})\index{half-tape} $\rightarrow$ {\rm{cnb}}\,({\it{x\/}})\index{cnb}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  tape-cnb \\ \index{tape-cnb}
{\rm{tape}}\,({\it{x\/}})\index{tape} $\rightarrow$ {\rm{cnb}}\,({\it{x\/}})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable tape; name this event `tape-off'.\index{tape-off}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  operation-cnb \\ \index{operation-cnb}
{\rm{operation}}\,({\it{op\/}})\index{operation} $\rightarrow$ {\rm{cnb}}\,({\it{op\/}})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable operation; name this event `operation-off'.\index{operation-off}

\addvspace{18pt}
\begin{tabbing}{\sc Theorem}:  turing-machine-cnb \\ \index{turing-machine-cnb}
{\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine} $\rightarrow$ {\rm{cnb}}\,({\it{tm\/}})\index{cnb}
\end{tabbing}

\noindent{\sc Event}:   Enable turing-machine; name this event `turing-machine-off'.\index{turing-machine-off}

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  turing-completeness-of-lisp \\ \index{turing-completeness-of-lisp}
\=\+({\rm{state}}\,({\it{st\/}})\index{state} $\wedge$ {\rm{tape}}\,({\it{tape\/}})\index{tape} $\wedge$ {\rm{turing-machine}}\,({\it{tm\/}})\index{turing-machine}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+($\neg$ {\rm{btmp}}\,({\rm{pr-eval}}\,({\rm{tmi-x}}\,({\it{st\/}}, {\it{tape\/}})\index{tmi-x}, {\bf{nil}}, {\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, {\it{n\/}})\index{pr-eval})\index{btmp}) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{btmp}}\,({\rm{tmi}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\rm{tmi-k}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{n\/}})\index{tmi-k})\index{tmi})\index{btmp}))\- \\ 
$\wedge$$\;\;\;\;$(\=\+($\neg$ {\rm{btmp}}\,({\rm{tmi}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}})\index{tmi})\index{btmp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{tmi}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}})\index{tmi} \\ 
$=$$\;\;\;\;${\rm{pr-eval}}\,(\=\+{\rm{tmi-x}}\,({\it{st\/}}, {\it{tape\/}})\index{tmi-x}, \\ 
{\bf{nil}}, \\ 
{\rm{tmi-fa}}\,({\it{tm\/}})\index{tmi-fa}, \\ 
{\rm{tmi-n}}\,({\it{st\/}}, {\it{tape\/}}, {\it{tm\/}}, {\it{k\/}})\index{tmi-n})\-\index{pr-eval})\-)\-)\-\-
\end{tabbing}
%\end{list}
\printindex
\end{document}
