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