We will illustrate LP's proof mechanisms by proving the following sample conjectures:

Except for the fourth, the sample conjectures are like the sample axioms: they are either formulas or induction rules. The fourth,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

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.