\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.  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 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 Robert S. Boyer 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 initial {\bf nqthm} theory.

\addvspace{18pt}

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

\addvspace{18pt}

\begin{verbatim};   The floor of the square root. This definition is taken from Goodstein.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{rt} \\  
\=\+{\rm{rt}}\,({\it{x\/}})\index{rt} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{x\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }(($1\;+$ {\rm{rt}}\,({\it{x\/}} $-\;1$)\index{rt}) $*$ ($1\;+$ {\rm{rt}}\,({\it{x\/}} $-\;1$)\index{rt})) $=$ {\it{x\/}}$\;\;${\bf then }$1\;+$ {\rm{rt}}\,({\it{x\/}} $-\;1$)\index{rt} \\ 
{\bf else }{\rm{rt}}\,({\it{x\/}} $-\;1$)\index{rt}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  times-add1 \\ \index{times-add1}
({\it{x\/}} $*$ ($1\;+$ {\it{y\/}})) $=$ ({\it{x\/}} $+$ ({\it{x\/}} $*$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  plus-add1 \\ \index{plus-add1}
({\it{x\/}} $+$ ($1\;+$ {\it{y\/}})) $=$ ($1\;+$ ({\it{x\/}} $+$ {\it{y\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  square-0 \\ \index{square-0}
(({\it{x\/}} $*$ {\it{x\/}}) $=$ {\tt{0}}) $=$ ({\it{x\/}} $\simeq {\tt{0}}$)
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  square-monotonic \\ \index{square-monotonic}
({\it{b\/}} $\not<$ {\it{a\/}}) $\rightarrow$ (({\it{b\/}} $*$ {\it{b\/}}) $\not<$ ({\it{a\/}} $*$ {\it{a\/}}))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  spec-for-rt \\ \index{spec-for-rt}
\=\+({\it{y\/}} $\not<$ ({\rm{rt}}\,({\it{y\/}})\index{rt} $*$ {\rm{rt}}\,({\it{y\/}})\index{rt})) \\ 
$\wedge$$\;\;\;\;$({\it{y\/}} $<$ ($1\;+$ ({\rm{rt}}\,({\it{y\/}})\index{rt} $+$ ({\rm{rt}}\,({\it{y\/}})\index{rt} $+$ ({\rm{rt}}\,({\it{y\/}})\index{rt} $*$ {\rm{rt}}\,({\it{y\/}})\index{rt})))))\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rt-is-unique \\ \index{rt-is-unique}
\=\+(({\it{a\/}} $\in\;${\bf{N}}${}$) $\wedge$ (({\it{a\/}} $*$ {\it{a\/}}) $\leq$ {\it{y\/}}) $\wedge$ ({\it{y\/}} $<$ (($1\;+$ {\it{a\/}}) $*$ ($1\;+$ {\it{a\/}})))) \\ 
$\rightarrow$$\;\;\;\;$({\it{a\/}} $=$ {\rm{rt}}\,({\it{y\/}})\index{rt})\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncons-lemma \\ \index{ncons-lemma}
{\rm{rt}}\,({\it{u\/}} $+$ (({\it{u\/}} $+$ {\it{v\/}}) $*$ ({\it{u\/}} $+$ {\it{v\/}})))\index{rt} $=$ ({\it{u\/}} $+$ {\it{v\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ncar}$\;\;$
{\rm{ncar}}\,({\it{x\/}})\index{ncar} $=$ ({\it{x\/}} $-$ ({\rm{rt}}\,({\it{x\/}})\index{rt} $*$ {\rm{rt}}\,({\it{x\/}})\index{rt}))
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ncdr}$\;\;$
{\rm{ncdr}}\,({\it{x\/}})\index{ncdr} $=$ ({\rm{rt}}\,({\it{x\/}})\index{rt} $-$ {\rm{ncar}}\,({\it{x\/}})\index{ncar})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ncons}$\;\;$
{\rm{ncons}}\,({\it{i\/}}, {\it{j\/}})\index{ncons} $=$ ({\it{i\/}} $+$ (({\it{i\/}} $+$ {\it{j\/}}) $*$ ({\it{i\/}} $+$ {\it{j\/}})))
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncar-ncons \\ \index{ncar-ncons}
({\it{i\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{ncar}}\,({\rm{ncons}}\,({\it{i\/}}, {\it{j\/}})\index{ncons})\index{ncar} $=$ {\it{i\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncdr-ncons \\ \index{ncdr-ncons}
({\it{j\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{ncdr}}\,({\rm{ncons}}\,({\it{i\/}}, {\it{j\/}})\index{ncons})\index{ncdr} $=$ {\it{j\/}})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ncadr}$\;\;$
{\rm{ncadr}}\,({\it{x\/}})\index{ncadr} $=$ {\rm{ncar}}\,({\rm{ncdr}}\,({\it{x\/}})\index{ncdr})\index{ncar}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{ncaddr}$\;\;$
{\rm{ncaddr}}\,({\it{x\/}})\index{ncaddr} $=$ {\rm{ncar}}\,({\rm{ncdr}}\,({\rm{ncdr}}\,({\it{x\/}})\index{ncdr})\index{ncdr})\index{ncar}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  rt-lessp \\ \index{rt-lessp}
(({\it{x\/}} $\not\simeq {\tt{0}}$) $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}})) $\rightarrow$ ({\rm{rt}}\,({\it{x\/}})\index{rt} $<$ {\it{x\/}})
\end{tabbing}

\begin{verbatim};   I'm sure the system could prove this without the hint, but it would use
;   induction and this is the obvious way to do it.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  rt-lesseqp \\ \index{rt-lesseqp}
{\it{x\/}} $\not<$ {\rm{rt}}\,({\it{x\/}})\index{rt}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  difference-0 \\ \index{difference-0}
({\it{x\/}} $<$ {\it{y\/}}) $\rightarrow$ (({\it{x\/}} $-$ {\it{y\/}}) $=$ {\tt{0}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  lessp-difference-1 \\ \index{lessp-difference-1}
\=\+(({\it{a\/}} $-$ {\it{b\/}}) $<$ {\it{c\/}}) \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{a\/}} $<$ {\it{b\/}}$\;\;${\bf then }{\tt{0}} $<$ {\it{c\/}} \\ 
{\bf else }{\it{a\/}} $<$ ({\it{b\/}} $+$ {\it{c\/}})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncar-lesseqp \\ \index{ncar-lesseqp}
{\it{x\/}} $\not<$ {\rm{ncar}}\,({\it{x\/}})\index{ncar}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  crock \\ \index{crock}
({\it{x\/}} $<$ ({\rm{rt}}\,({\it{x\/}})\index{rt} $-$ {\it{d\/}})) $=$ {\bf{f}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncdr-lesseqp \\ \index{ncdr-lesseqp}
{\it{x\/}} $\not<$ {\rm{ncdr}}\,({\it{x\/}})\index{ncdr}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  ncdr-lessp \\ \index{ncdr-lessp}
(({\it{fn\/}} $\in\;${\bf{N}}${}$) $\wedge$ ({\rm{ncar}}\,({\it{fn\/}})\index{ncar} $\not=$ {\tt{0}}) $\wedge$ ({\rm{ncar}}\,({\it{fn\/}})\index{ncar} $\not=$ {\tt{1}})) $\rightarrow$ ({\rm{ncdr}}\,({\it{fn\/}})\index{ncdr} $<$ {\it{fn\/}})
\end{tabbing}

\noindent{\sc Event}:   Disable ncar.

\addvspace{18pt}

\noindent{\sc Event}:   Disable ncdr.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{pr-apply} \\  
\=\+{\rm{pr-apply}}\,({\it{fn\/}}, {\it{arg\/}})\index{pr-apply} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{fn\/}} $\not\in\;${\bf{N}}${}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{0}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{1}}$\;\;${\bf then }{\it{arg\/}} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{2}}$\;\;${\bf then }$1\;+$ {\it{arg\/}} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{3}}$\;\;${\bf then }{\rm{rt}}\,({\it{arg\/}})\index{rt} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{4}} \\ 
{\bf then }\=\+{\bf if }{\it{arg\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{pr-apply}}\,({\rm{ncdr}}\,({\it{fn\/}})\index{ncdr}, {\rm{pr-apply}}\,({\it{fn\/}}, {\it{arg\/}} $-\;1$)\index{pr-apply})\index{pr-apply}$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{5}} \\ 
{\bf then }{\rm{pr-apply}}\,({\rm{ncadr}}\,({\it{fn\/}})\index{ncadr}, {\it{arg\/}})\index{pr-apply} $+$ {\rm{pr-apply}}\,({\rm{ncaddr}}\,({\it{fn\/}})\index{ncaddr}, {\it{arg\/}})\index{pr-apply} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{6}} \\ 
{\bf then }{\rm{pr-apply}}\,({\rm{ncadr}}\,({\it{fn\/}})\index{ncadr}, {\it{arg\/}})\index{pr-apply} $-$ {\rm{pr-apply}}\,({\rm{ncaddr}}\,({\it{fn\/}})\index{ncaddr}, {\it{arg\/}})\index{pr-apply} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{7}} \\ 
{\bf then }{\rm{pr-apply}}\,({\rm{ncadr}}\,({\it{fn\/}})\index{ncadr}, {\it{arg\/}})\index{pr-apply} $*$ {\rm{pr-apply}}\,({\rm{ncaddr}}\,({\it{fn\/}})\index{ncaddr}, {\it{arg\/}})\index{pr-apply} \\ 
{\bf elseif }{\rm{ncar}}\,({\it{fn\/}})\index{ncar} $=$ {\tt{8}} \\ 
{\bf then }{\rm{pr-apply}}\,({\rm{ncadr}}\,({\it{fn\/}})\index{ncadr}, {\rm{pr-apply}}\,({\rm{ncaddr}}\,({\it{fn\/}})\index{ncaddr}, {\it{arg\/}})\index{pr-apply})\index{pr-apply} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{non-pr-fn}$\;\;$
{\rm{non-pr-fn}}\,({\it{x\/}})\index{non-pr-fn} $=$ ($1\;+$ {\rm{pr-apply}}\,({\it{x\/}}, {\it{x\/}})\index{pr-apply})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{counter-example-for}$\;\;$
{\rm{counter-example-for}}\,({\it{x\/}})\index{counter-example-for} $=$ {\rm{fix}}\,({\it{x\/}})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  non-pr-functions-exist \\ \index{non-pr-functions-exist}
{\rm{non-pr-fn}}\,({\rm{counter-example-for}}\,({\it{fn\/}})\index{counter-example-for})\index{non-pr-fn} $\not=$ {\rm{pr-apply}}\,({\it{fn\/}}, {\rm{counter-example-for}}\,({\it{fn\/}})\index{counter-example-for})\index{pr-apply}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  counter-example-for-numeric \\ \index{counter-example-for-numeric}
{\rm{counter-example-for}}\,({\it{x\/}})\index{counter-example-for} $\in\;${\bf{N}}${}$
\end{tabbing}

\noindent{\sc Event}:   Disable pr-apply.

\addvspace{18pt}
\begin{tabbing}{\sc Definition}:\index{max2} \\  
\=\+{\rm{max2}}\,({\it{fn\/}}, {\it{i\/}})\index{max2} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{pr-apply}}\,({\it{fn\/}}, {\it{i\/}})\index{pr-apply} \\ 
{\bf else }{\rm{max}}\,({\rm{pr-apply}}\,({\it{fn\/}}, {\it{i\/}})\index{pr-apply}, {\rm{max2}}\,({\it{fn\/}}, {\it{i\/}} $-\;1$)\index{max2})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{max1} \\  
\=\+{\rm{max1}}\,({\it{fn\/}}, {\it{i\/}})\index{max1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{fn\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{max2}}\,({\it{fn\/}}, {\it{i\/}})\index{max2} \\ 
{\bf else }{\rm{max}}\,({\rm{max2}}\,({\it{fn\/}}, {\it{i\/}})\index{max2}, {\rm{max1}}\,({\it{fn\/}} $-\;1$, {\it{i\/}})\index{max1})$\;${\bf  endif}\-\-
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  max2-gte \\ \index{max2-gte}
{\rm{max2}}\,({\it{i\/}}, {\it{j\/}})\index{max2} $\not<$ {\rm{pr-apply}}\,({\it{i\/}}, {\it{j\/}})\index{pr-apply}
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{exceed}$\;\;$
{\rm{exceed}}\,({\it{j\/}})\index{exceed} $=$ ($1\;+$ {\rm{max1}}\,({\it{j\/}}, {\it{j\/}})\index{max1})
\end{tabbing}
\begin{tabbing}{\sc Definition}:\index{exceed-at}$\;\;$
{\rm{exceed-at}}\,({\it{i\/}})\index{exceed-at} $=$ {\it{i\/}}
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  max1-gte1 \\ \index{max1-gte1}
({\it{fn\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{max1}}\,({\it{j\/}} $+$ {\it{fn\/}}, {\it{i\/}})\index{max1} $\not<$ {\rm{pr-apply}}\,({\it{fn\/}}, {\it{i\/}})\index{pr-apply})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  max1-gte2 \\ \index{max1-gte2}
({\it{fn\/}} $\in\;${\bf{N}}${}$) $\rightarrow$ ({\rm{max1}}\,({\it{j\/}} $+$ {\it{fn\/}}, {\it{j\/}} $+$ {\it{fn\/}})\index{max1} $\not<$ {\rm{pr-apply}}\,({\it{fn\/}}, {\it{j\/}} $+$ {\it{fn\/}})\index{pr-apply})
\end{tabbing}
\begin{tabbing}{\sc Theorem}:  exceed-is-bigger \\ \index{exceed-is-bigger}
\=\+({\it{fn\/}} $\in\;${\bf{N}}${}$) \\ 
$\rightarrow$$\;\;\;\;$({\rm{pr-apply}}\,({\it{fn\/}}, {\it{j\/}} $+$ {\rm{exceed-at}}\,({\it{fn\/}})\index{exceed-at})\index{pr-apply} $<$ {\rm{exceed}}\,({\it{j\/}} $+$ {\rm{exceed-at}}\,({\it{fn\/}})\index{exceed-at})\index{exceed})\-
\end{tabbing}

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