\doc{Proofs by structural induction}
\ref{proof-by-structural-induction}
\ref{proof-by-well-founded-induction}

A proof of a formula \fq{F} by structural induction on a variable \fq{x} of
sort \fq{S} is based on an \llink{induction-rule}{induction rule} that
specifies a set \fq{G} of generators for \fq{S}, that is, a set of operators
with range \fq{S}.  LP generates subgoals for the basis and induction steps in
a proof by structural induction, as follows.
\begin{itemize}
\item
The \def{basis subgoals} involve proving the formulas that result from
substituting the basis generators in \fq{G} for \fq{x} in \fq{F}.  Basis
generators are those with no arguments of sort \fq{S}; fresh variables are used
for variables of other sorts, as in \fq#{e}#.
\p
\item
LP introduces additional hypotheses for the \def{induction subgoals} by
substituting one or more new \llink{constant}{constants} for \fq{x} in \fq{F}.
Each induction subgoal involves proving a formula that results from
substituting a nonbasis generator of \fq{G} (applied to these constants) for
\fq{x} in \fq{F} (e.g., \fq{s(xc)} or \fq{xc \U xc1}).
\end{itemize}

\head{2}{Examples}
\begin{verbatim}
assert sort Nat generated by 0, s
prove 0 + x = x by induction
  Basis subgoal:        0 + 0 = 0
  New constant:         xc
  Induction hypothesis: 0 + xc = xc
  Induction subgoal:    0 + s(xc) = s(xc)
\end{verbatim}
\begin{verbatim}
assert sort Set generated by {}, {__}, \U
prove x \subseteq x by induction
  Basis subgoals:       {} \subseteq {},    {e} \subseteq {e}
  New constants:        xc,                 xc1
  Induction hypotheses: xc \subseteq xc,    xc1 \subseteq xc1
  Induction subgoal:    (xc \U xc1) \subseteq (xc \U xc1)
\end{verbatim}

\head{2}{See also}
\begin{itemize}
\item Proofs by \dlink{multilevel-induction}{multilevel induction}
\item Proofs by \dlink{well-founded}{well-founded induction}
\end{itemize}