|
|
|---|
|
|
|
|---|
(macro) call the ACL2 prover without induction, after going into induction
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
Remark: Induction and the various processes will be used to the
extent that they are specified explicitly in the