` `

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.
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 by the next release).