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.

Note: Induction and the various processes will be used to the extent that they are ordered explicitly in the :induct and :do-not hints.