LP, the Larch Prover -- Sample proofs: an alternate induction rule

In order to prove a final theorem about subsets, x \subseteq x, it helps to use a different induction principle than the one we asserted as an axiom. We can prove that induction rule as follows:

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

LP formulates an appropriate subgoal for the proof of this conjecture, together with additional hypotheses to be used in the proof, using a new operator isGenerated:

Creating subgoals for proof of induction rule
Induction subgoal hypotheses:
  setTheoremsGenHyp.1: isGenerated({})
  setTheoremsGenHyp.2: isGenerated({e})
  setTheoremsGenHyp.3:
     isGenerated(s) /\ isGenerated(s1) => isGenerated(s \union s1)
Induction subgoal:
  isGenerated(s)

The user then directs LP to attempt to prove isGenerated(s) by induction (on s) using the asserted induction rule. LP proves the basis subgoal automatically using the hypothesis isGenerated({}). The user guides the proof of the induction subgoal by causing LP to compute critical pairs. The first critical-pairs command causes LP to derive

lemma.1: isGenerated(s) => isGenerated(insert(e, s))

as a critical pair between the second and third isGenerated hypotheses. The second critical-pairs command causes LP to derive the induction subgoal, isGenerated(insert(e, sc)), as a critical pair between this lemma and the induction hypothesis. This finishes the proof of the induction rule.