### 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.

`Bash`

is similar to `reduce`

in that neither of these allows induction.
But `bash`

only allows simplification, while `reduce`

allows processes
`eliminate-destructors`

, `fertilize`

, `generalize`

, and
`eliminate-irrelevance`

.

**Remark:** 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, but might remain unless there is pressure to
fix it).