LP, the Larch Prover -- Sample proofs: sample conjectures

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

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

Except for the fourth, the sample conjectures are like the sample axioms: they are either formulas or induction rules. The fourth, ac \union, is an abbreviation for the conjunction of the associative and commutative laws for the \union operator. It provides LP with useful operational information. For example, it allows LP to conclude that {} \union x is the same set as x \union {}; hence the third conjecture shows that both of these sets are the same as 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.