### ACL2-PC::BASH

(atomic macro)
` `

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

Call the theorem prover's simplifier, creating a subgoal for each
resulting goal.
Notice that unlike `prove`

, the arguments to `bash`

are spread out, and
are all hints.

**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).