call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS
Examples: reduce -- attempt to prove the current goal without using induction (reduce ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal by without using induction, with the indicated hintsAttempt to prove the current goal without using induction, using the indicated hints (if any). A subgoal will be created for each goal that would have been pushed for proof by induction in an ordinary proof.
General Form: (reduce &rest hints)
Notice that unlike
prove, the arguments to
reduce are spread out,
and are all hints.
Note: Induction will be used to the extent that it is ordered
explicitly in the hints.