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 hints
General Form:
(reduce &rest hints)
Attempt 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.
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.