--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Oct 13 11:15:56 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Oct 13 18:02:08 2000 +0200
@@ -10,10 +10,10 @@
utilize and even derive new induction schemas.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Massaging the proposition\label{sec:ind-var-in-prems}}
+\isamarkupsubsection{Massaging the proposition}
%
\begin{isamarkuptext}%
-\noindent
+\label{sec:ind-var-in-prems}
So far we have assumed that the theorem we want to prove is already in a form
that is amenable to induction, but this is not always the case:%
\end{isamarkuptext}%
@@ -101,15 +101,26 @@
A second reason why your proposition may not be amenable to induction is that
you want to induct on a whole term, rather than an individual variable. In
-general, when inducting on some term $t$ you must rephrase the conclusion as
-\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$
-are the free variables in $t$ and $x$ is new, and perform induction on $x$
-afterwards. An example appears below.%
+general, when inducting on some term $t$ you must rephrase the conclusion $C$
+as
+\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \]
+where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
+perform induction on $x$ afterwards. An example appears in
+\S\ref{sec:complete-ind} below.
+
+The very same problem may occur in connection with rule induction. Remember
+that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is
+some inductively defined set and the $x@i$ are variables. If instead we have
+a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
+replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
+\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
+For an example see \S\ref{sec:CTL-revisited} below.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Beyond structural and recursion induction}
%
\begin{isamarkuptext}%
+\label{sec:complete-ind}
So far, inductive proofs where by structural induction for
primitive recursive functions and recursion induction for total recursive
functions. But sometimes structural induction is awkward and there is no