\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) 1995 by Ken Kunen.  All Rights Reserved.

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

; NO WARRANTY

; Ken Kunen 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 Ken Kunen 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.



; This script is described in Section 4.2 of our paper,
; Non-Constructive Computational Mathematics.
; It includes three items

; ITEM 1: We show that induction on omega^2 is provable in PRA,
; even though there are non-primitive-recursive functions definable
; by recursion on omega^2
; ITEM 2: We use eval$ and v&c$, but not ordinal induction, and
; define the Ackermann function (and prove that the definition is correct).
; ITEM 3: We define a function (next-twin-prime x) and show that either there
; are no twin primes above x or next-twin-prime produces one.
; This is a simple demonstration of the non-constructiveness of eval$ and v&C$

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

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 1                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Represent ordinals below omega^2 as omega X omega, ordered lexically
; Elements of omega X omega are represented as pairs (m . n)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ordp} \\  
{\rm{ordp}}\,({\it{p\/}})\index{ordp} $=$ ({\rm{listp}}\,({\it{p\/}}) $\wedge$ ({\rm{car}}\,({\it{p\/}}) $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{cdr}}\,({\it{p\/}}) $\in\;${\bf{N}}${}$))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{lexp} \\  
\=\+{\rm{lexp}}\,({\it{p1\/}}, {\it{p2\/}})\index{lexp} \\ 
$=$$\;\;\;\;$(\=\+({\rm{car}}\,({\it{p1\/}}) $<$ {\rm{car}}\,({\it{p2\/}})) \\ 
$\vee$$\;\;\;\;$(({\rm{car}}\,({\it{p1\/}}) $=$ {\rm{car}}\,({\it{p2\/}})) $\wedge$ ({\rm{cdr}}\,({\it{p1\/}}) $<$ {\rm{cdr}}\,({\it{p2\/}}))))\-\-
\end{tabbing}

\begin{verbatim}; now let Q be any property of pairs:
\end{verbatim}
\noindent{\sc Event}:   Introduce the function symbol {\it q\index{q}\/} of one argument.

\addvspace{18pt}

\begin{verbatim}; Assume Q is inductive -- that is:
; NOT Q(p)  --> EXISTS r < p NOT Q(r)
; Of course, to say this in the framework of PRA, we have to assume
; we have a function which gives us an r

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

\addvspace{18pt}

\begin{tabbing}{\sc Axiom}:  q-induction \\ \index{q-induction}
\=\+({\rm{ordp}}\,({\it{p\/}})\index{ordp} $\wedge$ ($\neg$ {\rm{q}}\,({\it{p\/}})\index{q})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{ordp}}\,({\rm{g}}\,({\it{p\/}})\index{g})\index{ordp} $\wedge$ {\rm{lexp}}\,({\rm{g}}\,({\it{p\/}})\index{g}, {\it{p\/}})\index{lexp} $\wedge$ ($\neg$ {\rm{q}}\,({\rm{g}}\,({\it{p\/}})\index{g})\index{q}))\-
\end{tabbing}

\begin{verbatim}; Now,  we show Q is true everywhere :   (implies (ordp p) (Q p))
; by ordinary induction

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; First,  by ordinary induction on y (holding x fixed):
; Let fy = (fy x y) <= y be least such that (not (Q (x . fy)))
; fy = F if there is no such y

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fy} \\  
\=\+{\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\not\in\;${\bf{N}}${}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\it{y\/}} $=$ {\tt{0}} \\ 
{\bf then }\=\+{\bf if }{\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{fy}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{fy}$\;\;${\bf then }{\rm{fy}}\,({\it{x\/}}, {\it{y\/}} $-\;1$)\index{fy} \\ 
{\bf elseif }{\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}$\;\;${\bf then }{\bf{f}} \\ 
{\bf else }{\it{y\/}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  q-fails-at-x-fy \\ \index{q-fails-at-x-fy}
{\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\rightarrow$ ($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{q})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fy-is-a-number \\ \index{fy-is-a-number}
{\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\rightarrow$ ({\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\in\;${\bf{N}}${}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fy-is-defined \\ \index{fy-is-defined}
(($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fy-leq \\ \index{fy-leq}
{\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\rightarrow$ ({\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\leq$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fy-lessp \\ \index{fy-lessp}
({\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\wedge$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) $\rightarrow$ ({\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $<$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  q-below-undefined-fy \\ \index{q-below-undefined-fy}
(($\neg$ {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y1\/}} $\leq$ {\it{y\/}})) $\rightarrow$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y1\/}}))\index{q}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fy-is-first \\ \index{fy-is-first}
({\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy} $\wedge$ ({\it{y1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y1\/}} $<$ {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy})) $\rightarrow$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y1\/}}))\index{q}
\end{tabbing}

\begin{verbatim}; now, summarize what the Q-induction says for pairs:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  form-of-g \\ \index{form-of-g}
\=\+(\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) \\ 
$\wedge$$\;\;\;\;$({\it{x1\/}} $=$ {\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})) \\ 
$\wedge$$\;\;\;\;$({\it{y1\/}} $=$ {\rm{cdr}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{x1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g} $=$ {\rm{cons}}\,({\it{x1\/}}, {\it{y1\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g-is-below \\ \index{g-is-below}
\=\+(\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) \\ 
$\wedge$$\;\;\;\;$({\it{x1\/}} $=$ {\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})) \\ 
$\wedge$$\;\;\;\;$({\it{y1\/}} $=$ {\rm{cdr}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{x1\/}} $<$ {\it{x\/}}) $\vee$ (({\it{x1\/}} $=$ {\it{x\/}}) $\wedge$ ({\it{y1\/}} $<$ {\it{y\/}})))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  q-fails-at-g-aux1 \\ \index{q-fails-at-g-aux1}
\=\+(($\neg$ {\rm{q}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})\index{q}) $\wedge$ ({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g} $=$ {\rm{cons}}\,({\it{x1\/}}, {\it{y1\/}}))) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x1\/}}, {\it{y1\/}}))\index{q})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  q-fails-at-g \\ \index{q-fails-at-g}
\=\+(\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) \\ 
$\wedge$$\;\;\;\;$({\it{x1\/}} $=$ {\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})) \\ 
$\wedge$$\;\;\;\;$({\it{y1\/}} $=$ {\rm{cdr}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{g})))\- \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x1\/}}, {\it{y1\/}}))\index{q})\-
\end{tabbing}


\noindent{\sc Event}:   Disable q-fails-at-g-aux1.

\addvspace{18pt}

\begin{verbatim}; Now, if Q fails at x,y then Q fails at x,fy.  If we
; obtain x1,y1 from x,fy as above, we can't have 
; (and (equal x1 x) (lessp y1 fy)), so we must have x1 < x

\end{verbatim}\begin{tabbing}{\sc Theorem}:  smaller-x \\ \index{smaller-x}
\=\+(\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) \\ 
$\wedge$$\;\;\;\;$({\it{x1\/}} $=$ {\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g})) \\ 
$\wedge$$\;\;\;\;$({\it{y1\/}} $=$ {\rm{cdr}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g})))\- \\ 
$\rightarrow$$\;\;\;\;$(({\it{x1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y1\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{x1\/}} $<$ {\it{x\/}}) $\wedge$ ($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x1\/}}, {\it{y1\/}}))\index{q}))\-
\end{tabbing}

\begin{verbatim}; It is immediate from this that Q can never fail

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{q-holds-kludge} \\  
\=\+{\rm{q-holds-kludge}}\,({\it{x\/}}, {\it{y\/}})\index{q-holds-kludge} \\ 
$=$$\;\;\;\;$\=\+{\bf if }\=\+({\it{x\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g}) $\in\;${\bf{N}}${}$) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g}) $<$ {\it{x\/}})\- \\ 
{\bf then }{\rm{q-holds-kludge}}\,({\rm{car}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g}), {\rm{cdr}}\,({\rm{g}}\,({\rm{cons}}\,({\it{x\/}}, {\rm{fy}}\,({\it{x\/}}, {\it{y\/}})\index{fy}))\index{g}))\index{q-holds-kludge} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  q-holds \\ \index{q-holds}
(({\it{x\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\it{y\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ {\rm{q}}\,({\rm{cons}}\,({\it{x\/}}, {\it{y\/}}))\index{q}
\end{tabbing}



\begin{verbatim}; Finally, re-expressing this in terms of pairs:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  q-is-true \\ \index{q-is-true}
{\rm{ordp}}\,({\it{p\/}})\index{ordp} $\rightarrow$ {\rm{q}}\,({\it{p\/}})\index{q}
\end{tabbing}


\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 2                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; 1. We define qval (quick valuation).  This is a version of v&c$ which 
;    resets the cost to 0.  One problem with v&c$ is that it explicitly 
;    keeps track of the cost.  That makes proving theorems about
;    v&c$ working correctly on specific terms needlessly complicated.
; 2. We re-state the recursive definition of v&c$ in terms of qval.
; 3. We show how to formalize double recursions, such as occur in the 
;    definition of the Ackermann function.


; Since v&c$ uses the value of F to signify non-termination:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{reset} \\  
\=\+{\rm{reset}}\,({\it{x\/}})\index{reset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}}$\;\;${\bf then }{\rm{cons}}\,({\rm{car}}\,({\it{x\/}}), {\tt{0}}) \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{qval}$\;\;$
{\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} $=$ {\rm{reset}}\,({\rm{v\&c\$}}\,({\bf{t}}, {\it{term\/}}, {\it{va\/}}))\index{reset}
\end{tabbing}

\begin{verbatim}; va (a "variable assignment") is an association list which
; assigns values to variables.
; qval returns (val . 0) if the computation halts in the normal
; way to return val; otherwise, qval returns F

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{qval-list} \\  
\=\+{\rm{qval-list}}\,({\it{list-of-terms\/}}, {\it{va\/}})\index{qval-list} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{list-of-terms\/}} $\simeq\;${{\bf{nil}}}${}$$\;\;${\bf then }{\bf{nil}} \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{qval}}\,({\rm{car}}\,({\it{list-of-terms\/}}), {\it{va\/}})\index{qval}, \\ 
{\rm{qval-list}}\,({\rm{cdr}}\,({\it{list-of-terms\/}}), {\it{va\/}})\index{qval-list})\-$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Now, unwind the v&c$ axioms so that they are statements about
; qval and qval-list, and then disable qval and qval-list

; first, the two cases for qval-list:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-list-empty \\ \index{qval-list-empty}
({\it{lst\/}} $\simeq\;${{\bf{nil}}}${}$) $\rightarrow$ ({\rm{qval-list}}\,({\it{lst\/}}, {\it{va\/}})\index{qval-list} $=$ {\bf{nil}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-list-non-empty \\ \index{qval-list-non-empty}
\=\+{\rm{listp}}\,({\it{lst\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qval-list}}\,({\it{lst\/}}, {\it{va\/}})\index{qval-list} $=$ {\rm{cons}}\,({\rm{qval}}\,({\rm{car}}\,({\it{lst\/}}), {\it{va\/}})\index{qval}, {\rm{qval-list}}\,({\rm{cdr}}\,({\it{lst\/}}), {\it{va\/}})\index{qval-list}))\-
\end{tabbing}

\begin{verbatim}; in proving the cases for qval, it will be useful to have:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  same-f-membership \\ \index{same-f-membership}
({\bf{f}} $\in$ {\rm{qval-list}}\,({\it{lst\/}}, {\it{va\/}})\index{qval-list}) $\leftrightarrow$ ({\bf{f}} $\in$ {\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{lst\/}}, {\it{va\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  same-strip-cars \\ \index{same-strip-cars}
{\rm{strip-cars}}\,({\rm{qval-list}}\,({\it{lst\/}}, {\it{va\/}})\index{qval-list}) $=$ {\rm{strip-cars}}\,({\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{lst\/}}, {\it{va\/}}))
\end{tabbing}


\noindent{\sc Event}:   Disable qval-list.

\addvspace{18pt}

\begin{verbatim}; now, run down all the cases for qval:

; for a variable name, look up in assoc list
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-litatom \\ \index{qval-litatom}
{\rm{litatom}}\,({\it{term\/}}) $\rightarrow$ ({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} $=$ {\rm{cons}}\,({\rm{cdr}}\,({\rm{assoc}}\,({\it{term\/}}, {\it{va\/}})), {\tt{0}}))
\end{tabbing}

\begin{verbatim}; for a constant, return that constant value:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-constant \\ \index{qval-constant}
(($\neg$ {\rm{litatom}}\,({\it{term\/}})) $\wedge$ ({\it{term\/}} $\simeq\;${{\bf{nil}}}${}$)) $\rightarrow$ ({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} $=$ {\rm{cons}}\,({\it{term\/}}, {\tt{0}}))
\end{tabbing}

\begin{verbatim}; for a quoted expression, return the expression
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-quote \\ \index{qval-quote}
{\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{quote}}, {\it{object\/}}), {\it{va\/}})\index{qval} $=$ {\rm{cons}}\,({\it{object\/}}, {\tt{0}})
\end{tabbing}

\begin{verbatim}; evaluating an (if ...):
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-if \\ \index{qval-if}
\=\+{\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{if}}, {\it{test\/}}, {\it{thencase\/}}, {\it{elsecase\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{qval}}\,({\it{test\/}}, {\it{va\/}})\index{qval} \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\rm{qval}}\,({\it{test\/}}, {\it{va\/}})\index{qval})$\;\;${\bf then }{\rm{qval}}\,({\it{thencase\/}}, {\it{va\/}})\index{qval} \\ 
{\bf else }{\rm{qval}}\,({\it{elsecase\/}}, {\it{va\/}})\index{qval}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; except for (if ...) and (quote ...) : if evaluation of some
; arg doesn't halt, then qval doesn't halt.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-args-dont-halt-aux1 \\ \index{qval-args-dont-halt-aux1}
\=\+(({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) $\wedge$ ({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) $\wedge$ ({\bf{f}} $\in$ {\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}}))) \\ 
$\rightarrow$$\;\;\;\;$({\rm{v\&c\$}}\,({\bf{t}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}) $=$ {\bf{f}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-args-dont-halt \\ \index{qval-args-dont-halt}
\=\+(({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) $\wedge$ ({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) $\wedge$ ({\bf{f}} $\in$ {\rm{qval-list}}\,({\it{args\/}}, {\it{va\/}})\index{qval-list})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{qval}}\,({\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}})\index{qval} $=$ {\bf{f}})\-
\end{tabbing}

\begin{verbatim}; for a SUBR (a basic built-in) other than "if": if evaluation of the args 
; does halt, just use APPLY-SUBR on the value of args
; STRIP-CARS applied to ( (val1 . 0) (val2 . 0) ... ) returns (val1 val2 ...)

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-subr-aux1 \\ \index{qval-subr-aux1}
\=\+(({\bf{f}} $\not\in$ {\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}})) $\wedge$ ({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) $\wedge$ {\rm{subrp}}\,({\it{fn\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{v\&c\$}}\,({\bf{t}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}) \\ 
$=$$\;\;\;\;${\rm{cons}}\,(\=\+{\rm{apply-subr}}\,({\it{fn\/}}, {\rm{strip-cars}}\,({\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}}))), \\ 
$1\;+$ {\rm{sum-cdrs}}\,({\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}})))\-)\-\-
\end{tabbing}

\begin{verbatim}; the following auxiliary is trivial, 
; but the prover hangs on it:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-subr-aux2 \\ \index{qval-subr-aux2}
\=\+(({\it{vvv\/}} $=$ {\rm{cons}}\,({\it{uu\/}}, {\it{anything\/}})) $\wedge$ {\it{a\/}} $\wedge$ {\it{b\/}} $\wedge$ {\it{c\/}} $\wedge$ {\it{d\/}} $\wedge$ {\it{e\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\it{vvv\/}}) $=$ {\it{uu\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-subr \\ \index{qval-subr}
\=\+(({\bf{f}} $\not\in$ {\rm{qval-list}}\,({\it{args\/}}, {\it{va\/}})\index{qval-list}) $\wedge$ ({\it{fn\/}} $\not=$ {\tt{'}}{\tt{if}}) $\wedge$ {\rm{subrp}}\,({\it{fn\/}})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;${\rm{cons}}\,({\rm{apply-subr}}\,({\it{fn\/}}, {\rm{strip-cars}}\,({\rm{qval-list}}\,({\it{args\/}}, {\it{va\/}})\index{qval-list})), {\tt{0}}))\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-subr-aux2.

\addvspace{18pt}

\begin{verbatim}; for a non-SUBR (a basic built-in) other than "quote": 
; if evaluation of the args does halt, just evaluate 
; the BODY of the function on the 
; FORMALS of the function, paired with the value of the args

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-non-subr-aux1 \\ \index{qval-non-subr-aux1}
\=\+(({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) $\wedge$ ({\bf{f}} $\not\in$ {\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}})) $\wedge$ ($\neg$ {\rm{subrp}}\,({\it{fn\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{v\&c\$}}\,({\bf{t}}, {\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}}) \\ 
$=$$\;\;\;\;${\rm{fix-cost}}\,(\=\+{\rm{v\&c\$}}\,(\=\+{\bf{t}}, \\ 
{\rm{body}}\,({\it{fn\/}}), \\ 
{\rm{pairlist}}\,(\=\+{\rm{formals}}\,({\it{fn\/}}), \\ 
{\rm{strip-cars}}\,({\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}})))\-)\-, \\ 
$1\;+$ {\rm{sum-cdrs}}\,({\rm{v\&c\$}}\,({\tt{'}}{\tt{list}}, {\it{args\/}}, {\it{va\/}})))\-)\-\-
\end{tabbing}

\begin{verbatim}; again, the prover hangs on a trivial point
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-non-subr-aux2 \\ \index{qval-non-subr-aux2}
\=\+({\it{x1\/}} $\wedge$ ({\it{v1\/}} $=$ {\rm{cons}}\,({\it{w\/}}, {\it{x2\/}})) $\wedge$ {\it{x3\/}} $\wedge$ {\it{x4\/}} $\wedge$ {\it{x5\/}} $\wedge$ {\it{x6\/}} $\wedge$ {\it{x7\/}}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\it{v1\/}}) $=$ {\it{w\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-non-subr \\ \index{qval-non-subr}
\=\+(({\bf{f}} $\not\in$ {\rm{qval-list}}\,({\it{args\/}}, {\it{va\/}})\index{qval-list}) $\wedge$ ({\it{fn\/}} $\not=$ {\tt{'}}{\tt{quote}}) $\wedge$ ($\neg$ {\rm{subrp}}\,({\it{fn\/}}))) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\rm{cons}}\,({\it{fn\/}}, {\it{args\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\rm{body}}\,({\it{fn\/}}), \\ 
{\rm{pairlist}}\,({\rm{formals}}\,({\it{fn\/}}), {\rm{strip-cars}}\,({\rm{qval-list}}\,({\it{args\/}}, {\it{va\/}})\index{qval-list})))\-\index{qval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-non-subr-aux2.

\addvspace{18pt}

\begin{verbatim}; from now on, we need only the properties of qval and qval-list,
; not how they were defined:

\end{verbatim}
\noindent{\sc Event}:   Disable qval.

\addvspace{18pt}


\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; We illustrate the method by showing how to justify a double
; recursion, such as the definition of the Ackermann function:


;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;   Values of Ackermann Function
;
;    ---------------------
;  3| 1   2   4  16  2^16
;   |---------------------
;  2| 1   2   4   8   16
;   |---------------------
;  1| 1   2   4   6   8
;   |---------------------
;  0| 1   2   4   5   6
;   |_____________________
;     0   1   2   3   4
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; We can think of row 0 as given.  Row n+1 is obtained by
; iterating the function on row n, starting with a 1 in column 0.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{row0} \\  
\=\+{\rm{row0}}\,({\it{x\/}})\index{row0} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\it{x\/}} $+$ {\tt{2}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{row1} \\  
\=\+{\rm{row1}}\,({\it{x\/}})\index{row1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{row0}}\,({\rm{row1}}\,({\it{x\/}} $-\;1$)\index{row1})\index{row0}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{row2} \\  
\=\+{\rm{row2}}\,({\it{x\/}})\index{row2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{row1}}\,({\rm{row2}}\,({\it{x\/}} $-\;1$)\index{row2})\index{row1}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{row3} \\  
\=\+{\rm{row3}}\,({\it{x\/}})\index{row3} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{row2}}\,({\rm{row3}}\,({\it{x\/}} $-\;1$)\index{row3})\index{row2}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; GOAL: define a function, ACKERMANN, and prove
; (prove-lemma ackermann-works (rewrite) (equal (ackermann x y)
; 	(if (zerop x) 1
; 	(if (zerop y) (if (equal x 1) 2 (plus x 2))
; 	(ackermann (ackermann (sub1 x) y) (sub1 y))  ))))

; Without using ordinals and ord-lessp, we can't just use this
; as a definition.  However, we can use EVAL$ to define
; function whose body looks like this.  To simplify the work, we
; phrase the defn of ack so that the body is as simple as possible

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{base}$\;\;$
{\rm{base}}\,({\it{x\/}}, {\it{y\/}})\index{base} $=$ (({\it{x\/}} $\simeq {\tt{0}}$) $\vee$ ({\it{y\/}} $\simeq {\tt{0}}$))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{base-fn} \\  
\=\+{\rm{base-fn}}\,({\it{x\/}}, {\it{y\/}})\index{base-fn} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{y\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{row0}}\,({\it{x\/}})\index{row0} \\ 
{\bf else }{\tt{1}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; intended defn of ack is now:
;(defn ack (x y) (if (base x y) (base-fn x y)  (ack (ack (sub1 x) y) (sub1 y))))

; instead, use eval$ :
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ack} \\  
\=\+{\rm{ack}}\,({\it{x\/}}, {\it{y\/}})\index{ack} \\ 
$=$$\;\;\;\;${\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\tt{'}}{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{base}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{base-fn}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{x\/}}), {\rm{cons}}\,({\tt{'}}{\tt{y}}, {\it{y\/}})))\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;  begin r-loop

; *(body 'ack)
;  '(IF (BASE X Y)
;       (BASE-FN X Y)
;       (ACK (ACK (SUB1 X) Y) (SUB1 Y)))
; *(formals 'ack)
;  '(X Y)
; *(ack 3 1)
;  6
; *(ack 2 3)
;  4
; *(ack 4 2)
;  16
; *(qval '(ack x y) '( (x . 4) (y . 2) ))
;  '(16 . 0)
;;;;;;;;;;;;;;;;;;;;;;;  end r-loop

; Now that we have arranged for ack to have the correct body and formals, 
; we never use eval$ again.  We can define the official Ackermann function 
; using qval, and then prove inductively that it works.
; Since the formals will always be '(x y), we can simplify
; some of the general notation:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{assn} \\  
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn} $=$ {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{valx\/}}), {\rm{cons}}\,({\tt{'}}{\tt{y}}, {\it{valy\/}}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{a}$\;\;$
{\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a} $=$ {\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ackermann}$\;\;$
{\rm{ackermann}}\,({\it{valx\/}}, {\it{valy\/}})\index{ackermann} $=$ {\rm{car}}\,({\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a})
\end{tabbing}

\begin{verbatim}; Proving that ackermann works involves proving first that (A valx valy)
; holds (i.e., it is never F).

; First, since qval-list will always be operating on lists of terms of
; length two, let's concretely unwind that situation:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-list-1 \\ \index{qval-list-1}
{\rm{qval-list}}\,({\rm{list}}\,({\it{term\/}}), {\it{va\/}})\index{qval-list} $=$ {\rm{list}}\,({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  qval-list-2 \\ \index{qval-list-2}
{\rm{qval-list}}\,({\rm{list}}\,({\it{term1\/}}, {\it{term2\/}}), {\it{va\/}})\index{qval-list} $=$ {\rm{list}}\,({\rm{qval}}\,({\it{term1\/}}, {\it{va\/}})\index{qval}, {\rm{qval}}\,({\it{term2\/}}, {\it{va\/}})\index{qval})
\end{tabbing}


\noindent{\sc Event}:   Disable qval-list-non-empty.

\addvspace{18pt}

\begin{verbatim}; Now, analyze how qval works on sub-expressions of the body:
;   (if (base x y) (base-fn x y) (ack (ack (sub1 x) y) (sub1 y)))

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-x \\ \index{qval-on-x}
{\rm{qval}}\,({\tt{'}}{\tt{x}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\it{valx\/}}, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-on-y \\ \index{qval-on-y}
{\rm{qval}}\,({\tt{'}}{\tt{y}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\it{valy\/}}, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-on-sub1-x \\ \index{qval-on-sub1-x}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\it{valx\/}} $-\;1$, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-on-sub1-y \\ \index{qval-on-sub1-y}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\it{valy\/}} $-\;1$, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-on-base \\ \index{qval-on-base}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{base}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-on-base-fn \\ \index{qval-on-base-fn}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{base-fn}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\rm{base-fn}}\,({\it{valx\/}}, {\it{valy\/}})\index{base-fn}, {\tt{0}})
\end{tabbing}

\begin{verbatim}; on the whole body
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-body \\ \index{qval-on-body}
\=\+{\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{base}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{base-fn}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\-\index{qval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}$\;\;${\bf then }{\rm{cons}}\,({\rm{base-fn}}\,({\it{valx\/}}, {\it{valy\/}})\index{base-fn}, {\tt{0}}) \\ 
{\bf else }{\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}, \\ 
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\-\index{qval}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim}; Now on the ack expressions, we need two things:
; 1. Unwind the (qval '(ack x y) (assn valx valy)) in
;    the defn of (A valx valy) so we can prove thms about A
; 2. Reduce qval of the two ack expressions in the body:
;      (ack (sub1 x) y)       (ack (ack (sub1 x) y) (sub1 y))
;    to a qval of (ack x y)

; towards (2):

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ack-of-terms-aux1 \\ \index{qval-of-ack-of-terms-aux1}
\=\+({\rm{qval}}\,({\it{term1\/}}, {\it{va\/}})\index{qval} $\wedge$ {\rm{qval}}\,({\it{term2\/}}, {\it{va\/}})\index{qval}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{ack}}, {\it{term1\/}}, {\it{term2\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{base}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{base-fn}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{assn}}\,({\rm{car}}\,({\rm{qval}}\,({\it{term1\/}}, {\it{va\/}})\index{qval}), {\rm{car}}\,({\rm{qval}}\,({\it{term2\/}}, {\it{va\/}})\index{qval}))\index{assn})\-\index{qval})\-\-
\end{tabbing}

\begin{verbatim}; as a special case, for (ack x y):
     
\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ackxy-aux1 \\ \index{qval-of-ackxy-aux1}
\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}\=\+{\tt{if}} \\ 
{\tt{(}}{\tt{base}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{base-fn}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}} \\ 
{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}{\tt{)}}\-, \\ 
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\-\index{qval}\-
\end{tabbing}

\begin{verbatim}; we can unwind the if expr later -- first, let's reduce the
; (ack term1 term2).

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ack-of-terms \\ \index{qval-of-ack-of-terms}
\=\+({\rm{qval}}\,({\it{term1\/}}, {\it{va\/}})\index{qval} $\wedge$ {\rm{qval}}\,({\it{term2\/}}, {\it{va\/}})\index{qval}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{ack}}, {\it{term1\/}}, {\it{term2\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, \\ 
{\rm{assn}}\,({\rm{car}}\,({\rm{qval}}\,({\it{term1\/}}, {\it{va\/}})\index{qval}), {\rm{car}}\,({\rm{qval}}\,({\it{term2\/}}, {\it{va\/}})\index{qval}))\index{assn})\-\index{qval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-of-ack-of-terms-aux1.

\addvspace{18pt}

\begin{verbatim}; Now, unwinding the if expr:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ackxy \\ \index{qval-of-ackxy}
\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}$\;\;${\bf then }{\rm{cons}}\,({\rm{base-fn}}\,({\it{valx\/}}, {\it{valy\/}})\index{base-fn}, {\tt{0}}) \\ 
{\bf else }{\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}, \\ 
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\-\index{qval}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-of-ackxy-aux1.

\addvspace{18pt}

\begin{verbatim}; now, qval-of-ackxy would be simpler if we split it into
; the two cases base/non-base

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ackxy-base \\ \index{qval-of-ackxy-base}
\=\+{\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base} \\ 
$\rightarrow$$\;\;\;\;$({\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} $=$ {\rm{cons}}\,({\rm{base-fn}}\,({\it{valx\/}}, {\it{valy\/}})\index{base-fn}, {\tt{0}}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-of-ackxy-non-base-aux1 \\ \index{qval-of-ackxy-non-base-aux1}
\=\+($\neg$ {\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}, \\ 
{\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\-\index{qval})\-\-
\end{tabbing}
\begin{verbatim}; we have to analyze this further

\end{verbatim}
\noindent{\sc Event}:   Disable qval-of-ackxy.

\addvspace{18pt}

\begin{verbatim}; Now, we have to reduce the two ack expressions in the body:
;      (ack (sub1 x) y)       (ack (ack (sub1 x) y) (sub1 y))
;         small                       big

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ack-small \\ \index{qval-of-ack-small}
\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{assn})\index{qval}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  qval-of-ack-big \\ \index{qval-of-ack-big}
\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{assn})\index{qval} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{y}}{\tt{)}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, \\ 
{\rm{assn}}\,(\=\+{\rm{car}}\,({\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{(}}{\tt{sub1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval}), \\ 
{\it{valy\/}} $-\;1$)\-\index{assn})\-\index{qval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-of-ack-of-terms.

\addvspace{18pt}
\begin{verbatim}; we only need it for "small" and "big"

; using these, we can analyze the non-base case

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-of-ackxy-non-base \\ \index{qval-of-ackxy-non-base}
\=\+(($\neg$ {\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}) $\wedge$ {\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{assn})\index{qval}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}}, {\it{valy\/}})\index{assn})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, \\ 
{\rm{assn}}\,(\=\+{\rm{car}}\,({\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{assn})\index{qval}), \\ 
{\it{valy\/}} $-\;1$)\-\index{assn})\-\index{qval})\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable qval-of-ackxy-non-base-aux1.

\addvspace{18pt}


\noindent{\sc Event}:   Disable assn.

\addvspace{18pt}   
\begin{verbatim}; this is no longer needed, and it really slows things
; down when assn is unwound

; Now, let's prove : (A valx valy) by induction on (valx valy).
; Then -- we can remove the (qval '(ack x y) ...) hypotheses

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-is-true-aux1 \\ \index{a-is-true-aux1}
{\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base} $\rightarrow$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}
\end{tabbing}

\begin{verbatim}; specifically, there is only a problem if valx or valy are non-zero
\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-is-true-aux2 \\ \index{a-is-true-aux2}
({\it{valx\/}} $\simeq {\tt{0}}$) $\rightarrow$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  a-is-true-aux3 \\ \index{a-is-true-aux3}
({\it{valy\/}} $\simeq {\tt{0}}$) $\rightarrow$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}
\end{tabbing}

\begin{verbatim}; let's give a name to the x-value called in qval-of-ackxy-non-base
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{prev} \\  
{\rm{prev}}\,({\it{valx\/}}, {\it{valy\/}})\index{prev} $=$ {\rm{car}}\,({\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ack}}{\tt{ }}{\tt{x}}{\tt{ }}{\tt{y}}{\tt{)}}, {\rm{assn}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{assn})\index{qval})
\end{tabbing}
\begin{verbatim}; this will make the induction simpler

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-is-true-aux4 \\ \index{a-is-true-aux4}
\=\+(($\neg$ {\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}) $\wedge$ {\rm{a}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{a} $\wedge$ {\rm{a}}\,({\rm{prev}}\,({\it{valx\/}}, {\it{valy\/}})\index{prev}, {\it{valy\/}} $-\;1$)\index{a}) \\ 
$\rightarrow$$\;\;\;\;${\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}\-
\end{tabbing}


\noindent{\sc Event}:   Disable a.

\addvspace{18pt}  \begin{verbatim}; temporarily
\end{verbatim}
\noindent{\sc Event}:   Disable prev.

\addvspace{18pt} \begin{verbatim}; permanently

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We have enough now to prove that (A valx valy) is true by double induction,
; as in ITEM 1, above.
; If (A valx valy) fails, then (A valx' valy') fails, where
; (valy' valx') is lexically earlier than (valy valx).

; First,  by ordinary induction on valx (holding valy fixed):
; if (not (A valx valy)), there is a first-value, 
; fx = (fx valx valy), such that: (not (A fx valy)) but (A (sub1 fx) valy)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fx} \\  
\=\+{\rm{fx}}\,({\it{valx\/}}, {\it{valy\/}})\index{fx} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{valx\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }($\neg$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}) $\wedge$ {\rm{a}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{a}$\;\;${\bf then }{\it{valx\/}} \\ 
{\bf else }{\rm{fx}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{fx}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fx-is-first-1 \\ \index{fx-is-first-1}
($\neg$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}) $\rightarrow$ ($\neg$ {\rm{a}}\,({\rm{fx}}\,({\it{valx\/}}, {\it{valy\/}})\index{fx}, {\it{valy\/}})\index{a})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fx-is-first-2 \\ \index{fx-is-first-2}
($\neg$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}) $\rightarrow$ {\rm{a}}\,({\rm{fx}}\,({\it{valx\/}}, {\it{valy\/}})\index{fx} $-\;1$, {\it{valy\/}})\index{a}
\end{tabbing}

\begin{verbatim}; now, reexamine what A-is-true-aux4 says

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-is-true-aux5 \\ \index{a-is-true-aux5}
($\neg$ {\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}) $\rightarrow$ ($\neg$ {\rm{a}}\,({\rm{prev}}\,({\rm{fx}}\,({\it{valx\/}}, {\it{valy\/}})\index{fx}, {\it{valy\/}})\index{prev}, {\it{valy\/}} $-\;1$)\index{a})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{a-is-true-kludge} \\  
\=\+{\rm{a-is-true-kludge}}\,({\it{valx\/}}, {\it{valy\/}})\index{a-is-true-kludge} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{valy\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{a-is-true-kludge}}\,({\rm{prev}}\,({\rm{fx}}\,({\it{valx\/}}, {\it{valy\/}})\index{fx}, {\it{valy\/}})\index{prev}, {\it{valy\/}} $-\;1$)\index{a-is-true-kludge}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-is-true \\ \index{a-is-true}
{\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a}
\end{tabbing}


\noindent{\sc Event}:   Disable a-is-true-aux1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-is-true-aux2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-is-true-aux3.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-is-true-aux4.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-is-true-aux5.

\addvspace{18pt}

\noindent{\sc Event}:   Disable fx.

\addvspace{18pt}

\noindent{\sc Event}:   Disable fx-is-first-1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable fx-is-first-2.

\addvspace{18pt}

\noindent{\sc Event}:   Disable a-is-true-kludge.

\addvspace{18pt}

\begin{verbatim}; now, we do care what A is
\end{verbatim}
\noindent{\sc Event}:   Enable a.

\addvspace{18pt}
\begin{verbatim}; while we rephrase  qval-of-ackxy-base and  qval-of-ackxy-non-base 
; in terms of A, using the fact that A is true:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  a-base \\ \index{a-base}
{\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base} $\rightarrow$ ({\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a} $=$ {\rm{cons}}\,({\rm{base-fn}}\,({\it{valx\/}}, {\it{valy\/}})\index{base-fn}, {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a-induction \\ \index{a-induction}
\=\+($\neg$ {\rm{base}}\,({\it{valx\/}}, {\it{valy\/}})\index{base}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{a}}\,({\it{valx\/}}, {\it{valy\/}})\index{a} $=$ {\rm{a}}\,({\rm{car}}\,({\rm{a}}\,({\it{valx\/}} $-\;1$, {\it{valy\/}})\index{a}), {\it{valy\/}} $-\;1$)\index{a})\-
\end{tabbing}

\begin{verbatim}; Now, we can forget how A was defined; its car satisfies
; the defn of the Ackermann function

\end{verbatim}
\noindent{\sc Event}:   Disable a.

\addvspace{18pt}

\begin{verbatim}; GOAL:
\end{verbatim}\begin{tabbing}{\sc Theorem}:  ackermann-works \\ \index{ackermann-works}
\=\+{\rm{ackermann}}\,({\it{x\/}}, {\it{y\/}})\index{ackermann} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{y\/}} $\simeq {\tt{0}}$ \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\it{x\/}} $+$ {\tt{2}}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{ackermann}}\,({\rm{ackermann}}\,({\it{x\/}} $-\;1$, {\it{y\/}})\index{ackermann}, {\it{y\/}} $-\;1$)\index{ackermann}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 3                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; GOAL:  define a function
; (next-twin-prime x) and prove, that for each x
; either:
;   1. (next-twin-prime x) is some y > x such that y, y+2 are both prime
; or
;   2. (next-twin-prime x) = F, and 
;      for all y > x, it isn't true that y and y+2 are both prime

; First, define some primitive recursive functions

; a divisor of x between 2 and top (inclusively), or,  F if there is none :
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{divisor} \\  
\=\+{\rm{divisor}}\,({\it{x\/}}, {\it{top\/}})\index{divisor} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{top\/}} $<$ {\tt{2}}$\;\;${\bf then }{\bf{f}} \\ 
{\bf elseif }{\rm{divisor}}\,({\it{x\/}}, {\it{top\/}} $-\;1$)\index{divisor}$\;\;${\bf then }{\rm{divisor}}\,({\it{x\/}}, {\it{top\/}} $-\;1$)\index{divisor} \\ 
{\bf elseif }({\it{x\/}} ${}${\bf{mod}}${}$ {\it{top\/}}) $\simeq {\tt{0}}$$\;\;${\bf then }{\it{top\/}} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{primep}$\;\;$
{\rm{primep}}\,({\it{x\/}})\index{primep} $=$ (({\tt{1}} $<$ {\it{x\/}}) $\wedge$ ($\neg$ {\rm{divisor}}\,({\it{x\/}}, {\it{x\/}} $-\;1$)\index{divisor}))
\end{tabbing}

\begin{verbatim}; y is the first part of a prime pair
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fpp}$\;\;$
{\rm{fpp}}\,({\it{y\/}})\index{fpp} $=$ ({\rm{primep}}\,({\it{y\/}})\index{primep} $\wedge$ {\rm{primep}}\,($1\;+$ ($1\;+$ {\it{y\/}}))\index{primep})
\end{tabbing}

\begin{verbatim}; intended -- by upwards recursion 
; (defn next-twin-prime(x) (if (fpp (add1 x))
; 	(add1 x)
; 	(next-twin-prime (add1 x))))

; obviously, this won't be accepted, but in Nqthm, one can do this with eval$ :

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{ntp} \\  
\=\+{\rm{ntp}}\,({\it{x\/}})\index{ntp} \\ 
$=$$\;\;\;\;${\rm{eval\$}}\,(\=\+{\bf{t}}, \\ 
{\tt{'}}{\tt{(}}{\tt{if}}{\tt{ }}{\tt{(}}{\tt{fpp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{x\/}})))\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;  begin r-loop
; 
; *(formals 'ntp)
;  '(X)
; *(body 'ntp)
;  '(IF (FPP (ADD1 X))
;       (ADD1 X)
;       (NTP (ADD1 X)))
; *(ntp 8)
;  11
; *(ntp 19)
;  29
; *(formals 'fpp)
;  '(Y)
; *(body 'fpp)
;  '(AND (PRIMEP Y)
;        (PRIMEP (ADD1 (ADD1 Y))))
; 
;;;;;;;;;;;;;;;;;;;;;;;  end r-loop

; Of course, this doesn't prove anything.  
; We want to define next-twin-prime AND PROVE IT WORKS

; Using the same trick as with the Ackermann function:
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n}$\;\;$
{\rm{n}}\,({\it{valx\/}})\index{n} $=$ {\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{x}}{\tt{)}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{valx\/}})))\index{qval}
\end{tabbing}


\begin{verbatim}; Now, we have to analyze qval on the body of ntp
;  '(if (fpp (add1 x)) (add1 x) (ntp (add1 x)))
; Fortunately, for a pure primitive recursive function, such as fpp.
; the Nqthm built-ins REWRITE-V&C-APPLY$ and REWRITE-CAR-V&C-APPLY$
; easily prove that v&c$ does the right thing; so:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-fpp \\ \index{qval-on-fpp}
\=\+{\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} \\ 
$\rightarrow$$\;\;\;\;$({\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{fpp}}, {\it{term\/}}), {\it{va\/}})\index{qval} $=$ {\rm{cons}}\,({\rm{fpp}}\,({\rm{car}}\,({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval}))\index{fpp}, {\tt{0}}))\-
\end{tabbing}


\noindent{\sc Event}:   Disable fpp.

\addvspace{18pt}

\begin{verbatim}; as with ack, we have to compare qval on an expression
; (ntp term) with qval on the basic (ntp x)

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-ntp-term \\ \index{qval-on-ntp-term}
\=\+{\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{ntp}}, {\it{term\/}}), {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;${\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{x}}{\tt{)}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\rm{car}}\,({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval}))))\index{qval})\-\-
\end{tabbing}

\begin{verbatim}; we can rewrite this in terms of N

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-ntp-term-n \\ \index{qval-on-ntp-term-n}
{\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval} $\rightarrow$ ({\rm{qval}}\,({\rm{list}}\,({\tt{'}}{\tt{ntp}}, {\it{term\/}}), {\it{va\/}})\index{qval} $=$ {\rm{n}}\,({\rm{car}}\,({\rm{qval}}\,({\it{term\/}}, {\it{va\/}})\index{qval}))\index{n})
\end{tabbing}

\begin{verbatim}; Now, the relevant term in the body is just (add1 x), so:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  qval-on-ntp-add1 \\ \index{qval-on-ntp-add1}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{valx\/}})))\index{qval} $=$ {\rm{n}}\,($1\;+$ {\it{valx\/}})\index{n}
\end{tabbing}

\begin{verbatim}; now, we unwind the defn of N:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  unwind-1 \\ \index{unwind-1}
\=\+{\rm{n}}\,({\it{valx\/}})\index{n} \\ 
$=$$\;\;\;\;${\rm{qval}}\,(\=\+{\tt{'}}{\tt{(}}{\tt{if}}{\tt{ }}{\tt{(}}{\tt{fpp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{)}}, \\ 
{\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{valx\/}})))\-\index{qval}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unwind-2 \\ \index{unwind-2}
{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{fpp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}, {\it{va\/}})\index{qval} $=$ {\rm{cons}}\,({\rm{fpp}}\,($1\;+$ {\rm{cdr}}\,({\rm{assoc}}\,({\tt{'}}{\tt{x}}, {\it{va\/}})))\index{fpp}, {\tt{0}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unwind-3 \\ \index{unwind-3}
\=\+{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{if}}{\tt{ }}{\tt{(}}{\tt{fpp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{ }}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}{\tt{)}}, {\it{va\/}})\index{qval} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{fpp}}\,($1\;+$ {\rm{cdr}}\,({\rm{assoc}}\,({\tt{'}}{\tt{x}}, {\it{va\/}})))\index{fpp}$\;\;${\bf then }{\rm{cons}}\,($1\;+$ {\rm{cdr}}\,({\rm{assoc}}\,({\tt{'}}{\tt{x}}, {\it{va\/}})), {\tt{0}}) \\ 
{\bf else }{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}, {\it{va\/}})\index{qval}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unwind-4 \\ \index{unwind-4}
\=\+{\rm{n}}\,({\it{valx\/}})\index{n} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{fpp}}\,($1\;+$ {\it{valx\/}})\index{fpp}$\;\;${\bf then }{\rm{cons}}\,($1\;+$ {\it{valx\/}}, {\tt{0}}) \\ 
{\bf else }{\rm{qval}}\,({\tt{'}}{\tt{(}}{\tt{ntp}}{\tt{ }}{\tt{(}}{\tt{add1}}{\tt{ }}{\tt{x}}{\tt{)}}{\tt{)}}, {\rm{list}}\,({\rm{cons}}\,({\tt{'}}{\tt{x}}, {\it{valx\/}})))\index{qval}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unwind-5 \\ \index{unwind-5}
\=\+{\rm{n}}\,({\it{valx\/}})\index{n} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{fpp}}\,($1\;+$ {\it{valx\/}})\index{fpp}$\;\;${\bf then }{\rm{cons}}\,($1\;+$ {\it{valx\/}}, {\tt{0}}) \\ 
{\bf else }{\rm{n}}\,($1\;+$ {\it{valx\/}})\index{n}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable unwind-1.

\addvspace{18pt} 
\noindent{\sc Event}:   Disable unwind-2.

\addvspace{18pt} 
\noindent{\sc Event}:   Disable unwind-3.

\addvspace{18pt}

\noindent{\sc Event}:   Disable unwind-4.

\addvspace{18pt} 
\noindent{\sc Event}:   Disable unwind-5.

\addvspace{18pt}

\begin{verbatim}; now, we can justify the upward recursion:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  n-basis \\ \index{n-basis}
{\rm{fpp}}\,($1\;+$ {\it{x\/}})\index{fpp} $\rightarrow$ ({\rm{n}}\,({\it{x\/}})\index{n} $=$ {\rm{cons}}\,($1\;+$ {\it{x\/}}, {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n-induction \\ \index{n-induction}
($\neg$ {\rm{fpp}}\,($1\;+$ {\it{x\/}})\index{fpp}) $\rightarrow$ ({\rm{n}}\,({\it{x\/}})\index{n} $=$ {\rm{n}}\,($1\;+$ {\it{x\/}})\index{n})
\end{tabbing}

\begin{verbatim}; it might be useful to know the form of N

\end{verbatim}\begin{tabbing}{\sc Theorem}:  form-of-n \\ \index{form-of-n}
{\rm{n}}\,({\it{x\/}})\index{n} $\rightarrow$ ({\rm{n}}\,({\it{x\/}})\index{n} $=$ {\rm{cons}}\,({\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n}), {\tt{0}}))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  n-of-zero \\ \index{n-of-zero}
({\it{x\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{n}}\,({\it{x\/}})\index{n} $=$ {\tt{'}}{\tt{(}}{\tt{3}}{\tt{ .\ }}{\tt{0}}{\tt{)}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{good}$\;\;$
{\rm{good}}\,({\it{x\/}})\index{good} $=$ ({\rm{fpp}}\,({\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n}))\index{fpp} $\wedge$ ({\it{x\/}} $<$ {\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n})))
\end{tabbing}
\begin{verbatim}; so, the twin prime conjecture will imply that all x are good

; we don't need the defn of N any more:
\end{verbatim}
\noindent{\sc Event}:   Disable n.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  n-of-fpp \\ \index{n-of-fpp}
{\rm{fpp}}\,({\it{x\/}})\index{fpp} $\rightarrow$ ({\rm{n}}\,({\it{x\/}} $-\;1$)\index{n} $=$ {\rm{cons}}\,({\it{x\/}}, {\tt{0}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n-of-non-fpp \\ \index{n-of-non-fpp}
(($\neg$ {\rm{fpp}}\,({\it{x\/}})\index{fpp}) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$)) $\rightarrow$ ({\rm{n}}\,({\it{x\/}} $-\;1$)\index{n} $=$ {\rm{n}}\,({\it{x\/}})\index{n})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  zero-is-good \\ \index{zero-is-good}
({\it{x\/}} $\simeq {\tt{0}}$) $\rightarrow$ {\rm{good}}\,({\it{x\/}})\index{good}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-goes-down-aux1 \\ \index{good-goes-down-aux1}
{\rm{fpp}}\,({\it{x\/}})\index{fpp} $\rightarrow$ {\rm{good}}\,({\it{x\/}} $-\;1$)\index{good}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-goes-down-aux2 \\ \index{good-goes-down-aux2}
(($\neg$ {\rm{fpp}}\,({\it{x\/}})\index{fpp}) $\wedge$ ({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ {\rm{good}}\,({\it{x\/}})\index{good}) $\rightarrow$ {\rm{good}}\,({\it{x\/}} $-\;1$)\index{good}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-goes-down \\ \index{good-goes-down}
{\rm{good}}\,({\it{x\/}})\index{good} $\rightarrow$ {\rm{good}}\,({\it{x\/}} $-\;1$)\index{good}
\end{tabbing}

\begin{verbatim}; Next, we prove that (fpp y) and x < y implies (good x)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{good-below-kludge} \\  
\=\+{\rm{good-below-kludge}}\,({\it{y\/}}, {\it{z\/}})\index{good-below-kludge} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{z\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{good-below-kludge}}\,({\it{y\/}}, {\it{z\/}} $-\;1$)\index{good-below-kludge}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-below-aux1 \\ \index{good-below-aux1}
(({\it{y\/}} $-\;1$) $-$ {\it{z\/}}) $=$ (({\it{y\/}} $-$ {\it{z\/}}) $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-below-aux2 \\ \index{good-below-aux2}
{\rm{fpp}}\,({\it{y\/}})\index{fpp} $\rightarrow$ {\rm{good}}\,({\it{y\/}} $-$ ($1\;+$ {\it{z\/}}))\index{good}
\end{tabbing}


\noindent{\sc Event}:   Disable good-below-aux1.

\addvspace{18pt}

\noindent{\sc Event}:   Disable good-below-aux2.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  good-below-aux3 \\ \index{good-below-aux3}
(({\it{x\/}} $<$ {\it{y\/}}) $\wedge$ ({\it{x\/}} $\in\;${\bf{N}}${}$)) $\rightarrow$ (({\it{y\/}} $-$ ($1\;+$ (({\it{y\/}} $-$ {\it{x\/}}) $-\;1$))) $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  good-below \\ \index{good-below}
({\rm{fpp}}\,({\it{y\/}})\index{fpp} $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ {\rm{good}}\,({\it{x\/}})\index{good}
\end{tabbing}


\noindent{\sc Event}:   Disable good-below-aux3.

\addvspace{18pt}

\begin{verbatim}; now, every x is either good or not good.

; if x is not good, there are no twin primes above x:

\end{verbatim}\begin{tabbing}{\sc Theorem}:  properties-of-bad-aux1 \\ \index{properties-of-bad-aux1}
(($\neg$ {\rm{good}}\,({\it{x\/}})\index{good}) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ ($\neg$ {\rm{fpp}}\,({\it{y\/}})\index{fpp})
\end{tabbing}

\begin{verbatim}; on the other hand, if x is good, then by the definition

\end{verbatim}\begin{tabbing}{\sc Theorem}:  properties-of-good-aux1 \\ \index{properties-of-good-aux1}
{\rm{good}}\,({\it{x\/}})\index{good} $\rightarrow$ ({\rm{fpp}}\,({\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n}))\index{fpp} $\wedge$ ({\it{x\/}} $<$ {\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n})))
\end{tabbing}

\begin{verbatim}; Now, we can define next-twin-prime as:

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{next-twin-prime} \\  
\=\+{\rm{next-twin-prime}}\,({\it{x\/}})\index{next-twin-prime} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{good}}\,({\it{x\/}})\index{good}$\;\;${\bf then }{\rm{car}}\,({\rm{n}}\,({\it{x\/}})\index{n}) \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable good-below.

\addvspace{18pt}

\noindent{\sc Event}:   Disable good.

\addvspace{18pt}

\begin{verbatim}; finally, GOAL:

; EITHER
;   1. (next-twin-prime x) is some y > x such that y, y+2 are both prime
\end{verbatim}\begin{tabbing}{\sc Theorem}:  properties-of-good \\ \index{properties-of-good}
{\rm{good}}\,({\it{x\/}})\index{good} $\rightarrow$ ({\rm{fpp}}\,({\rm{next-twin-prime}}\,({\it{x\/}})\index{next-twin-prime})\index{fpp} $\wedge$ ({\it{x\/}} $<$ {\rm{next-twin-prime}}\,({\it{x\/}})\index{next-twin-prime}))
\end{tabbing}

\begin{verbatim}; OR
;   2. (next-twin-prime x) = F, and 
;      for all y > x, it isn't true that y and y+2 are both prime
\end{verbatim}\begin{tabbing}{\sc Theorem}:  properties-of-bad-1 \\ \index{properties-of-bad-1}
($\neg$ {\rm{good}}\,({\it{x\/}})\index{good}) $\rightarrow$ ({\rm{next-twin-prime}}\,({\it{x\/}})\index{next-twin-prime} $=$ {\bf{f}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  properties-of-bad-2 \\ \index{properties-of-bad-2}
(($\neg$ {\rm{good}}\,({\it{x\/}})\index{good}) $\wedge$ ({\it{x\/}} $<$ {\it{y\/}})) $\rightarrow$ ($\neg$ {\rm{fpp}}\,({\it{y\/}})\index{fpp})
\end{tabbing}


\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       THE END                              ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;





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