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.