### ACL2-PC::PROVE

(primitive)
` `

call the ACL2 theorem prover to prove the current goal
Major Section: PROOF-CHECKER-COMMANDS

Examples:
prove -- attempt to prove the current goal
(prove :otf-flg t
:hints (("Subgoal 2" :by foo) ("Subgoal 1" :use bar)))
-- attempt to prove the current goal, with the indicated hints
and with OTF-FLG set
General Form:
(prove &rest rest-args)

Attempt to prove the current goal, where `rest-args`

is as in the
keyword arguments to `defthm`

except that only `:hints`

and `:otf-flg`

are
allowed. The command succeeds exactly when the corresponding `defthm`

would succeed, except that it is all right for some goals to be
given ``bye''s. Each goal given a ``bye'' will be turned into a new
subgoal. (See hints for an explanation of `:by`

hints.)
**Note:** Use `(= t)`

instead if you are not at the top of the
conclusion. Also note that if there are any hypotheses in the
current goal, then what is actually attempted is a proof of
`(implies hyps conc)`

, where `hyps`

is the conjunction of the
top-level hypotheses and `conc`

is the goal's conclusion.

**Note:** It is allowed to use abbreviations in the hints.