### ACL2-PC::INDUCT

(atomic macro)
` `

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 goal
General Form:
(induct &optional term)

Induct as in the corresponding `:induct`

hint given to the theorem
prover, creating new subgoals for the base and induction steps. If
term is `t`

or 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.

**Remark:** `Induct`

actually calls the `prove`

command with all
processes turned off. Thus, you must be at top of the goal for an `induct`

instruction.