generate subgoals using induction
Major Section: PROOF-CHECKER-COMMANDS
Examples: induct, (induct t) -- induct according to a heuristically-chosen scheme, creating a new subgoal for each base and induction step (induct (append (reverse x) y)) -- as above, but choose an induction scheme based on the term (append (reverse x) y) rather than on the current goalInduct as in the corresponding
General Form: (induct &optional term)
:inducthint given to the theorem prover, creating new subgoals for the base and induction steps. If term is
tor is not supplied, then use the current goal to determine the induction scheme; otherwise, use that term.
Remark: As usual, abbreviations are allowed in the term.
Induct actually calls the
prove command with all
processes turned off. Thus, you must be at top of the goal for an