\batchmode
\documentstyle[twoside]{article}
\makeatletter
\input epsf

\newcommand{\w}[3]{\mbox{\wf{#1 \wh{#2} #3}}}
\newcommand{\wf}[1]{\mbox{\fbox{$#1$}}}
\newcommand{\wfout}[1]{\fbox{$#1$}}
\newcommand{\wfin}[1]{\fbox{$#1$}}
\newcommand{\wh}[1]{\mbox{$\underline{#1}$}}
\newcommand{\sink}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\eqref}[1]{(\ref{#1})}
\newcommand{\app}[2]{#1 \mbox{$\! \mbox{@} \!$} #2}
\newcommand{\cons}[2]{#1 \mbox{$\! :: \!$} #2}
\newcommand{\consnil}[1]{[#1]}
\newcommand{\nil}{[]}
\newcommand{\appd}[2]{app(#1,#2)}
\newcommand{\consd}[2]{cons(#1,#2)}
\newcommand{\consdnil}[1]{\consd{#1}{\nild}}
\newcommand{\len}{\mbox{\it len}}
\newcommand{\rev}{\mbox{\it rev}}
\newcommand{\qrev}{\mbox{\it qrev}}
\newcommand{\xxx}{\mbox{\it x}}
\newcommand{\yyy}{\mbox{\it y}}
\newcommand{\zzz}{\mbox{\it z}}
\newcommand{\uuu}{\mbox{\it u}}
\newcommand{\vvv}{\mbox{\it v}}
\newcommand{\www}{\mbox{\it w}}
\newcommand{\aaa}{\mbox{\it a}}
\newcommand{\bbb}{\mbox{\it b}}
\newcommand{\ccc}{\mbox{\it c}}
\newcommand{\ddd}{\mbox{\it d}}
\newcommand{\eee}{\mbox{\it e}}
\newcommand{\fff}{\mbox{\it f}}
\newcommand{\ggg}{\mbox{\it g}}
\newcommand{\hhh}{\mbox{\it h}}
\newcommand{\lll}{\mbox{\it l}}
\newcommand{\nnn}{\mbox{\it n}}
\newcommand{\ttt}{\mbox{\it t}}
\newcommand{\sss}{\mbox{\it s}}
\newcommand{\rrr}{\mbox{\it r}}
\newcommand{\XXX}{\mbox{\it X}}
\newcommand{\YYY}{\mbox{\it Y}}
\newcommand{\ZZZ}{\mbox{\it Z}}
\newcommand{\UUU}{\mbox{\it U}}
\newcommand{\VVV}{\mbox{\it V}}
\newcommand{\WWW}{\mbox{\it W}}
\newcommand{\AAA}{\mbox{\it A}}
\newcommand{\BBB}{\mbox{\it B}}
\newcommand{\CCC}{\mbox{\it C}}
\newcommand{\DDD}{\mbox{\it D}}
\newcommand{\EEE}{\mbox{\it E}}
\newcommand{\FFF}{\mbox{\it F}}
\newcommand{\GGG}{\mbox{\it G}}
\newcommand{\HHH}{\mbox{\it H}}
\newcommand{\LLL}{\mbox{\it L}}
\newcommand{\NNN}{\mbox{\it N}}
\newcommand{\TTT}{\mbox{\it T}}
\newcommand{\SSS}{\mbox{\it S}}
\newcommand{\RRR}{\mbox{\it R}}
\newcommand{\sorted}{\mbox{\it sorted}}
\newcommand{\isort}{\mbox{\it isort}}
\newcommand{\insertd}{\mbox{\it insert}}
\newcommand{\rot}{\mbox{\it rot}}
\newcommand{\half}{\mbox{\it half}}

\makeatother
\newenvironment{tex2html_wrap}{}{}
\setlength{\textheight}{10in}\begin{document}
\pagestyle{empty}
\stepcounter{section}
\newpage

{\samepage \clearpage \begin{eqnarray*}\forall n \ . \ dbl(n) & = & n+n.
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}X + 0 & = &  X \\ 
X + s(Y) & = & s(X+Y) \\ 
dbl(0) & = & 0 \\ 
dbl(s(X)) & = & s(s(dbl(X))) 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $s(X)$
}


\newpage

{\samepage \clearpage $X$
}


\newpage

{\samepage \clearpage $X+1$
}


\newpage

{\samepage \clearpage $Y$
}


\newpage

{\samepage \clearpage $x$
}


\newpage

{\samepage \clearpage $$ dbl(x) = x + x $$
}


\newpage

{\samepage \clearpage $$ dbl(s(x))  = s(x)+s(x). $$
}


\newpage

{\samepage \clearpage $dbl$
}


\newpage

{\samepage \clearpage $$ s(s(dbl(x))) = s(s(x) + x). $$
}


\newpage

{\samepage \clearpage $$ s(dbl(x)) = s(x) + x. $$
}


\newpage

{\samepage \clearpage $$ s(x+x) = s(x) + x. $$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}s(x + x) & = & s(x)+x \\ 
s(s(x + x)) & = & s(s(x))+x \\ 
s(s(s(x + x))) & = & s(s(s(x)))+x \\ 
s(s(s(s(x + x)))) & = & s(s(s(s(x))))+x \\ 
s(s(s(s(s(x + x))))) & = & s(s(s(s(s(x)))))+x \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$s(X) + Y = s(X+Y).$$
}


\newpage

{\samepage \clearpage $$\forall x,y \ . \ s(x) + y = s(x+y).$$
}


\newpage

{\samepage \clearpage $y$
}


\stepcounter{section}
\newpage

{\samepage \clearpage \[ dbl(x) = x + x \]
}


\newpage

{\samepage \clearpage \[ dbl(s(x)) = s(x) + s(x). \]
}


\newpage

{\samepage \clearpage \[ dbl(\mbox{\fbox{$s(\mbox{$\underline{x}$})$}}) = \mbox{\fbox{$s(\mbox{$\underline{x}$})$}} + \mbox{\fbox{$s(\mbox{$\underline{x}$})$}}. \]
}


\newpage

{\samepage \clearpage $\mbox{\fbox{$s(s(\mbox{$\underline{x}$}))$}}$
}


\newpage

{\samepage \clearpage $\mbox{\fbox{$s(\mbox{$\underline{\mbox{\fbox{$s(\mbox{$\underline{x}$})$}}}$})$}}$
}


\newpage

{\samepage \clearpage $r$
}


\newpage

{\samepage \clearpage $s$
}


\newpage

{\samepage \clearpage $t$
}


\newpage

{\samepage \clearpage $\sigma$
}


\newpage

{\samepage \clearpage $\sigma(skeleton(r)) = t$
}


\newpage

{\samepage \clearpage $erase(r)=s$
}


\newpage

{\samepage \clearpage $skeleton(r)$
}


\newpage

{\samepage \clearpage $erase(r)$
}


\newpage

{\samepage \clearpage $\mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}$
}


\newpage

{\samepage \clearpage $s(\mbox{\fbox{$s(\mbox{$\underline{x}$})$}})$
}


\newpage

{\samepage \clearpage $s(s(x))$
}


\newpage

{\samepage \clearpage $s(x)$
}


\newpage

{\samepage \clearpage \begin{eqnarray}dbl(\mbox{\fbox{$s(\mbox{$\underline{X}$})$}}) & = & \fbox{$s(s(\mbox{$\underline{dbl(X)}$}))$} \label{dbl-rule} \\ 
X+\fbox{$s(\mbox{$\underline{Y}$})$} &=& \fbox{$s(\mbox{$\underline{X +Y}$})$} \label{plus2-rule} \\ 
\fbox{$s(\mbox{$\underline{X}$})$}+Y &=& \fbox{$s(\mbox{$\underline{X +Y}$})$} \label{plus1-rule} 
\end{eqnarray}
}


\newpage

{\samepage \clearpage \[ \mbox{\fbox{$s(s(\mbox{$\underline{dbl(x)}$}))$}} = \mbox{\fbox{$s(\mbox{$\underline{x}$})$}} + \mbox{\fbox{$s(\mbox{$\underline{x}$})$}}. \]
}


\newpage

{\samepage \clearpage \[ \mbox{\fbox{$s(s(\mbox{$\underline{dbl(x)}$}))$}} = \mbox{\fbox{$s(\mbox{$\underline{\mbox{\fbox{$s(\mbox{$\underline{x}$})$}} + x}$})$}}. \]
}


\newpage

{\samepage \clearpage \[ \mbox{\fbox{$s(s(\mbox{$\underline{dbl(x)}$}))$}} = \mbox{\fbox{$s(s(\mbox{$\underline{x + x}$}))$}}. \]
}


\newpage

{\samepage \clearpage \[ \mbox{\fbox{$s(s(\mbox{$\underline{x+x}$}))$}} = \mbox{\fbox{$s(s(\mbox{$\underline{x + x}$}))$}}. \]
}


\stepcounter{section}
\newpage

{\samepage \clearpage \begin{eqnarray*}s(x + x) & = & s(x)+x \\ 
s(s(x + x)) & = & s(s(x))+x \\ 
s(s(s(x + x))) & = & s(s(s(x)))+x \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}s(x + x) & = & s(x)+x \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(x + x)}$})$}} & = & \mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}+x \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(s(x + x))}$})$}} & = & \mbox{\fbox{$s(\mbox{$\underline{s(s(x))}$})$}}+x \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ 
\mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y = \mbox{\fbox{$s(\mbox{$\underline{X+Y}$})$}}.  $$
}


\newpage

{\samepage \clearpage \begin{figure}% latex2html id marker 219
[htb]
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

\begin{enumerate}
\item There is a sequence of equations $s_i=t_i$ which
the prover attempts to prove by induction ($i$ = 0, 1 ...);
\item There exists (non trivial) $G, H$ such 
that for each $j$, the maximal difference match has
$s_{j}$ = $G(U_j)$, and $s_{j+1}=G(\mbox{\fbox{$H(\mbox{$\underline{U_j}$})$}})$.
\end{enumerate}
}
\end{minipage}
}
\caption{Preconditions to the divergence critic}
\end{center}
\end{figure}
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, .\, \mbox{\it z} $
}


\newpage

{\samepage \clearpage $H$
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, .\, s(\mbox{\it z})$
}


\newpage

{\samepage \clearpage $G$
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, . \, \mbox{\it z} + x$
}


\newpage

{\samepage \clearpage $U_0$
}


\stepcounter{section}
\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y = \mbox{\fbox{$F(\mbox{$\underline{X+Y}$})$}} $$
}


\newpage

{\samepage \clearpage $F$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}s(x + x) & = & s(x)+x \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(x + x)}$})$}} & = & \mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}+x \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(s(x + x))}$})$}} & = & \mbox{\fbox{$s(\mbox{$\underline{s(s(x))}$})$}}+x \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, . \, \mbox{\it s}(\mbox{\it z})$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y = \mbox{\fbox{$s(\mbox{$\underline{X+Y}$})$}} . $$
}


\newpage

{\samepage \clearpage $$ \forall l \ . \  \mbox{\it sorted}(\mbox{\it isort}(l)) = true $$
}


\newpage

{\samepage \clearpage $\sorted$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}sorted(nil) & = & true \\ 
sorted(cons(X,nil)) & = & true \\ 
X<Y \rightarrow sorted(cons(X,cons(Y,Z))) & = & sorted(cons(Y,Z)) \\ 
isort(nil)& = & nil \\ 
isort(cons(X,Y)) & = & insert(X,isort(Y))
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $insert(X,Z)$
}


\newpage

{\samepage \clearpage $Z$
}


\newpage

{\samepage \clearpage $X<Y$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}0<X & = & true \\ 
s(X)<0 & = & false \\ 
s(X)<s(Y) & = & X<Y \\ 
insert(X,nil) & = & cons(X,nil) \\ 
X<Y \rightarrow insert(X,cons(Y,Z)) & = & cons(X,cons(Y,Z)) \\ 
\neg(X<Y) \rightarrow insert(X,cons(Y,Z)) & = & cons(Y,insert(X,Z)) \\ 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ \mbox{\it sorted}(\mbox{\fbox{$\mbox{\it insert}(\mbox{\it Y},\mbox{$\underline{\mbox{\it X}}$})$}}) =  \mbox{\fbox{$F(\mbox{$\underline{\mbox{\it sorted}(\mbox{\it X})}$}$}} . $$
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, .\, \zzz$
}


\newpage

{\samepage \clearpage $$ \mbox{\it sorted}(\mbox{\fbox{$\mbox{\it insert}(\mbox{\it Y},\mbox{$\underline{\mbox{\it X}}$})$}}) =  \mbox{\it sorted}(\mbox{\it X}). $$
}


\newpage

{\samepage \clearpage $$ \forall i, j, l \ . \ nth(i,nth(j,l)) = nth(j,nth(i,l)) $$
}


\newpage

{\samepage \clearpage $nth$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}nth(0,L) & = & L \\ 
nth(N,nil) & = & nil \\ 
nth(s(N),cons(H,T)) & = & nth(N,T).
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}nth(s(i),nth(j,x)) & = & nth(s(j),nth(i,x)) \\ 
nth(s(s(i)),nth(j,cons(y,x))) & = & nth(s(j),nth(i,x)) \\ 
nth(s(s(s(i))),nth(j,cons(z,cons(y,x)))) & = & nth(s(j),nth(i,x)) \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}nth(s(i),nth(j,x)) & = & nth(s(j),nth(i,x)) \\ 
nth(\mbox{\fbox{$s(\mbox{$\underline{s(i)}$})$}},nth(j,\mbox{\fbox{$cons(y,\mbox{$\underline{x}$})$}})) & = & nth(s(j),nth(i,x)) \\ 
nth(\mbox{\fbox{$s(\mbox{$\underline{s(s(i))}$})$}},nth(j,\mbox{\fbox{$cons(z,\mbox{$\underline{cons(y,x)}$})$}})) & = & nth(s(j),nth(i,x)) \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ nth(\mbox{\fbox{$s(\mbox{$\underline{I}$})$}},nth(J,\mbox{\fbox{$cons(Y,\mbox{$\underline{X}$})$}})) = 
\mbox{\fbox{$F(\mbox{$\underline{nth(I,nth(J,X))}$})$}}. $$
}


\newpage

{\samepage \clearpage $\lambda \mbox{\it z} \, .\, \zzz$
}


\newpage

{\samepage \clearpage $$ nth(\mbox{\fbox{$s(\mbox{$\underline{I}$})$}},nth(J,\mbox{\fbox{$cons(Y,\mbox{$\underline{X}$})$}})) = 
nth(I,nth(J,X)). $$
}


\newpage

{\samepage \clearpage \begin{figure}% latex2html id marker 278
[htb]
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

\begin{enumerate}
\item The critic proposes a rule of the
form,
\begin{eqnarray*}
G(\mbox{\fbox{$H(\mbox{$\underline{U_0}$})$}}) & = & \mbox{\fbox{$F\mbox{$\underline{(G(U_0)}$})$}}
\end{eqnarray*}
\item $F$ is instantiated by the cancellation
or petering out heuristics;
\item Lemmas are filtered through a type checker and a conjecture
disprover;
\item If several lemmas are suggested, 
the critic deletes any that are subsumed.
\end{enumerate}
}
\end{minipage}
}
\caption{Postconditions to the divergence critic}
\end{center}
\end{figure}
}


\newpage

{\samepage \clearpage $nth(i,nth(j,l))=nth(j,nth(i,l))$
}


\stepcounter{section}
\newpage

{\samepage \clearpage $$ \forall \mbox{\it a} , \mbox{\it b} \ . \ \mbox{\it len}(\mbox{\it a})+\mbox{\it len}(\mbox{\it b}) = \mbox{\it len}(app(\mbox{\it a},\mbox{\it b})) $$
}


\newpage

{\samepage \clearpage $len$
}


\newpage

{\samepage \clearpage $app$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it len}(nil) & = & 0\\ 
\mbox{\it len}(cons(\mbox{\it H},\mbox{\it T})) & = & \mbox{\it s}(\mbox{\it len}(\mbox{\it T})) \\ 
app(nil,\mbox{\it T}) & = & \mbox{\it T} \\ 
app(cons(\mbox{\it H},\mbox{\it T}),\mbox{\it R}) & = & cons(\mbox{\it H},app(\mbox{\it T},\mbox{\it R})).
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}0+len(b) & = & len(b) \\ 
s(0)+len(b) & = & s(len(b)) \\ 
s(s(0))+len(b) & = & s(s(len(b))) \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}0+len(b) & = & len(b) \\ 
\mbox{\fbox{$s(\mbox{$\underline{0}$})$}}+len(b) & = & \mbox{\fbox{$s(\mbox{$\underline{len(b)}$})$}} \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(0)}$})$}}+len(b) & = & \mbox{\fbox{$s(\mbox{$\underline{s(len(b))}$})$}} \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$\mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{0}$})$}}+\mbox{\it len}(\mbox{\it B})  =
\mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{0+\mbox{\it len}(\mbox{\it B})}$})$}}. $$
}


\newpage

{\samepage \clearpage $\{ s(0)+\mbox{\it len}(\mbox{\it B}), \mbox{\it len}(\mbox{\it B}), \mbox{\it B}\}$
}


\newpage

{\samepage \clearpage $\{ s(0+\mbox{\it len}(\mbox{\it B})), 0+\mbox{\it len}(\mbox{\it B}),\mbox{\it len}(\mbox{\it B}), \mbox{\it B}\}$
}


\newpage

{\samepage \clearpage $\{\mbox{\it len}(\mbox{\it B}),\mbox{\it B}\}$
}


\newpage

{\samepage \clearpage $\BBB$
}


\newpage

{\samepage \clearpage $\mbox{\it len}(\mbox{\it B})$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{0}$})$}}+\mbox{\it Y} = 
\mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{0+\mbox{\it Y}}$})$}}. $$
}


\newpage

{\samepage \clearpage $0$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{\mbox{\it X}}$})$}}+\mbox{\it Y} =  \mbox{\fbox{$\mbox{\it s}(\mbox{$\underline{\XXX+\mbox{\it Y}}$})$}}. $$
}


\newpage

{\samepage \clearpage $\mbox{\it sorted}(\mbox{\it isort}(\mbox{\it x}))$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it sorted}(\mbox{\fbox{$\mbox{\it insert}(0,\mbox{$\underline{\mbox{\it X}}$})$}}) & = & \mbox{\it sorted}(\mbox{\it X}) \\ 
\mbox{\it sorted}(\mbox{\fbox{$\mbox{\it insert}(\mbox{\it s}(\mbox{\it Y}),\mbox{$\underline{\mbox{\it X}}$})$}}) & = & \mbox{\it sorted}(\mbox{\it X})
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $\{0,\mbox{\it s}(\mbox{\it Y})\}$
}


\newpage

{\samepage \clearpage $$ \mbox{\it sorted}(\mbox{\fbox{$\mbox{\it insert}(\mbox{\it Y},\mbox{$\underline{\mbox{\it X}}$})$}}) = \mbox{\it sorted}(\mbox{\it X}). $$
}


\stepcounter{section}
\newpage

{\samepage \clearpage $$ \forall \mbox{\it a} , \mbox{\it b} \ . \ \mbox{\it qrev}(\mbox{\it a},\mbox{\it b}) = app(\mbox{\it rev}(\mbox{\it a}),\mbox{\it b}) $$
}


\newpage

{\samepage \clearpage $a$
}


\newpage

{\samepage \clearpage $b$
}


\newpage

{\samepage \clearpage $\rev$
}


\newpage

{\samepage \clearpage $\qrev$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it rev}(nil) & = & nil \\ 
\mbox{\it rev}(cons(\mbox{\it H},\mbox{\it T})) & = & app(\mbox{\it rev}(\mbox{\it T}),cons(\mbox{\it H},nil)) \\ 
\mbox{\it qrev}(nil,\mbox{\it R}) & = & \mbox{\it R} \\ 
\mbox{\it qrev}(cons(\mbox{\it H},\mbox{\it T}),\mbox{\it R}) & = & \mbox{\it qrev}(\mbox{\it T},cons(\mbox{\it H},\mbox{\it R})).
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it qrev}(\mbox{\it a},\mbox{\it b}) & = & app(\mbox{\it rev}(\mbox{\it a}),\mbox{\it b})  \\ 
\mbox{\it qrev}(\mbox{\it a},{cons(\mbox{\it c},{\mbox{\it b}})}) & = & app({app({\mbox{\it rev}(\mbox{\it a})},cons(\mbox{\it c},nil ))},\mbox{\it b}) \\ 
\mbox{\it qrev}(\mbox{\it a},{cons(\mbox{\it c},{cons(\mbox{\it d},\mbox{\it b})})}) & = & 
app({app({app(\mbox{\it rev}(\mbox{\it a}),cons(\mbox{\it c},nil ))},cons(\mbox{\it d},nil ))},\mbox{\it b}) \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it qrev}(\mbox{\it a},\mbox{\it b}) & = & app(\mbox{\it rev}(\mbox{\it a}),\mbox{\it b})  \\ 
\mbox{\it qrev}(\mbox{\it a},\mbox{\fbox{$cons(\mbox{\it c},\mbox{$\underline{\mbox{\it b}}$})$}}) & = & app(\mbox{\fbox{$app(\mbox{$\underline{\mbox{\it rev}(\mbox{\it a})}$},cons(\mbox{\it c},nil ))$}},\mbox{\it b}) \\ 
\mbox{\it qrev}(\mbox{\it a},\mbox{\fbox{$cons(\mbox{\it c},\mbox{$\underline{cons(\mbox{\it d},\mbox{\it b})}$})$}}) & = & 
app(\mbox{\fbox{$app(\mbox{$\underline{app(\mbox{\it rev}(\mbox{\it a}),cons(\mbox{\it c},nil ))}$},cons(\mbox{\it d},nil ))$}},\mbox{\it b}) \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ app(\mbox{\fbox{$app(\mbox{$\underline{\mbox{\it rev}(\mbox{\it A})}$},cons(\mbox{\it C},nil ))$}},\mbox{\it B})  = 
app(\mbox{\it rev}(\mbox{\it A}),\mbox{\fbox{$F({\mbox{$\underline{\mbox{\it B}}$}})$}}).  $$
}


\newpage

{\samepage \clearpage $$ app(\mbox{\fbox{$app(\mbox{$\underline{\mbox{\it rev}(\mbox{\it A})}$},cons(\mbox{\it C},nil ))$}},\mbox{\it B}) =  
app(\mbox{\it rev}(\mbox{\it A}),\mbox{\fbox{$cons(\mbox{\it C},\mbox{$\underline{\mbox{\it B}}$})$}}).  $$
}


\newpage

{\samepage \clearpage $$ app(\mbox{\fbox{$app(\mbox{$\underline{\mbox{\it A}}$},cons(\mbox{\it C},nil ))$}},\mbox{\it B})  = 
app(\mbox{\it A},\mbox{\fbox{$cons(\mbox{\it C},\mbox{$\underline{\mbox{\it B}}$})$}}).   $$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y = X+\mbox{\fbox{$F(\mbox{$\underline{Y}$})$}} . $$
}


\newpage

{\samepage \clearpage $\lambda z \, . \, s(z)$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y = X+\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}} . $$
}


\newpage

{\samepage \clearpage $$ \forall \mbox{\it x} , \mbox{\it y} \ . \ (\xxx+\mbox{\it y})-\mbox{\it x} =  \mbox{\it y} $$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}X-0 & = & X \\ 
0-X & = & 0 \\ 
s(\mbox{\it X})-s(\mbox{\it Y}) & = & \mbox{\it X}-\mbox{\it Y}.
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}(x+y)-x & = & y \\ 
(s(x)+y)-x & = & s(y) \\ 
(s(s(x))+y)-x & = & s(s(y)) \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}(x+y)-x & = & y \\ 
(\mbox{\fbox{$s(\mbox{$\underline{x}$})$}}+y)-x & = & \mbox{\fbox{$s(\mbox{$\underline{y}$})$}} \\ 
(\mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}+y)-x & = & \mbox{\fbox{$s(\mbox{$\underline{s(y)}$})$}} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ (\mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y)-X  =  (X+\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}})-X. $$
}


\newpage

{\samepage \clearpage $\lambda z \, . \, z - X$
}


\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y  =  X+\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}}. $$
}


\newpage

{\samepage \clearpage \begin{figure}% latex2html id marker 428
[htb]
\begin{center}
\fbox{
\begin{minipage}{4in}
{
\mbox{} 

Preconditions:
\begin{enumerate}
\item There is a sequence of equations $s_i=t_i$ which
the prover attempts to prove by induction ($i$ = 0, 1 ...);
\item There exists (non trivial) $G, H$ such 
that for each $j$, the maximal difference match has
$s_{j} = G(U_j,Acc)$  and
$s_{j+1} = G(\mbox{\fbox{$H(\mbox{$\underline{U_j}$})$}},Acc)$. 
\end{enumerate}
Postconditions:
\begin{enumerate}
\item The critic proposes a rule of the
form,
\begin{eqnarray*}
G(\mbox{\fbox{$H(\mbox{$\underline{U_0}$})$}},Acc) & = & G(U_0,\mbox{\fbox{$F(\mbox{$\underline{Acc}$})$}})
\end{eqnarray*}
\item $F$ is instantiated by the fertilization or simplification
heuristics;
\item The lemma is generalized using the (augmented) primary terms 
and equality heuristics;
\item Generalized lemmas are filtered through a 
type checker and a conjecture
disprover;
\item If several lemmas are suggested, 
the critic deletes any that are subsumed.
\end{enumerate}
}
\end{minipage}
}
\caption{Speculation of transverse wave rules.}
\end{center}
\end{figure}
}


\stepcounter{section}
\newpage

{\samepage \clearpage \begin{figure}% latex2html id marker 457
{
\hline
\begin{verbatim}

% compiling file /home/dream5/tw/work/Spike/diverge/data.double.x+x
% data.double.x+x compiled in module user, 0.233 sec 1,612 bytes

| ?- speculate.

  Equations input:
  double(x1)=x1+x1
  s(x1+x1)=s(x1)+x1
  s(s(x1+x1))=s(s(x1))+x1
  s(s(s(x1+x1)))=s(s(s(x1)))+x1

  Lemmas speculated:
  s(x1)+x1=s(x1+x1)
  s(x1)+x99=s(x1+x99)
  s(x99)+x1=s(x99+x1)
  s(x99)+x100=s(x99+x100)
  s(x1)+x1=x1+s(x1)
  s(x1)+x99=x1+s(x99)
  s(x99)+x1=x99+s(x1)  
  s(x99)+x100=x99+s(x100)

  Deleting lemmas subsumed:
  s(x1)+x99=s(x1+x99)
  s(x1)+x99=x1+s(x99)

  Merging remaining lemmas:
  s(x1)+x99=s(x1+x99)
  s(x1)+x99=x1+s(x99)

yes
| ?-\end{verbatim}
}
\hline
\caption{Example output of the divergence critic. }
\end{figure}
}


\stepcounter{section}
\newpage

{\samepage \clearpage \begin{table}% latex2html id marker 467
{
{\small
\begin{tabular}{|r|c|c|r|} \hline
No & Theorem & Lemmas speculated & Time/s \\  \hline \hline
1 & s(x)+x=s(x+x) & s(X)+Y=s(X+Y) & 7.8 \\ 
& & s(X)+Y=X+s(Y) & \\  \hline
2 & dbl(x)=x+x $\leftrightarrow$ & s(X)+Y=s(X+Y) & 8.2 \\ 
& $ \ \ \ \ $  dbl(0)=0, \ dbl(s(x))=s(s(dbl(x))) & s(X)+Y=X+s(Y) & \\  \hline
3 & len(x \mbox{$\! \mbox{@} \!$} y)=len(y \mbox{$\! \mbox{@} \!$} x) & 
 len(X \mbox{$\! \mbox{@} \!$} (Z \mbox{$\! :: \!$} Y))=s(len(X \mbox{$\! \mbox{@} \!$} Y)) & 3.6 \\ 
& &len(X \mbox{$\! \mbox{@} \!$} (Z \mbox{$\! :: \!$} Y))=len((W \mbox{$\! :: \!$} X) \mbox{$\! \mbox{@} \!$} Y) & \\ 
\hline
4 & len(x \mbox{$\! \mbox{@} \!$} y)=len(x)+len(y) & s(X)+Y=s(X+Y)
& 7.2 \\  & & s(X)+Y=X+s(Y) & \\  \hline
5 & len(x \mbox{$\! \mbox{@} \!$} x)=dbl(len(x)) &
len(X \mbox{$\! \mbox{@} \!$} (Z \mbox{$\! :: \!$} Y))=s(len(X \mbox{$\! \mbox{@} \!$} Y)) & 11.6 \\ 
& & len(X \mbox{$\! \mbox{@} \!$} (W \mbox{$\! :: \!$} Z \mbox{$\! :: \!$} Y))=s(len(X \mbox{$\! \mbox{@} \!$} (W \mbox{$\! :: \!$} Y))) &
\\  \hline
6 & even(x+x) &  even(s(s(X))+Y)=even(X+Y) & 5.4 \\  \hline
7 & odd(s(x)+x) & odd(s(s(X))+Y)=odd(X+Y) & 16.0 \\  \hline
8 & even\mbox{${}_m$}(x+x) &
even\mbox{${}_m$}(s(s(X))+Y)=even\mbox{${}_m$}(X+Y) & 28.4 \\ 
& & odd\mbox{${}_m$}(s(s(X))+Y)=odd\mbox{${}_m$}(X+Y) &  \\  \hline
9 & odd\mbox{${}_m$}(s(x)+x) &
even\mbox{${}_m$}(s(s(X))+Y)=even\mbox{${}_m$}(X+Y) & 65.5 \\ 
& & odd\mbox{${}_m$}(s(s(X))+Y)=odd\mbox{${}_m$}(X+Y) &  \\  \hline
10 & even\mbox{${}_m$}(x) $\rightarrow$ half(x)+half(x)=x &
s(X)+Y=s(X+Y) & 6.0 \\  & & s(X)+Y=X+s(Y) & \\  \hline
11 & half(x+x)=x &  s(s(X))+Y=X+s(s(Y)) & 11.1 \\  
& & half(s(s(X))+Y)=half(X+Y) & \\  \hline
12 & half(s(x)+x)=x &  s(s(X))+Y=X+s(s(Y)) & 31.0 \\  
& & half(s(s(X))+Y)=half(X+Y) & \\  \hline
13 & rot(len(x),x)=x &
rot(len(X),X \mbox{$\! \mbox{@} \!$} [Y])=Y \mbox{$\! :: \!$} rot(len(X),X) & 2.4 \\  \hline
14 & len(rot(len(x),x))=len(x) &  
len(rot(X,Z \mbox{$\! \mbox{@} \!$} [Y]))=s(len(rot(X,Z)))  & 4.8 \\  \hline
15 & rot(len(x),x \mbox{$\! \mbox{@} \!$} [y])=y \mbox{$\! :: \!$} rot(len(x),x) & 
(X \mbox{$\! \mbox{@} \!$} [Y]) \mbox{$\! \mbox{@} \!$} Z=X \mbox{$\! \mbox{@} \!$} (Y \mbox{$\! :: \!$} Z)& 86.3 \\ 
& &
rot(len(X),(X \mbox{$\! \mbox{@} \!$} [Y]) \mbox{$\! \mbox{@} \!$} Z)=Y \mbox{$\! :: \!$} rot(len(X),X \mbox{$\! \mbox{@} \!$} Z)
&  \\  \hline
16 & len(rev(x))=len(x) & len(X \mbox{$\! \mbox{@} \!$} [Y])=s(len(X)) & 2.0 \\  \hline
17 & rev(rev(x))=x & rev(X \mbox{$\! \mbox{@} \!$} [Y])=Y \mbox{$\! :: \!$} rev(X) & 1.2
\\  \hline 
18 & rev(rev(x) \mbox{$\! \mbox{@} \!$} [y])=y \mbox{$\! :: \!$} x &
 rev(X \mbox{$\! \mbox{@} \!$} [Y])=Y \mbox{$\! :: \!$} rev(X) & 16.0  \\   \hline
19 & rev(rev(x) \mbox{$\! \mbox{@} \!$} [y])=y \mbox{$\! :: \!$} rev(rev(x)) &
rev(X \mbox{$\! \mbox{@} \!$} [Y])=Y \mbox{$\! :: \!$} rev(X)
& 18.6 \\  \hline
20 & len(rev(x \mbox{$\! \mbox{@} \!$} y))=len(x)+len(y) &
len(X \mbox{$\! \mbox{@} \!$} [Y])=s(len(X)) & 10.0 \\ 
& & s(X)+Y=s(X+Y)& \\  & & s(X)+Y=X+s(Y)& \\  \hline
21 & len(qrev(x,[]))=len(x) & len(qrev(X,Z \mbox{$\! :: \!$} Y))=s(len(qrev(X,Y)))
& 2.2 \\  \hline
22 & qrev(x,y)=rev(x) \mbox{$\! \mbox{@} \!$} y &
(X \mbox{$\! \mbox{@} \!$} [Y]) \mbox{$\! \mbox{@} \!$} Z=X \mbox{$\! \mbox{@} \!$} (Y \mbox{$\! :: \!$} Z) & 3.4 \\  \hline
23 & len(qrev(x,y))=len(x)+len(y) & s(X)+Y=s(X+Y)
& 12.0 \\  & & s(X)+Y=X+s(Y) & \\  \hline
24 & qrev(qrev(x,[]),[])=x &
qrev(qrev(X,{[Y]}),Z)=Y \mbox{$\! :: \!$} qrev(qrev(X,[]),Z) & 5.0 \\ 
\hline
25 & rev(qrev(x,[]))=x & 
rev(qrev(X,[Y]))=Y \mbox{$\! :: \!$} rev(qrev(X,[])) & 5.8 \\  
\hline
26 & qrev(rev(x),[])=x &
qrev(X \mbox{$\! \mbox{@} \!$} [Y],Z)=Y \mbox{$\! :: \!$} qrev(X,Z) & 5.2 \\  \hline
27 & nth(i,nth(j,x))=nth(j,nth(i,x)) & 
nth(s(I),nth(J,Y \mbox{$\! :: \!$} X))=nth(I,nth(J,X)) & 7.4 \\  \hline
28 & nth(i,nth(j,nth(k,x)))=nth(k,nth(j,nth(i,x))) & 
nth(s(I),nth(J,Y \mbox{$\! :: \!$} X))=nth(I,nth(J,X)) & 7.6 \\  \hline
29 & len(isort(x))=len(x) & len(insert(Y,X))=s(len(X)) & 2.0 \\  \hline
30 & sorted(isort(x)) & sorted(insert(Y,X))=sorted(X) & 114 \\ 
& & sorted(insert(Y,insert(Z,X)))=sorted(X) & \\  \hline
\end{tabular} 
}

\caption{Some lemmas speculated by the divergence critic.}


\noindent
{\bf Notes:}  \mbox{$\! :: \!$}  is written for 
infix cons,  \mbox{$\! \mbox{@} \!$}  for infix append, []\ for 
nil, and [\mbox{\it x}] for cons(\mbox{\it x},nil ). 
In addition, even is defined by a s(s(x)) recursion,
even$\mbox{}_{m}$ by a mutual recursion with
odd$\mbox{}_{m}$, and
rot($n,l$) rotates a list $l$ by $n$ elements.


}
\end{table}
}


\newpage

{\samepage \clearpage $$ \# \# \ \ \ \ \ \  len(\mbox{\fbox{$app(\mbox{$\underline{X}$},cons(Y,nil))$}})=len(X) \ \ \ \ \ \ \# \# $$
}


\newpage

{\samepage \clearpage $$  len(\mbox{\fbox{$app(\mbox{$\underline{X}$},cons(Y,nil))$}})=\mbox{\fbox{$s(\mbox{$\underline{len(X)}$})$}} . $$
}


\newpage

{\samepage \clearpage $$ len(app(X,(cons(W,\mbox{\fbox{$cons(Z,\mbox{$\underline{Y}$})$}}))))=\mbox{\fbox{$s(\mbox{$\underline{len(app(X,cons(W,Y)))}$})$}} . $$
}


\newpage

{\samepage \clearpage $$ even(\mbox{\fbox{$s(s(\mbox{$\underline{X}$}))$}}+Y) = even(X+Y) $$
}


\newpage

{\samepage \clearpage $s(X)+Y=s(X+Y)$
}


\newpage

{\samepage \clearpage $s(X)+Y=X+s(Y)$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}even_m(x+x) & = & true \\ 
odd_m(s(x)+x) & = & true \\ 
even_m(s(s(x))+x) & = & true \\ 
odd_m(s(s(s(x)))+x) & = & true \\ 
even_m(s(s(s(s(x))))+x) & = & true \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}even_m(x+x)  =  true & \ \ \ \ \ \ \ \ \ \ & odd_m(s(x)+x)  =  true  \\ 
even_m(\mbox{\fbox{$s(s(\mbox{$\underline{x}$}))$}}+x) =  true & & odd_m(\mbox{\fbox{$s(s(\mbox{$\underline{s(x)}$}))$}}+x) =  true  \\ 
even_m(\mbox{\fbox{$s(s(\mbox{$\underline{s(s(x))}$}))$}}+x)  =  true & & odd_m(\mbox{\fbox{$s(s(\mbox{$\underline{s(s(s(x)))}$}))$}}+x)  =  true \\ 
\vdots & & \vdots 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}even_m(\mbox{\fbox{$s(s(\mbox{$\underline{X}$}))$}}+Y) & = & even_m(X+Y) \\ 
odd_m(\mbox{\fbox{$s(s(\mbox{$\underline{X}$}))$}}+Y) & = & odd_m(X+Y) 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $rot$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}len(rev(x))  & = &  0+len(x) \\ 
len(\mbox{\fbox{$app(\mbox{$\underline{rev(x)}$},cons(y,nil))$}})  & = &  \mbox{\fbox{$s(\mbox{$\underline{0+len(x)}$})$}} \\ 
len(\mbox{\fbox{$app(\mbox{$\underline{app(rev(x),cons(y,nil))}$},cons(z,nil))$}})  & = &  \mbox{\fbox{$s(\mbox{$\underline{s(0+len(x))}$})$}} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}len(\mbox{\fbox{$app(\mbox{$\underline{X}$},cons(Y,nil))$}})  & = &  \mbox{\fbox{$s(\mbox{$\underline{len(X)}$})$}}
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}s(x)+len(y) & = & s(x+len(y)) \\ 
 \mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}+len(y)  & = & \mbox{\fbox{$s(\mbox{$\underline{s(x+len(y))}$})$}} \\ 
 \mbox{\fbox{$s(\mbox{$\underline{s(s(x))}$})$}}+len(y)  & = &  \mbox{\fbox{$s(\mbox{$\underline{s(s(x+len(y)))}$})$}} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\fbox{$s(\mbox{$\underline{X}$})$}} + Y & = & \mbox{\fbox{$s(\mbox{$\underline{X+Y}$})$}} \\ 
\mbox{\fbox{$s(\mbox{$\underline{X}$})$}} + Y & = & X+\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}} 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{table}% latex2html id marker 658
{\begin{tabular}{|r|c|c|r|} \hline
No & Theorem & Lemmas speculated & Time/s \\  \hline \hline
31 & s(x) $\times$ y=y+(x $\times$ y) & -- & n/a \\  \hline
32 & x $\times$ y=y $\times$ x & s(X)+Y=X+s(Y) & 8.0 \\  \hline
33 & x+(y+(z+(v+w))) = w+(x+(y+(z+v))) & s(X)+Y=s(X+Y) & 17.7 \\ 
   &               & s(X)+Y=X+s(Y) & \\  \hline
34 & qrev(qrev(x,{[y]}),z)=y \mbox{$\! :: \!$} qrev(qrev(x,[]),z) & 
qrev(Y,X \mbox{$\! :: \!$} Z)) = qrev(X \mbox{$\! :: \!$} Y,Z) & 9.6 \\ 
& &  qrev(qrev(X,Y \mbox{$\! :: \!$} Z),W)=qrev(qrev(Y \mbox{$\! :: \!$} X,Z),W) & \\ 
& &  qrev(qrev(X,Y \mbox{$\! :: \!$} [Z]),W)=Z \mbox{$\! :: \!$} qrev(qrev(X,[Y]),W) & \\  \hline
\end{tabular}}

\caption{Some of the divergence critic's failures.}
\end{table}
}


\newpage

{\samepage \clearpage $\times$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}s(y) + (x+ (x \times y)) & = & s(y) + (y + (x \times y)) \\ 
s(s(y)) + (x + (x + (x\times  y))) & = & s(x) + (s(y) + (x + (x \times y)) \\ 
s(s(s(y))) + (x + (x + (x + (x \times y)))) & = & s(x) + (s(s(y)) + (x + (x + (x \times y)))) \\ 
& \vdots &
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}} + \mbox{\fbox{$(X+ \mbox{$\underline{Z}$})$}} & = & \mbox{\fbox{$F(\mbox{$\underline{Y + Z}$})$}}
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $\lambda z \, . \, s(X + z)$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\fbox{$s(\mbox{$\underline{X}$})$}} + Y & = & \mbox{\fbox{$s(\mbox{$\underline{X+Y}$})$}} \\ 
Y + \mbox{\fbox{$(X+\mbox{$\underline{Z}$})$}} & = & \mbox{\fbox{$X+\mbox{$\underline{(Y+Z)}$}$}} 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\fbox{$s(\mbox{$\underline{X}$})$}}+Y & = & X+\mbox{\fbox{$s(\mbox{$\underline{Y}$})$}}
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}x+(y+(x+(x*y))) & = & y+(x+(x+(x*y))) \\ 
x+(y+\mbox{\fbox{$(x+\mbox{$\underline{(x+(x*y))}$})$}}) & = & y+\mbox{\fbox{$(x+\mbox{$\underline{(x+(x+(x*y)))}$})$}} \\ 
x+(y+\mbox{\fbox{$(x+\mbox{$\underline{(x+(x+(x*y)))}$})$}}) & = & y+\mbox{\fbox{$(x+\mbox{$\underline{(x+(x+(x+(x*y))))}$})$}} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}X+\mbox{\fbox{$(Y+\mbox{$\underline{Z}$})$}} & = & \mbox{\fbox{$Y+\mbox{$\underline{(X+Z)}$}$}}
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}0 + x & = & x \\ 
\mbox{\fbox{$s(\mbox{$\underline{0}$})$}} + x & = & \mbox{\fbox{$s(\mbox{$\underline{x}$})$}} \\ 
\mbox{\fbox{$s(\mbox{$\underline{s(0)}$})$}} + x & = & \mbox{\fbox{$s(\mbox{$\underline{s(x)}$})$}}
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$
qrev(X,Y) = app(qrev(X,nil),Y)
$$
}


\stepcounter{section}
\newpage

{\samepage \clearpage $$ \mbox{\fbox{$s(\mbox{$\underline{\mbox{\fbox{$s(\mbox{$\underline{x}$})$}}+x}$})$}}. $$
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},nil)) & = & \mbox{\it x} \\ 
\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},{cons(\mbox{\it y},{nil})})) & = & {cons(\mbox{\it y},{\mbox{\it x}})} \\ 
\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},{cons(\mbox{\it z},{cons(\mbox{\it y},nil)})})) & = & {cons(\mbox{\it z},{cons(\mbox{\it y},\mbox{\it x})})} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage \begin{eqnarray*}\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},nil)) & = & \mbox{\it x} \\ 
\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},\mbox{\fbox{$cons(\mbox{\it y},\mbox{$\underline{nil}$})$}})) & = & \mbox{\fbox{$cons(\mbox{\it y},\mbox{$\underline{\mbox{\it x}}$})$}} \\ 
\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it x},\mbox{\fbox{$cons(\mbox{\it z},\mbox{$\underline{cons(\mbox{\it y},nil)}$})$}})) & = & \mbox{\fbox{$cons(\mbox{\it z},\mbox{$\underline{cons(\mbox{\it y},\mbox{\it x})}$})$}} \\ 
& \vdots & 
\end{eqnarray*}
}


\newpage

{\samepage \clearpage $$ \mbox{\it rev}(\mbox{\it qrev}(\mbox{\it X},\mbox{\fbox{$cons(\mbox{\it Y},\mbox{$\underline{nil}$})$}})) =
\mbox{\fbox{$cons(\mbox{\it Y},\mbox{$\underline{\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it X},nil))}$})$}}. $$
}


\newpage

{\samepage \clearpage $\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it X},\mbox{\it Z}))$
}


\newpage

{\samepage \clearpage $\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it X},cons(\mbox{\it Y},\mbox{\it Z})))$
}


\newpage

{\samepage \clearpage $\mbox{\it rev}(\mbox{\it qrev}(\mbox{\it X},{cons(\mbox{\it Y},{nil})}))$
}


\stepcounter{section}
\stepcounter{section}

\end{document}