In order to prove a final theorem about subsets,

LP formulates an appropriate subgoal for the proof of this conjecture, together with additional hypotheses to be used in the proof, using a new operatorprove sort S generated by {}, {__}, \union resume by induction set name lemma critical-pairs *GenHyp with *GenHyp critical-pairs *InductHyp with lemma qed

The user then directs LP to attempt to proveCreating 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)

as a critical pair between the second and thirdlemma.1: isGenerated(s) => isGenerated(insert(e, s))