LP, the Larch Prover -- Sample proofs: three theorems about union

The next three theorems in set1.lp follow from the principle of extensionality.

prove x \union {} = x
  instantiate y by x \union {} in extensionality
qed

The instantiate command directs LP to form the substitution instance

\A e (e \in x <=> e \in x \union {}) => x = x \union {}

of the fact name extensionality. LP rewrites this formula automatically to

\A e (e \in x <=> e \in x \/ e \in {}) => x = x \union {}

using the definition of \union, then to

\A e (e \in x <=> e \in x \/ false) => x = x \union {}

using the definition of \in, and then successively to

\A e (e \in x <=> e \in x) => x = x \union {}
\A e (true) => x = x \union {}
true => x = x \union {}
x = x \union {}

using LP's hardwired axioms. LP orients this final simplification into the rewrite rule x \union {} -> x, which it uses to simplify the conjecture to true.

Two other theorems about union can also be proved by instantiating the extensionality axiom. Both proofs are left as exercises to the reader.

prove x \union insert(e, y) = insert(e, x \union y)
prove ac \union