\doc{Sample proofs: sample conjectures}

We will illustrate LP's proof mechanisms by proving the following sample
conjectures:
\begin{verbatim}
set name setTheorems
prove e \in {e}
prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
prove x \union {} = x
prove x \union insert(e, y) = insert(e, x \union y)
prove ac \union
prove e \in x /\ x \subseteq y => e \in y
prove x \subseteq y /\ y \subseteq x => x = y
prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z
prove sort S generated by {}, {__}, \union
prove x \subseteq (x \union y)
prove x \subseteq x
\end{verbatim}
Except for the fourth, the sample conjectures are like the sample axioms: they
are either formulas or induction rules.  The fourth, \f{ac \union}, is an
abbreviation for the conjunction of the 
\llink{operator-theory}{associative and commutative laws} for the \fq{\union} 
operator.  It provides LP with useful operational information.  For example, it
allows LP to conclude that \f#{} \union x# is the same set as \f#x \union {}#;
hence the third conjecture shows that both of these sets are the same as \f#x#.
\p
The order in which we have stated these conjectures is not completely
arbitrary.  As we shall see, some of them are used to prove conjectures
appearing later in the list.