Editing Larch Prover (section)

==Sample LP Proofs==

<pre>
set name setTheorems
prove e \in {e}
qed

prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
  resume by specializing x to insert(e2, {e1})
qed

% Three theorems about union (proved using extensionality)

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

prove x \union insert(e, y) = insert(e, x \union y)
  resume by contradiction
    set name lemma
    critical-pairs *Hyp with extensionality
qed

prove ac \union
    resume by contradiction
      set name lemma
      critical-pairs *Hyp with extensionality
    resume by contradiction
      set name lemma
      critical-pairs *Hyp with extensionality
qed

% Three theorems about subset

set proof-methods =>, normalization

prove e \in x /\ x \subseteq y => e \in y by induction on x
      resume by case ec = e1c
        set name lemma
        complete
qed

prove x \subseteq y /\ y \subseteq x => x = y
    set name lemma
    prove e \in xc <=> e \in yc by <=>
        complete
        complete
    instantiate x by xc, y by yc in extensionality
qed

prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x
qed

% An alternate induction rule

prove sort S generated by {}, {__}, \union
    set name lemma
    resume by induction
      critical-pairs *GenHyp with *GenHyp
      critical-pairs *InductHyp with lemma
qed
</pre>