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

The command \fq{prove F by induction on x using IR} directs LP to prove a
formula \fq{F} by induction on the variable \fq{x} using the named 
\llink{induction-rule}{induction rule}.  The name of the variable and/or that 
of the induction rule can be omitted if they can be inferred (e.g., because
induction is possible on only one variable in \fq{F} and there is only one
induction rule for the sort of that variable).  The keyword \fq{on} is
optional.  The keyword \fq{using} can be omitted if the name of a variable is
given.
\p
The command \fq{resume by induction} directs LP to resume the proof of the
current conjecture by induction.
\p
LP supports proofs both by structural and well-founded induction.  Induction
rules beginning with \fq{generated by} provide the basis for proofs by
\dlink{structural}{structural} induction.  Induction rules beginning with 
\fq{well founded} provide the basis for proofs by
\dlink{well-founded}{well-founded} induction.
\p
LP generates appropriate subgoals for each kind of proof by induction.  Some of
those subgoals introduce additional hypotheses, known as 
\def{induction hypotheses}.  
The names of the induction hypotheses have the form
\s{simpleId}\fq{InductHyp.}\s{number}, where \s{simpleId} is the current value
of the \setlink{name-prefix} setting.