\doc{The prove command}
\ref{prove-command}
\ref{contexts}
\ref{hypothesis}
\ref{hypotheses}

The \def{prove command} initiates the proof of a conjecture.

\head{2}{\dlink{../symbols/syntax}{Syntax}}
\begin{verbatim}
\sd{prove-command} ::= \f{prove} \slink{assert}{assertion} [ \f{by} \slink{../proof/methods}{proof-method} ]
\end{verbatim}

\head{2}{Examples}
\begin{verbatim}
prove e \in {e}
prove i * (j + k) = (i * j) + (i * k) by induction on i
prove sort Set generated by {}, insert
\end{verbatim}

\head{2}{Usage}

The \fq{prove} command initiates an attempt to prove a conjectured assertion
using the specified method.  If no method is specified, LP uses the one
determined by the current value of the \setlink{proof-methods} setting.  LP
assigns a \dlink{../misc/name}{name} to the conjecture using the current
\setlink{name-prefix} setting, unless the assertion begins with
\f{:}\s{simpleId}\f{:}, in which case LP uses that identifier as the
name-prefix for the assertion.  If and when the proof of a conjecture succeeds,
LP adds the conjecture to its logical system and uses it as if it had been
asserted by the \cflink{assert} command.  The \setlink{activity} and
\setlink{immunity} of the conjecture, however, are determined when it is
introduced by a \fq{prove} command, not when it is proved; these attributes can
be changed using the \cflink{make} command.
\p
LP maintains a stack of \def{proof contexts} for conjectures whose proofs are
not yet complete.  Each proof context consists of a conjecture, a
\llink{system}{logical system} of facts available for the proof, and
values for the \dlink{set}{local settings} that govern
the proof.  The conjecture in the topmost proof context on the stack is known
as the \def{current conjecture}.
\p
The \fq{prove} command pushes a new proof context on top of the stack.  Certain
proof methods create \def{subgoals} for proving a conjecture.  LP associates a
separate proof context with each subgoal, and it adds appropriate additional
facts, called \def{hypotheses}, to the logical system in that proof context.
\p
The user can cancel the proof of a conjecture with the \cflink{cancel} command,
which pops the stack of proof contexts.  Or the user can resume the proof of
the current conjecture with the \cflink{resume} command (for example, to
specify a new method of proof or after proving a lemma).  Whenever a proof
succeeds or is canceled, LP pops the stack of proof contexts, restores its
logical system and settings to those in effect before work began on the
conjecture (thereby discarding any lemmas proved while working on the
conjecture), adds the conjecture to the system if it was proved, and resumes
work on the new current conjecture.  As soon as LP can establish the current
conjecture, it terminates any forward inference mechanisms (such as
internormalization of the rewriting system or the computation of critical-pair
equations) that may be in progress.

\head{2}{See also}

\begin{itemize}
\item \dlink{../proof/methods}{Proof methods} available for proving formulas
\item Proofs of \dlink{../proof/of-dr}{deduction rules}, including those
associated with \fq{partitioned by}. 
\item Proofs of \dlink{../proof/of-ir}{induction rules}
\item Proofs of \dlink{../proof/of-ot}{operator theories}
\item Using the \cflink{normalize} and \cflink{rewrite} commands with the 
current conjecture
\end{itemize}