LP, the Larch Prover -- Sample proofs: two final theorems about subset

The new induction rule, setTheorems.9, helps us prove the following theorem about subsets:

prove x \subseteq (x \union y) by induction on x using setTheorems
qed

The prove command directs LP to use the induction rule just proved to formulate subgoals for the proof by induction using the generators {}, {__}, and \union instead of the generators {} and insert:

Creating subgoals for proof by structural induction on `x'
Basis subgoals:
  Subgoal 1: {} \subseteq ({} \union y)
  Subgoal 2: {e} \subseteq ({e} \union y)
Induction constants: xc, xc1
Induction hypotheses:
  setTheoremsInductHyp.1: xc \subseteq (xc \union y)
  setTheoremsInductHyp.2: xc1 \subseteq (xc1 \union y)
Induction subgoal:
  Subgoal 3: (xc \union xc1) \subseteq (xc1 \union xc \union y)

LP establishes all three subgoals automatically.

Finally, we prove the last theorem by directing LP to compute a critical pair between the theorem just established and an earlier theorem, x \union {} = x.

prove x \subseteq x
  critical-pairs setTheorems with setTheorems
qed