		Search-engine friendly clone of the ACL2 documentation.

ACL2-pc::bash

(atomic macro) call the ACL2 theorem prover's simplifier

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