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 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.
Reduce is similar to
bash in that neither of these allows induction.
bash only allows simplification, while
reduce allows processes
Note: Induction will be used to the extent that it is ordered
explicitly in the hints.