The proof of the first theorem in set1.lp is straightforward.

The prove command directs LP to initiate the proof of a conjecture, and the qed command directs LP to confirm that its proof is complete. LP proves this conjecture automatically by using the user-supplied axioms as rewrite rules. When using a formula as a rewrite rule, either LP rewrites terms matching the entire formula toset name setTheorems prove e \in {e} qed

Most proofs require user guidance. For example, to prove that for any two elementse \in {e} ~> e \in insert(e, {}) by setAxioms.2 ~> e = e \/ e \in {} by setAxioms.4 ~> true \/ e \in {} by a hardwired axiom for = ~> true by a hardwired axiom for \/

Users can specify a proof method for a conjecture either as part of the prove command or in a separate resume command, which continues the proof of the conjecture.prove \E x \A e (e \in x <=> e = e1 \/ e = e2) resume by specializing x to insert(e2, {e1}) qed