\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};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; In an unpublished paper, Textbook Examples of Recursion, Donald E.
; Knuth of Stanford University gives the following generalization of
; McCarthy's 91 function:

; Let a be a real, let b and d be positive reals, and let c be a
; positive integer.

; Define K( x ) for integer inputs x by

;   K( x ) <== if  x > a  then  x - b
;                         else  K( ... K( x+d ) ... ).

; Here the else-clause in this definition has c applications of the
; function K.

; When a = 100, b = 10, c = 2, and d = 11, the definition specializes
; to McCarthy's original 91 function:

;   K( x ) <== if  x > 100  then  x - 10
;                           else  K( K( x+11 ) ).

; Knuth calls the first definition of K given above, the generalized 
; 91 recursion scheme with parameters ( a,b,c,d ).  

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

; The purpose of this file of Boyer-Moore-Kaufmann events is to 
; provide mechanical verification of the following theorem given by 
; Knuth in his paper.

; Theorem.  The generalized 91 recursion with parameters ( a,b,c,d )
;           defines a total function on the integers if and only if
;           (c-1)b < d.  In such a case the values of K( x ) also
;           satisfy the much simpler recurrence

;           K( x )  =  if  x > a  then  x - b
;                                 else  K( x+d-(c-1)b ).

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Use the library of integer facts.

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"integers"}}.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce a new function FN of one argument with
;  no constraints.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  fn-intro \\ \index{fn-intro}
{\bf{t}}
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it fn\/}.

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Recursively define what it means to 
; iterate applications of FN.

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

\begin{tabbing}{\sc Theorem}:  iter-fn=fn \\ \index{iter-fn=fn}
{\rm{iter-fn}}\,({\tt{1}}, {\it{x\/}})\index{iter-fn} $=$ {\rm{fn}}\,({\it{x\/}})\index{fn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iter-fn-sum \\ \index{iter-fn-sum}
{\rm{iter-fn}}\,({\it{i\/}}, {\rm{iter-fn}}\,({\it{j\/}}, {\it{x\/}})\index{iter-fn})\index{iter-fn} $=$ {\rm{iter-fn}}\,({\it{i\/}} $+$ {\it{j\/}}, {\it{x\/}})\index{iter-fn}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iter-fn-sum-integer \\ \index{iter-fn-sum-integer}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-fn}}\,({\it{i\/}}, {\rm{iter-fn}}\,({\it{j\/}}, {\it{x\/}})\index{iter-fn})\index{iter-fn} $=$ {\rm{iter-fn}}\,({\rm{iplus}}\,({\it{i\/}}, {\it{j\/}})\index{iplus}, {\it{x\/}})\index{iter-fn})\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce new constants (ie., functions with no arguments)
;  P, Q, R, and S with the indicated constaints

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  p-q-r-s-intro \\ \index{p-q-r-s-intro}
\=\+{\rm{integerp}}\,({\sc{p}}\index{p})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{q}}\index{q})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{r}}\index{r})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{s}}\index{s})\index{integerp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\sc{q}}\index{q}, {\tt{0}})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\sc{s}}\index{s})\index{ilessp})\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it p\/}, {\it q\/}, {\it r\/}, and {\it s\/}.

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define a "general Knuth" function, GK, of one argument
;  which will be used later to help witness the existence 
;  of functions which satisfy the defining recursion of
;  the generalized 91 function.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{k-measure} \\  
\=\+{\rm{k-measure}}\,({\it{a\/}}, {\it{x\/}})\index{k-measure} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\it{a\/}}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{iplus}}\,({\tt{1}}, {\rm{iplus}}\,({\it{a\/}}, {\rm{ineg}}\,({\it{x\/}})\index{ineg})\index{iplus})\index{iplus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k-measure-returns-numberp \\ \index{k-measure-returns-numberp}
{\rm{k-measure}}\,({\it{a\/}}, {\it{x\/}})\index{k-measure} $\in\;${\bf{N}}${}$
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k-measure-x+y$<$k-measure-y \\ \index{k-measure-x+y$<$k-measure-y}
\=\+(($\neg$ {\rm{ilessp}}\,({\it{a\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{k-measure}}\,({\it{a\/}}, {\rm{iplus}}\,({\it{x\/}}, {\it{y\/}})\index{iplus})\index{k-measure} $<$ {\rm{k-measure}}\,({\it{a\/}}, {\it{y\/}})\index{k-measure})\-
\end{tabbing}


\noindent{\sc Event}:   Disable k-measure.

\addvspace{18pt}

\begin{tabbing}{\sc Definition}:\index{gk} \\  
\=\+{\rm{gk}}\,({\it{x\/}})\index{gk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus} \\ 
{\bf elseif }{\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp}$\;\;${\bf then }{\rm{gk}}\,({\rm{iplus}}\,({\sc{r}}\index{r}, {\it{x\/}})\index{iplus})\index{gk} \\ 
{\bf else }{\sc{s}}\index{s}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{iter-gk} \\  
\=\+{\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{gk}}\,({\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\it{x\/}})\index{iter-gk})\index{gk}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iter-gk=gk \\ \index{iter-gk=gk}
{\rm{iter-gk}}\,({\tt{1}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{gk}}\,({\it{x\/}})\index{gk}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk-x=itergk-x+r \\ \index{itergk-x=itergk-x+r}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\sc{r}}\index{r}, {\it{x\/}})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  count\_x-1$<$count\_x \\ \index{count\_x-1$<$count\_x}
({\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp} $\wedge$ ({\it{x\/}} $\not=$ {\tt{1}})) $\rightarrow$ ({\rm{count}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{x\/}})\index{iplus}) $<$ {\rm{count}}\,({\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{induct-hint-pos-int} \\  
\=\+{\rm{induct-hint-pos-int}}\,({\it{x\/}})\index{induct-hint-pos-int} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\it{x\/}} $=$ {\tt{1}}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{induct-hint-pos-int}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{x\/}})\index{iplus})\index{induct-hint-pos-int}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n-1$>$0-when-n$>$0\&n$<$$>$1 \\ \index{n-1$>$0-when-n$>$0\&n$<$$>$1}
({\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} $\wedge$ ({\it{n\/}} $\not=$ {\tt{1}})) $\rightarrow$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$<$=z-when-x$<$y\&y$<$=z \\ \index{x$<$=z-when-x$<$y\&y$<$=z}
({\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{z\/}}, {\it{y\/}})\index{ilessp})) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{z\/}}, {\it{x\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x+\_n-1\_r$<$x+nr-when-0$<$r \\ \index{x+\_n-1\_r$<$x+nr-when-0$<$r}
\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{r\/}})\index{ilessp} \\ 
$\rightarrow$$\;\;\;\;${\rm{ilessp}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\it{r\/}})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\it{r\/}})\index{itimes})\index{iplus})\index{ilessp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  p+r$>$=x+\_n-1\_r-when-p+r$>$=x+nr \\ \index{p+r$>$=x+\_n-1\_r-when-p+r$>$=x!+nr}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=y-z-when-x+z$>$=y \\ \index{x$>$=y-z-when-x+z$>$=y}
($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{x\/}}, {\it{z\/}})\index{iplus}, {\it{y\/}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{iplus}}\,({\it{y\/}}, {\rm{ineg}}\,({\it{z\/}})\index{ineg})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk-x=itergk-x+nr-induction-step \\ \index{itergk-x=itergk-x+nr-induction-!step}
\=\+(\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+({\tt{0}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{iter-gk}))\- \\ 
$\wedge$$\;\;\;\;$({\tt{0}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\it{n\/}})\index{itimes})\index{iplus})\index{iter-gk}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk-x=itergk-x+nr \\ \index{itergk-x=itergk-x+nr}
\=\+(\=\+({\tt{0}} $<$ {\it{i\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{r}}\index{r})\index{itimes})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define the function N( a,d,x ) recursively, 
;  so that whenever d > 0, N( a,d,x ) is the smallest 
;  nonnegative integer i such that x + id > a.

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{n} \\  
\=\+{\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\it{x\/}})\index{n} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{ilessp}}\,({\tt{0}}, {\it{d\/}})\index{ilessp}$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\it{a\/}}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{iplus}}\,({\tt{1}}, {\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\rm{iplus}}\,({\it{x\/}}, {\it{d\/}})\index{iplus})\index{n})\index{iplus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n$>$=0 \\ \index{n$>$=0}
$\neg$ {\rm{ilessp}}\,({\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\it{x\/}})\index{n}, {\tt{0}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n$>$0-when-d$>$o\&x$<$=a \\ \index{n$>$0-when-d$>$o\&x$<$=a}
({\rm{ilessp}}\,({\tt{0}}, {\it{d\/}})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{a\/}}, {\it{x\/}})\index{ilessp})) $\rightarrow$ {\rm{ilessp}}\,({\tt{0}}, {\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\it{x\/}})\index{n})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a$<$x+nd \\ \index{a$<$x+nd}
{\rm{ilessp}}\,({\tt{0}}, {\it{d\/}})\index{ilessp} $\rightarrow$ {\rm{ilessp}}\,({\it{a\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\it{x\/}})\index{n}, {\it{d\/}})\index{itimes})\index{iplus})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a+d$>$=x+nd-when-d$>$0\&a$>$=x \\ \index{a+d$>$=x+nd-when-d$>$0\&a$>$=x}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{d\/}})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{a\/}}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{a\/}}, {\it{d\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\it{a\/}}, {\it{d\/}}, {\it{x\/}})\index{n}, {\it{d\/}})\index{itimes})\index{iplus})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q+nr-step-1 \\ \index{itergk\_i\_x=itergk\_i-1\_x-q+n!r-step-1}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q+nr-step-2 \\ \index{itergk\_i\_x=itergk\_i-1\_x-q+n!r-step-2}
\=\+({\tt{0}} $<$ {\it{i\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-gk}}\,({\it{i\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{iter-gk} \\ 
$=$$\;\;\;\;${\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{gk})\index{iter-gk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q+nr-step-3 \\ \index{itergk\_i\_x=itergk\_i-1\_x-q+n!r-step-3}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{gk})\index{iter-gk} \\ 
$=$$\;\;\;\;${\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{iplus})\index{iter-gk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q+nr \\ \index{itergk\_i\_x=itergk\_i-1\_x-q+n!r}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} \\ 
$=$$\;\;\;\;${\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{iplus})\index{iter-gk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=z-when-x$>$=y\&y$>$=z \\ \index{x$>$=z-when-x$>$=y\&y$>$=z}
(($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\it{z\/}})\index{ilessp})) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{z\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x+y$>$=x+-z+y-when-z$>$=0 \\ \index{x+y$>$=x+-z+y-when-z$>$=0}
($\neg$ {\rm{ilessp}}\,({\it{z\/}}, {\tt{0}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{x\/}}, {\it{y\/}})\index{iplus}, {\rm{iplus}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{z\/}})\index{ineg})\index{iplus}, {\it{y\/}})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i-1\_x-q=itergk\_i-1\_x-q+nr \\ \index{itergk\_i-1\_x-q=itergk\_i-1\_x!-q+nr}
\=\+(({\tt{1}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk} \\ 
$=$$\;\;\;\;${\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg}, {\rm{itimes}}\,({\sc{r}}\index{r}, {\rm{n}}\,({\sc{p}}\index{p}, {\sc{r}}\index{r}, {\it{x\/}})\index{n})\index{itimes})\index{iplus})\index{iplus})\index{iter-gk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q-when-p$>$=x\&r$>$0 \\ \index{itergk\_i\_x=itergk\_i-1\_x-q-w!hen-p$>$=x\&r$>$0}
\=\+(({\tt{1}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk=s-when-p$>$=x\&0$>$=r\&0$<$i \\ \index{itergk=s-when-p$>$=x\&0$>$=r\&0!$<$i}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\sc{s}}\index{s})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=x+-y-when-y$>$=0 \\ \index{x$>$=x+-y-when-y$>$=0}
($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\tt{0}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{y\/}})\index{ineg})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q-when-p$>$=x\&0$>$=r \\ \index{itergk\_i\_x=itergk\_i-1\_x-q-w!hen-p$>$=x\&0$>$=r}
\=\+(({\tt{1}} $<$ {\it{i\/}}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q-when-p$<$x \\ \index{itergk\_i\_x=itergk\_i-1\_x-q-w!hen-p$<$x}
\=\+(({\tt{0}} $<$ {\it{i\/}}) $\wedge$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q \\ \index{itergk\_i\_x=itergk\_i-1\_x-q}
({\tt{1}} $<$ {\it{i\/}}) $\rightarrow$ ({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\it{i\/}} $-\;1$, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-1\_x-q-integer \\ \index{itergk\_i\_x=itergk\_i-1\_x-q-i!nteger}
{\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\rightarrow$ ({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{iter-gk}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus})\index{iter-gk})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  one-one+y=y \\ \index{one-one+y=y}
{\rm{integerp}}\,({\it{y\/}})\index{integerp} $\rightarrow$ ({\rm{iplus}}\,({\tt{1}}, {\rm{iplus}}\,({\tt{-1}}, {\it{y\/}})\index{iplus})\index{iplus} $=$ {\it{y\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=itergk\_i-j\_x-jq \\ \index{itergk\_i\_x=itergk\_i-j\_x-jq}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\it{j\/}}, {\it{i\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} \\ 
$=$$\;\;\;\;${\rm{iter-gk}}\,({\rm{iplus}}\,({\it{i\/}}, {\rm{ineg}}\,({\it{j\/}})\index{ineg})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\it{j\/}}, {\sc{q}}\index{q})\index{itimes})\index{ineg})\index{iplus})\index{iter-gk})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=gk\_x-\_i-1\_q-when-i$>$1 \\ \index{itergk\_i\_x=gk\_x-\_i-1\_q-whe!n-i$>$1}
\=\+{\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\sc{q}}\index{q})\index{itimes})\index{ineg})\index{iplus})\index{gk})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x=1-or-x$>$1-when-x$>$0 \\ \index{x=1-or-x$>$1-when-x$>$0}
{\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp} $\rightarrow$ (({\it{x\/}} $=$ {\tt{1}}) $\vee$ {\rm{ilessp}}\,({\tt{1}}, {\it{x\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itergk\_i\_x=gk\_x-\_i-1\_q \\ \index{itergk\_i\_x=gk\_x-\_i-1\_q}
\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{i\/}})\index{ilessp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-gk}}\,({\it{i\/}}, {\it{x\/}})\index{iter-gk} $=$ {\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\sc{q}}\index{q})\index{itimes})\index{ineg})\index{iplus})\index{gk})\-
\end{tabbing}
 
\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Introduce new constants (ie., functions with no arguments)
;  A, B, C, and E with the indicated constaints.

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  a-b-c-d-intro \\ \index{a-b-c-d-intro}
\=\+{\rm{integerp}}\,({\sc{a}}\index{a})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{b}}\index{b})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{c}}\index{c})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{integerp}}\,({\sc{d}}\index{d})\index{integerp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{b}}\index{b})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\sc{d}}\index{d})\index{ilessp}\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it a\/}, {\it b\/}, {\it c\/}, and {\it d\/}.

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define two functions K and K1 which will be shown to satisfy
; the generalized 91 recursion scheme with parameters 
; ( (A),(B),(C),(D) ).

#| The following is the original version, which failed to be the
   correct lemma for the acceptance of the definition of K in Nqthm-1992.
   Following that is a new version.

(PROVE-LEMMA K-MEASURE-DECREASES-DEFN-K&K1
  (REWRITE)
  (IMPLIES
       (AND (NOT (ILESSP (A) X))
            (ILESSP 0
                    (IPLUS (D)
                           (IPLUS (INEG (ITIMES (B) (C)))
                                  (INEG (ITIMES (B) -1))))))
       (LESSP
        (K-MEASURE
                (A)
                (IPLUS (D)
                       (IPLUS (INEG (ITIMES (B) (C)))
                              (IPLUS (INEG (ITIMES (B) -1)) X))))
        (K-MEASURE (A) X)))
  ; hint
  ( (USE (K-MEASURE-X+Y<K-MEASURE-Y
	  (A (A))
	  (Y X)
	  (X (IPLUS (D)
		    (IPLUS (INEG (ITIMES (B) (C)))
			   (INEG (ITIMES (B) -1))))))) ))
|#

\end{verbatim}\begin{tabbing}{\sc Theorem}:  k-measure-decreases-defn-k\&k1 \\ \index{k-measure-decreases-defn-k\&k1}
\=\+(($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) $\wedge$ {\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\sc{c}}\index{c})\index{itimes}, {\rm{iplus}}\,({\sc{b}}\index{b}, {\sc{d}}\index{d})\index{iplus})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{k-measure}}\,({\sc{a}}\index{a}, {\rm{iplus}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{iplus}}\,({\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\sc{c}}\index{c})\index{itimes})\index{ineg}, {\it{x\/}})\index{iplus})\index{iplus})\index{iplus})\index{k-measure} \\ 
$<$$\;\;\;\;${\rm{k-measure}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{k-measure})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{k} \\  
\=\+{\rm{k}}\,({\it{x\/}})\index{k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf elseif }{\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{ilessp} \\ 
{\bf then }{\rm{k}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k} \\ 
{\bf else }{\sc{a}}\index{a}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{k1} \\  
\=\+{\rm{k1}}\,({\it{x\/}})\index{k1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf elseif }{\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{ilessp} \\ 
{\bf then }{\rm{k1}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k1} \\ 
{\bf else }{\rm{iplus}}\,({\sc{a}}\index{a}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{iter-k} \\  
\=\+{\rm{iter-k}}\,({\it{i\/}}, {\it{x\/}})\index{iter-k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{k}}\,({\rm{iter-k}}\,({\it{i\/}} $-\;1$, {\it{x\/}})\index{iter-k})\index{k}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{iter-k1} \\  
\=\+{\rm{iter-k1}}\,({\it{i\/}}, {\it{x\/}})\index{iter-k1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{k1}}\,({\rm{iter-k1}}\,({\it{i\/}} $-\;1$, {\it{x\/}})\index{iter-k1})\index{k1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=x \\ \index{x$>$=x}
$\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{x\/}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterk\_i\_x=k\_x-\_i-1\_b \\ \index{iterk\_i\_x=k\_x-\_i-1\_b}
{\rm{ilessp}}\,({\tt{0}}, {\it{i\/}})\index{ilessp} $\rightarrow$ ({\rm{iter-k}}\,({\it{i\/}}, {\it{x\/}})\index{iter-k} $=$ {\rm{k}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\sc{b}}\index{b})\index{itimes})\index{ineg})\index{iplus})\index{k})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=x-y-when-y$>$0 \\ \index{x$>$=x-y-when-y$>$0}
{\rm{ilessp}}\,({\tt{0}}, {\it{y\/}})\index{ilessp} $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{y\/}})\index{ineg})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterk1\_i\_x=k1\_x-\_i-1\_b \\ \index{iterk1\_i\_x=k1\_x-\_i-1\_b}
\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{i\/}})\index{ilessp} \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-k1}}\,({\it{i\/}}, {\it{x\/}})\index{iter-k1} $=$ {\rm{k1}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\sc{b}}\index{b})\index{itimes})\index{ineg})\index{iplus})\index{k1})\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The two functions K and K1 satisfy the generalized 91 
; recursion scheme with parameters ( (A),(B),(C),(D) ):

\end{verbatim}\begin{tabbing}{\sc Theorem}:  x$>$=y+z-when-x$>$=y\&0$>$=z \\ \index{x$>$=y+z-when-x$>$=y\&0$>$=z}
(($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\it{z\/}})\index{ilessp})) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{iplus}}\,({\it{y\/}}, {\it{z\/}})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  gk\_x+r=s-when-p$>$=x\&0$>$=r \\ \index{gk\_x+r=s-when-p$>$=x\&0$>$=r}
(($\neg$ {\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\sc{r}}\index{r})\index{ilessp})) $\rightarrow$ ({\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\sc{r}}\index{r})\index{iplus})\index{gk} $=$ {\sc{s}}\index{s})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k\_x+d-\_c-1\_b=a-when-a$>$=x\&0$>$=d-\_c-1\_b \\ \index{k\_x+d-\_c-1\_b=a-when-a$>$=x\&!0$>$=d-\_c-1\_b}
\=\+(($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{k}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k} $=$ {\sc{a}}\index{a})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k1\_x+d-\_c-1\_b=a-b-when-a$>$=x\&0$>$=d-\_c-1\_b \\ \index{k1\_x+d-\_c-1\_b=a-b-when-a$>$=!x\&0$>$=d-\_c-1\_b}
\=\+(($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{k1}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k1} \\ 
$=$$\;\;\;\;${\rm{iplus}}\,({\sc{a}}\index{a}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  itimes2--1 \\ \index{itimes2--1}
{\rm{itimes}}\,({\it{x\/}}, {\tt{-1}})\index{itimes} $=$ {\rm{ineg}}\,({\it{x\/}})\index{ineg}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k-satisfies-gen-91-recursion \\ \index{k-satisfies-gen-91-recursion}
\=\+{\rm{k}}\,({\it{x\/}})\index{k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{iter-k}}\,({\sc{c}}\index{c}, {\rm{iplus}}\,({\it{x\/}}, {\sc{d}}\index{d})\index{iplus})\index{iter-k}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k1-satisfies-gen-91-recursion \\ \index{k1-satisfies-gen-91-recursion}
\=\+{\rm{k1}}\,({\it{x\/}})\index{k1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{iter-k1}}\,({\sc{c}}\index{c}, {\rm{iplus}}\,({\it{x\/}}, {\sc{d}}\index{d})\index{iplus})\index{iter-k1}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; So now that it has been verified that the two functions 
; K and K1 satisfy the generalized 91 recursion scheme 
; with parameters ( (A),(B),(C),(D) ); we now verify that
; the two functions are not the same when 
; (D) <= (B)[(C)-1].

\end{verbatim}\begin{tabbing}{\sc Theorem}:  x-y$<$=0-when-x$<$=y \\ \index{x-y$<$=0-when-x$<$=y}
($\neg$ {\rm{ilessp}}\,({\it{y\/}}, {\it{x\/}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{y\/}})\index{ineg})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x-y$<$x-when-0$<$y \\ \index{x-y$<$x-when-0$<$y}
{\rm{ilessp}}\,({\tt{0}}, {\it{y\/}})\index{ilessp} $\rightarrow$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{y\/}})\index{ineg})\index{iplus}, {\it{x\/}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k\&k1-are-not-equal-functions \\ \index{k\&k1-are-not-equal-functions}
\=\+(($\neg$ {\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp}) $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{k}}\,({\it{x\/}})\index{k} $\not=$ {\rm{k1}}\,({\it{x\/}})\index{k1})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  k\&k1-are-not-equal-functions-version-2 \\ \index{k\&k1-are-not-equal-functions-ve!rsion-2}
($\neg$ {\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp}) $\rightarrow$ ({\rm{k}}\,({\sc{a}}\index{a})\index{k} $\not=$ {\rm{k1}}\,({\sc{a}}\index{a})\index{k1})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
; Introduce a new function G of one argument which 
; satisfies the simpler recurrence given in Knuth's 
; Theorem.

\end{verbatim}\begin{tabbing}{\sc Theorem}:  gk-version-of-simple-recursion \\ \index{gk-version-of-simple-recursion}
\=\+{\rm{gk}}\,({\it{x\/}})\index{gk} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{p}}\index{p}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{q}}\index{q})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{gk}}\,({\rm{iplus}}\,({\it{x\/}}, {\sc{r}}\index{r})\index{iplus})\index{gk}$\;${\bf  endif}\-\-
\end{tabbing}


\noindent{\sc Event}:   Disable k-satisfies-gen-91-recursion.

\addvspace{18pt}

\noindent{\sc Event}:   Disable k1-satisfies-gen-91-recursion.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  k-satisfies-simple-recursion \\ \index{k-satisfies-simple-recursion}
\=\+{\rm{k}}\,({\it{x\/}})\index{k} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{k}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Conservative Axiom}:  g-satisfies-simple-recursion \\ \index{g-satisfies-simple-recursion}
\=\+{\rm{g}}\,({\it{x\/}})\index{g} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{g}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\tt{-1}}, {\sc{c}}\index{c})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{g}$\;${\bf  endif}\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbol {\it g\/}.

\begin{tabbing}{\sc Theorem}:  g=x-b-when-a$<$x \\ \index{g=x-b-when-a$<$x}
{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp} $\rightarrow$ ({\rm{g}}\,({\it{x\/}})\index{g} $=$ {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})
\end{tabbing}


\noindent{\sc Event}:   Disable g-satisfies-simple-recursion.

\addvspace{18pt}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Verify that any function, such as G, which satisfies the
; simpler recurrence given in Knuth's Theorem, is in fact
; equal to K, provided (B)[(C) - 1] < (D):

\end{verbatim}\begin{tabbing}{\sc Theorem}:  x-y$>$0-when-y$<$x \\ \index{x-y$>$0-when-y$<$x}
{\rm{ilessp}}\,({\it{y\/}}, {\it{x\/}})\index{ilessp} $\rightarrow$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\it{y\/}})\index{ineg})\index{iplus})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  lessp-k-measure \\ \index{lessp-k-measure}
\=\+({\rm{ilessp}}\,({\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{itimes}}\,({\sc{b}}\index{b}, {\sc{c}}\index{c})\index{itimes})\index{iplus}, {\sc{d}}\index{d})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{k-measure}}\,({\sc{a}}\index{a}, {\rm{iplus}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{iplus}}\,({\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\sc{c}}\index{c})\index{itimes})\index{ineg}, {\it{x\/}})\index{iplus})\index{iplus})\index{iplus})\index{k-measure} \\ 
$<$$\;\;\;\;${\rm{k-measure}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{k-measure})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{k-induct-hint} \\  
\=\+{\rm{k-induct-hint}}\,({\it{x\/}})\index{k-induct-hint} \\ 
$=$$\;\;\;\;$\=\+{\bf if }$\neg$ {\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp}$\;\;${\bf then }{\bf{t}} \\ 
{\bf elseif }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{k-induct-hint}}\,({\rm{iplus}}\,(\=\+{\it{x\/}}, \\ 
{\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\-\index{iplus})\index{k-induct-hint}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g=k-when-b\_c-1\_$<$d-induction-step \\ \index{g=k-when-b\_c-1\_$<$d-induction!-step}
\=\+(\=\+{\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{g}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{g} \\ 
$=$$\;\;\;\;${\rm{k}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{k})\-)\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{g}}\,({\it{x\/}})\index{g} $=$ {\rm{k}}\,({\it{x\/}})\index{k})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  g=k-when-b\_c-1\_$<$d \\ \index{g=k-when-b\_c-1\_$<$d}
{\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp} $\rightarrow$ ({\rm{g}}\,({\it{x\/}})\index{g} $=$ {\rm{k}}\,({\it{x\/}})\index{k})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 
; Introduce a new function H of one argument which 
; satisfies the general 91 recursion with parameters
; ( (A),(B),(C),(D) ).

\end{verbatim}\begin{tabbing}{\sc Conservative Axiom}:  h-satisfies-gen-91-recursion \\ \index{h-satisfies-gen-91-recursion}
\=\+(\=\+{\rm{h}}\,({\it{x\/}})\index{h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{iter-h}}\,({\sc{c}}\index{c}, {\rm{iplus}}\,({\it{x\/}}, {\sc{d}}\index{d})\index{iplus})\index{iter-h}$\;${\bf  endif}\-)\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{i\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\it{x\/}} \\ 
{\bf else }{\rm{h}}\,({\rm{iter-h}}\,({\it{i\/}} $-\;1$, {\it{x\/}})\index{iter-h})\index{h}$\;${\bf  endif}\-)\-\-
\end{tabbing}\noindent Simultaneously, we introduce the new function symbols {\it h\/} and {\it iter-h\/}.

\begin{tabbing}{\sc Theorem}:  h=x-b-when-a$<$x \\ \index{h=x-b-when-a$<$x}
{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp} $\rightarrow$ ({\rm{h}}\,({\it{x\/}})\index{h} $=$ {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h=iterh-when-a$>$=x \\ \index{h=iterh-when-a$>$=x}
($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) $\rightarrow$ ({\rm{h}}\,({\it{x\/}})\index{h} $=$ {\rm{iter-h}}\,({\sc{c}}\index{c}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\it{x\/}})\index{iplus})\index{iter-h})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh=x-when-i-is-zerop \\ \index{iterh=x-when-i-is-zerop}
({\it{i\/}} $\simeq {\tt{0}}$) $\rightarrow$ ({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\it{x\/}})
\end{tabbing}


\noindent{\sc Event}:   Disable h-satisfies-gen-91-recursion.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  iterh=h-iter-h-when-not-zerop-i \\ \index{iterh=h-iter-h-when-not-zerop-i}
({\it{i\/}} $\not\simeq {\tt{0}}$) $\rightarrow$ ({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{h}}\,({\rm{iter-h}}\,({\it{i\/}} $-\;1$, {\it{x\/}})\index{iter-h})\index{h})
\end{tabbing}

\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; To prevent looping at least one of the following
; should be disabled:

\end{verbatim}
\noindent{\sc Event}:   Disable h=iterh-when-a$>$=x.

\addvspace{18pt}

\noindent{\sc Event}:   Disable iterh=h-iter-h-when-not-zerop-i.

\addvspace{18pt}

\begin{tabbing}{\sc Theorem}:  iter-h=h \\ \index{iter-h=h}
{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} $=$ {\rm{h}}\,({\it{x\/}})\index{h}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iter-h-sum \\ \index{iter-h-sum}
{\rm{iter-h}}\,({\it{i\/}}, {\rm{iter-h}}\,({\it{j\/}}, {\it{x\/}})\index{iter-h})\index{iter-h} $=$ {\rm{iter-h}}\,({\it{i\/}} $+$ {\it{j\/}}, {\it{x\/}})\index{iter-h}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iter-h-sum-integer \\ \index{iter-h-sum-integer}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{i\/}}, {\rm{iter-h}}\,({\it{j\/}}, {\it{x\/}})\index{iter-h})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\it{i\/}}, {\it{j\/}})\index{iplus}, {\it{x\/}})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h-satisfies-simple-rec-when-c=1 \\ \index{h-satisfies-simple-rec-when-c=1}
\=\+({\sc{c}}\index{c} $=$ {\tt{1}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{h}}\,({\it{x\/}})\index{h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{h}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  i-is-integer-when-1$<$i \\ \index{i-is-integer-when-1$<$i}
{\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\rightarrow$ {\rm{integerp}}\,({\it{i\/}})\index{integerp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1\_x-b-when-x$>$a \\ \index{iterh\_i\_x=iterh\_i-1\_x-b-whe!n-x$>$a}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a$>$=x-when-a+d$>$=d+x \\ \index{a$>$=x-when-a+d$>$=d+x}
($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{a\/}}, {\it{d\/}})\index{iplus}, {\rm{iplus}}\,({\it{d\/}}, {\it{x\/}})\index{iplus})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{a\/}}, {\it{x\/}})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_1+x\_y=iterh\_x\_h\_y \\ \index{iterh\_1+x\_y=iterh\_x\_h\_y}
{\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp} $\rightarrow$ ({\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\it{x\/}})\index{iplus}, {\it{y\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\it{x\/}}, {\rm{h}}\,({\it{y\/}})\index{h})\index{iter-h})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_x\_h\_y=iterh\_x+c-1\_x+d-when-x$>$0\&a$>$=y \\ \index{iterh\_x\_h\_y=iterh\_x+c-1\_x+!d-when-x$>$0\&a$>$=y}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{y\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{x\/}}, {\rm{h}}\,({\it{y\/}})\index{h})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\sc{c}}\index{c}, {\it{x\/}})\index{iplus}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\it{y\/}})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_1\_x=iterh\_1+n\_c-1\_x+nd-induction-step-part-1 \\ \index{iterh\_1\_x=iterh\_1+n\_c-1\_x+!nd-induction-step-part-1}
\=\+(\=\+{\rm{ilessp}}\,({\tt{0}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  n-1*c-1$>$0 \\ \index{n-1*c-1$>$0}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} $\wedge$ ({\it{n\/}} $\not=$ {\tt{1}}) $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ilessp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a$>$=x+\_n-1\_d-when-a+d$>$=x+dn \\ \index{a$>$=x+\_n-1\_d-when-a+d$>$=x+d!n}
\=\+($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{a\/}}, {\it{d\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{d\/}}, {\it{n\/}})\index{itimes})\index{iplus})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\it{a\/}}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\it{d\/}})\index{itimes})\index{iplus})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_1\_x=iterh\_1+n\_c-1\_x+nd-induction-step-part-2 \\ \index{iterh\_1\_x=iterh\_1+n\_c-1\_x+!nd-induction-step-part-2}
\=\+(\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}) \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h})\-)\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  a+d$>$=x+\_n-1\_d-when-a+d$>$=x+dn \\ \index{a+d$>$=x+\_n-1\_d-when-a+d$>$=x!+dn}
\=\+({\rm{ilessp}}\,({\tt{0}}, {\it{d\/}})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{a\/}}, {\it{d\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{d\/}}, {\it{n\/}})\index{itimes})\index{iplus})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\it{a\/}}, {\it{d\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\it{d\/}})\index{itimes})\index{iplus})\index{ilessp})\-
\end{tabbing}  

\begin{tabbing}{\sc Theorem}:  iterh\_1\_x=iterh\_1+n\_c-1\_x+nd-induction-step \\ \index{iterh\_1\_x=iterh\_1+n\_c-1\_x+!nd-induction-step}
\=\+(\=\+{\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$({\it{n\/}} $\not=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;$(\=\+(\=\+{\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{n\/}})\index{iplus}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h})\-)\- \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_1\_x=iterh\_1+n\_c-1\_x+nd-base-step \\ \index{iterh\_1\_x=iterh\_1+n\_c-1\_x+!nd-base-step}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\it{x\/}})\index{iplus})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\sc{c}}\index{c}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\it{x\/}})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_1\_x=iterh\_1+n\_c-1\_x+nd \\ \index{iterh\_1\_x=iterh\_1+n\_c-1\_x+!nd}
\=\+(\=\+{\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i+n\_c-1\_x+nd-step-1 \\ \index{iterh\_i\_x=iterh\_i+n\_c-1\_x+!nd-step-1}
{\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\rightarrow$ ({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h})\index{iter-h})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i+n\_c-1\_x+nd-step-2 \\ \index{iterh\_i\_x=iterh\_i+n\_c-1\_x+!nd-step-2}
\=\+(\=\+{\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iter-h}}\,({\tt{1}}, {\it{x\/}})\index{iter-h})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, \\ 
{\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  cn-n$>$=0-when-1$<$c\&0$<$n \\ \index{cn-n$>$=0-when-1$<$c\&0$<$n}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{c\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\rm{ineg}}\,({\it{n\/}})\index{ineg}, {\rm{itimes}}\,({\it{c\/}}, {\it{n\/}})\index{itimes})\index{iplus}, {\tt{0}})\index{ilessp})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i+n\_c-1\_x+nd-step-3 \\ \index{iterh\_i\_x=iterh\_i+n\_c-1\_x+!nd-step-3}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, \\ 
{\rm{iter-h}}\,({\rm{iplus}}\,({\tt{1}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i+n\_c-1\_x+nd \\ \index{iterh\_i\_x=iterh\_i+n\_c-1\_x+!nd}
\=\+(\=\+{\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\wedge$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{ilessp}}\,({\rm{iplus}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{ilessp}))\- \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,({\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\it{n\/}}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1+n\_c-1\_x+nd-b-step-1 \\ \index{iterh\_i\_x=iterh\_i-1+n\_c-1\_!x+nd-b-step-1}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  i+n\_c-1\_-1$>$0 \\ \index{i+n\_c-1\_-1$>$0}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\it{c\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{n\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;${\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\it{n\/}}, {\rm{iplus}}\,({\it{c\/}}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus})\index{ilessp}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1+n\_c-1\_x+nd-b-step-2 \\ \index{iterh\_i\_x=iterh\_i-1+n\_c-1\_!x+nd-b-step-2}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus}, \\ 
{\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\-\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{h})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1+n\_c-1\_x+nd-b-step-3 \\ \index{iterh\_i\_x=iterh\_i-1+n\_c-1\_!x+nd-b-step-3}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{h})\-\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1+n\_c-1\_x+nd-b \\ \index{iterh\_i\_x=iterh\_i-1+n\_c-1\_!x+nd-b}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x$>$=y-z-when-x$>$=y\&0$<$z \\ \index{x$>$=y-z-when-x$>$=y\&0$<$z}
(($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\it{y\/}})\index{ilessp}) $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{z\/}})\index{ilessp}) $\rightarrow$ ($\neg$ {\rm{ilessp}}\,({\it{x\/}}, {\rm{iplus}}\,({\it{y\/}}, {\rm{ineg}}\,({\it{z\/}})\index{ineg})\index{iplus})\index{ilessp})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x+2-1=1+x \\ \index{x+2-1=1+x}
{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\tt{2}}, {\it{x\/}})\index{iplus})\index{iplus} $=$ {\rm{iplus}}\,({\tt{1}}, {\it{x\/}})\index{iplus}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i-1\_x-b=iterh\_i-1+n\_c-1\_x+nd-b-when-i=2 \\ \index{iterh\_i-1\_x-b=iterh\_i-1+n\_c!-1\_x+nd-b-when-i=2}
\=\+(({\it{i\/}} $=$ {\tt{2}}) $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  i-1$>$1-when-i$<$$>$2\&1$<$i \\ \index{i-1$>$1-when-i$<$$>$2\&1$<$i}
(({\it{i\/}} $\not=$ {\tt{2}}) $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp}) $\rightarrow$ {\rm{ilessp}}\,({\tt{1}}, {\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i-1\_x-b=iterh\_i-1+n\_c-1\_x+nd-b-when-i$>$2 \\ \index{iterh\_i-1\_x-b=iterh\_i-1+n\_c!-1\_x+nd-b-when-i$>$2}
\=\+(({\it{i\/}} $\not=$ {\tt{2}}) $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i-1\_x-b=iterh\_i-1+n\_c-1\_x+nd-b \\ \index{iterh\_i-1\_x-b=iterh\_i-1+n\_c!-1\_x+nd-b}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h} \\ 
$=$$\;\;\;\;${\rm{iter-h}}\,(\=\+{\rm{iplus}}\,({\tt{-1}}, {\rm{iplus}}\,({\it{i\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{iplus})\index{iplus}, \\ 
{\rm{iplus}}\,({\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg}, {\rm{iplus}}\,({\it{x\/}}, {\rm{itimes}}\,({\rm{n}}\,({\sc{a}}\index{a}, {\sc{d}}\index{d}, {\it{x\/}})\index{n}, {\sc{d}}\index{d})\index{itimes})\index{iplus})\index{iplus})\-\index{iter-h})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1\_i-b-when-a$>$=x \\ \index{iterh\_i\_x=iterh\_i-1\_i-b-whe!n-a$>$=x}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-1\_i-b \\ \index{iterh\_i\_x=iterh\_i-1\_i-b}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\tt{-1}}, {\it{i\/}})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  x*1=x-when-0$<$x \\ \index{x*1=x-when-0$<$x}
{\rm{ilessp}}\,({\tt{0}}, {\it{x\/}})\index{ilessp} $\rightarrow$ ({\rm{itimes}}\,({\it{x\/}}, {\tt{1}})\index{itimes} $=$ {\it{x\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_i\_x=iterh\_i-j\_i-jb \\ \index{iterh\_i\_x=iterh\_i-j\_i-jb}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\it{i\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\tt{0}}, {\it{j\/}})\index{ilessp} $\wedge$ {\rm{ilessp}}\,({\it{j\/}}, {\it{i\/}})\index{ilessp}) \\ 
$\rightarrow$$\;\;\;\;$({\rm{iter-h}}\,({\it{i\/}}, {\it{x\/}})\index{iter-h} $=$ {\rm{iter-h}}\,({\rm{iplus}}\,({\it{i\/}}, {\rm{ineg}}\,({\it{j\/}})\index{ineg})\index{iplus}, {\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\it{j\/}})\index{itimes})\index{ineg})\index{iplus})\index{iter-h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  c-1$>$0-when-c$>$1 \\ \index{c-1$>$0-when-c$>$1}
{\rm{ilessp}}\,({\tt{1}}, {\it{c\/}})\index{ilessp} $\rightarrow$ {\rm{ilessp}}\,({\tt{0}}, {\rm{iplus}}\,({\it{c\/}}, {\tt{-1}})\index{iplus})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  c-1$<$c \\ \index{c-1$<$c}
{\rm{ilessp}}\,({\rm{iplus}}\,({\it{c\/}}, {\tt{-1}})\index{iplus}, {\it{c\/}})\index{ilessp}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  iterh\_c\_x=h\_x-\_c-1\_b \\ \index{iterh\_c\_x=h\_x-\_c-1\_b}
{\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\rightarrow$ ({\rm{iter-h}}\,({\sc{c}}\index{c}, {\it{x\/}})\index{iter-h} $=$ {\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{h})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h\_x=h\_x+d-\_c-1\_b \\ \index{h\_x=h\_x+d-\_c-1\_b}
\=\+({\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} $\wedge$ ($\neg$ {\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{h}}\,({\it{x\/}})\index{h} $=$ {\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{h})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h-satisfies-simple-rec-when-c$>$1 \\ \index{h-satisfies-simple-rec-when-c$>$!1}
\=\+{\rm{ilessp}}\,({\tt{1}}, {\sc{c}}\index{c})\index{ilessp} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{h}}\,({\it{x\/}})\index{h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{h}$\;${\bf  endif}\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h-satisfies-simple-rec \\ \index{h-satisfies-simple-rec}
\=\+{\rm{h}}\,({\it{x\/}})\index{h} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{ilessp}}\,({\sc{a}}\index{a}, {\it{x\/}})\index{ilessp}$\;\;${\bf then }{\rm{iplus}}\,({\it{x\/}}, {\rm{ineg}}\,({\sc{b}}\index{b})\index{ineg})\index{iplus} \\ 
{\bf else }{\rm{h}}\,({\rm{iplus}}\,({\it{x\/}}, {\rm{iplus}}\,({\sc{d}}\index{d}, {\rm{ineg}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes})\index{ineg})\index{iplus})\index{iplus})\index{h}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  h=k-when-b\_c-1\_$<$d \\ \index{h=k-when-b\_c-1\_$<$d}
{\rm{ilessp}}\,({\rm{itimes}}\,({\sc{b}}\index{b}, {\rm{iplus}}\,({\sc{c}}\index{c}, {\tt{-1}})\index{iplus})\index{itimes}, {\sc{d}}\index{d})\index{ilessp} $\rightarrow$ ({\rm{h}}\,({\it{x\/}})\index{h} $=$ {\rm{k}}\,({\it{x\/}})\index{k})
\end{tabbing}

\begin{verbatim};;;;;;;;;;MAKE-LIB IS HERE;;;;;;;;;;;;;;;;

;;;;;;;;;;;;;;;I am here;;;;;;;;;;;;
; (MAKE-LIB "knuth-91a")
; (MAKE-LIB-CONDITIONAL "knuth-91a" T T)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
\end{verbatim}
%\end{list}
\printindex
\end{document}
