LP, the Larch Prover -- Proofs by induction

The command prove F by induction on x using IR directs LP to prove a formula F by induction on the variable x using the named induction rule. The name of the variable and/or that of the induction rule can be omitted if they can be inferred (e.g., because induction is possible on only one variable in F and there is only one induction rule for the sort of that variable). The keyword on is optional. The keyword using can be omitted if the name of a variable is given.

The command resume by induction directs LP to resume the proof of the current conjecture by induction.

LP supports proofs both by structural and well-founded induction. Induction rules beginning with generated by provide the basis for proofs by structural induction. Induction rules beginning with well founded provide the basis for proofs by well-founded induction.

LP generates appropriate subgoals for each kind of proof by induction. Some of those subgoals introduce additional hypotheses, known as induction hypotheses. The names of the induction hypotheses have the form <simpleId>InductHyp.<number>, where <simpleId> is the current value of the name-prefix setting.