The next three theorems in set1.lp establish some basic properties of the subset relation. They illustrate how LP's proof techniques combine to establish conjectures. The user types a few commands to select proof strategies (e.g., a proof by induction or a proof by cases). LP generates subgoals appropriate for the selected strategies and fills in most of the details automatically. Sometimes the user needs to tell LP to work a little harder near the end of a proof to fill in the remaining details.

The set command directs LP to use an automatic proof technique whenever the user does not specify one explicitly. Here, it directs LP to try to prove conjectures first by rewriting, and then to assume the hypotheses of implications and try again. This setting forset proof-methods normalization, => prove e \in x /\ x \subseteq y => e \in y by induction on x resume by case ec = e1c complete qed

LP proves the basis subgoal automatically by rewriting the termCreating subgoals for proof by structural induction on `x' Basis subgoal: Subgoal 1: e \in {} /\ {} \subseteq y => e \in y Induction constant: xc Induction hypothesis: setTheoremsInductHyp.1: e \in xc /\ xc \subseteq y => e \in y Induction subgoal: Subgoal 2: e \in insert(e1, xc) /\ insert(e1, xc) \subseteq y => e \in y

The hypothesis for this subgoal is the result of reducing the hypothesis of the implication in the induction subgoal, after replacing its variables by new constants.Creating subgoals for proof of => New constants: e1c, ec, yc Hypothesis: setTheoremsImpliesHyp.1: (ec = e1c \/ ec \in xc) /\ e1c \in yc /\ xc \subseteq yc Subgoal: ec \in yc

LP finishes the first case by using the case hypothesis to rewrite the subtermCreating subgoals for proof by cases Case hypotheses: setTheoremsCaseHyp.1.1: ec = e1c setTheoremsCaseHyp.1.2: ~(ec = e1c) Same subgoal for all cases: ec \in yc

In the second case, LP uses the case hypothesis and its hardwired rules to
rewrite the first conjunct of the implication hypothesis to `ec \in xc`, at
which point it gets stuck. The complete command directs LP to use what
it knows to finish the proof by deriving a few critical-pair equations. First,
LP derives `xc \subseteq y => ec \in y` as critical pair between
`ec \in xc` and the induction hypothesis . Then it obtains `ec \in yc`
as a critical pair between this fact and the last conjunct of the implication
hypothesis. This finishes the proof by cases, the proof of the implication for
the induction step of the conjecture, and the proof of the conjecture itself.

In the second, LP fills in all the details in a proof by induction without requiring further guidance from the user.prove x \subseteq y /\ y \subseteq x => x = y 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