### ACL2-PC::REDUCE-BY-INDUCTION

(macro)
` `

call the ACL2 prover without induction, after going into
` `

induction
Major Section: PROOF-CHECKER-COMMANDS

Examples:
reduce-by-induction
-- attempt to prove the current goal after going into induction,
with no further inductions
(reduce-by-induction ("Subgoal 2" :by foo) ("Subgoal 1" :use bar))
-- attempt to prove the current goal after going into induction,
with no further inductions, using the indicated hints
General Form:
(reduce-by-induction &rest hints)

A subgoal will be created for each goal that would have been
pushed for proof by induction in an ordinary proof, except that the
proof begins with a top-level induction.Notice that unlike `prove`

, the arguments to `reduce-by-induction`

are
spread out, and are all hints. See also `prove`

, `reduce`

, and `bash`

.

**Remark**: Induction and the various processes will be used to the
extent that they are ordered explicitly in the `:induct`

and `:do-not`

hints.