\doc{Proofs of induction rules}
\ref{proof-of-induction-rule}
\ref{isGenerated}

LP permits users to prove \llink{induction-rule}{induction rules} as well as
\clink{assert} them.  To prove a \dlink{structural}{structural} induction rule 
such as
\begin{verbatim}
sort Set generated by {}, {__}, \U
\end{verbatim}
LP creates a single subgoal that involves proving the formula
\fq{isGenerated(x)} using the hypotheses
\begin{verbatim}
isGenerated({})
isGenerated({e})
isGenerated(s1) /\ isGenerated(s2) => isGenerated(s1 /\ s2)
\end{verbatim}
where \fq{isGenerated} is a new operator with signature \fq{Set->Bool}.  The
names of the hypotheses have the form \s{simpleId}\fq{GenHyp.}\s{number}, where
\s{simpleId} is the current value of the \setlink{name-prefix} setting.  User
guidance is generally required to finish the proof, for example, by using the
induction rule \fq#sort Set generated by {}, insert#.
\p
To prove a structural induction rule such as
\begin{verbatim}
sort Nat generated freely by 0:->Nat, f:Nat->Nat, g:Nat->Nat
\end{verbatim}
LP also attempts to prove the subgoals
\begin{verbatim}
f(n) ~= 0          f(n) = f(n1) <=> n = n1          f(n) ~= g(n1)
g(n) ~= 0          g(n) = g(n1) <=> n = n1
\end{verbatim}
in addition to the subgoal \fq{isGenerated(n)}.
\p
To prove a \dlink{well-founded}{well-founded} induction rule such as 
\fq{well founded <}, LP creates a single subgoal that involves proving the 
formula
\fq{isGenerated(x)} using the hypothesis
\begin{verbatim}
\A n1 (n1 < n => isGenerated(n1)) => isGenerated(n)
\end{verbatim}