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