\doc{Proofs by multilevel induction}
\ref{multilevel-induction}

The command \fq{prove F by induction on x depth n using IR} directs LP to prove
a formula \f{F} by \v{n}-level structural induction; by default, \v{n} is 1.
For example, proving a formula \fq{F(x)} by depth 2 induction using the
induction rule \fq{sort Nat generated by 0, s}, involves proving two basis
subgoals, \fq{F(0)} and \fq{F(s(0))}, and one induction subgoal,
\fq{F(s(s(xc)))}, given \fq{F(xc)} and \fq{F(s(xc))} as induction hypotheses.
\p
In general, LP constructs the basis and induction steps using the set \v{G} of
generators for the sort \f{S} of \fq{x} specified by the induction rule \f{IR},
as follows.
\p
Definition 1.  A (\v{G},\f{F},\v{C})-\def{ground term}, where \v{C} is a set of
constants of sort \f{S}, is a quantifier-free term of sort \f{S} in which all
operators are either in \v{C} or are inductive generators in \v{G}, no variable
has sort \f{S}, no variable occurs more than once, and no variable also occurs
in \f{F}.
\p
Definition 2.  A (\v{G},\f{F})-\def{ground term} is a
(\v{G},\f{F},\v{B})-ground term, where \v{B} is the set of basis generators in
\v{G}.
\p
Definition 3.  The \def{depth} of a quantifier-free term is 0 if the term
consists of a variable; otherwise it is one more than the maximum depth of its
arguments.
\p
Definition 4.  A (\v{G},\f{F},{\f{c1},...,\f{cm}})-ground term is
\def{canonical} if it contains exactly one occurrence of each of \f{c1}, ..., 
\f{ck} for some \v{k <= m}.
\p
The basis step involves proving all formulas of the form \fq{F(x gets t)} where
\fq{t} is an (\v{G},\f{F},\v{B})-ground term of depth at most \v{n}.
\p
The induction step introduces a set \v{C} = {\f{c1},...,\f{cm}} of new
constants of sort \f{S}, where \v{m} is the maximum number of arguments of sort
\f{S} in a generator in \v{G} raised to the power \v{n}.  The induction step
involves proving all formulas of the form \fq{F(x gets t)}, where \fq{t} is a
canonical (\v{G},\f{F},\v{C})-ground term of depth \v{n+1}.  The induction
hypotheses available in the induction step consist of all formulas of the form
\fq{F(x gets t)}, where \fq{t} is a (\v{G},\f{F},\v{C})-ground term of depth at
most \v{n}.
\p
When \v{n} is 1, the induction hypotheses consist of all formulas of the form
\fq{F(x gets c)}, where \fq{c} is in \v{C}; and the induction step involves 
proving all formulas of the form \fq{F(x gets t)}, where \fq{t} is a canonical
(\v{G},\f{F},\v{C})-ground term of depth 2.
\p
Examples:
\begin{verbatim}
Gener-  Level   Basis           Induction                 Induction
ators           Subgoals        Hypotheses                Subgoals

0, s      1     f(0)            f(c)                      f(s(c))

0, s      2     f(0)            f(c)                      f(s(s(c)))
                f(s(0))         f(s(c))

0, 1, +   1     f(0)            f(c1)                     f(c1+c2)
                f(1)            f(c2)

0, 1, +   2     f(0)            f(c1), f(c2)              f(c1+(c2+c3)
                f(1)            f(c3), f(c4)              f((c1+c2)+c3)
                f(0+0)          f(c1+c1), f(c1+c2), ...   f((c1+c2)+(c3+c4))
                f(0+1)          f(c2+c1), f(c2+c2), ...       
                f(1+0)          f(c3+c1), f(c3+c2), ...
                f(1+1)          f(c4+c1), f(c4+c2), ...
                                
                                
nil       1     f(nil)          f(c)                      f(cons(x, c))
cons

nil       2     f(nil)          f(c)                      f(cons(x,cons(y,c))
cons            f(cons(x,nil))  f(cons(x,c))
\end{verbatim}