call the ACL2 prover without induction, after going into
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
spread out, and are all hints. See also
Remark: Induction and the various processes will be used to the
extent that they are ordered explicitly in the