call the ACL2 theorem prover's simplifier
Major Section: PROOF-CHECKER-COMMANDS
Examples: bash -- attempt to prove the current goal by simplification alone (bash ("Subgoal 2" :by foo) ("Subgoal 1" :use bar)) -- attempt to prove the current goal by simplification alone, with the indicated hintsCall the theorem prover's simplifier, creating a subgoal for each resulting goal.
General Form: (bash &rest hints)
Notice that unlike
prove, the arguments to
bash are spread out, and
are all hints.
Bash is similar to
reduce in that neither of these allows induction.
bash only allows simplification, while
reduce allows processes
Note: All forcing rounds will be skipped (unless there are more
than 15 subgoals generated in the first forcing round, an injustice
that should be rectified by the next release).