:prove is t (the
default), then the proof will succeed entirely using bdds or else
it will fail immediately. See bdd.
prove the current goal using bdds
Major Section: PROOF-CHECKER-COMMANDS
Examples: bdd (bdd :vars nil :bdd-constructors (cons) :prove t :literal :all)
The general form is as shown in the latter example above, but with
any keyword-value pairs omitted and with values as described for the
:bdd hint; see hints.
This command simply calls the theorem prover with the indicated bdd
hint for the top-level goal. Note that if :prove is t (the
default), then the proof will succeed entirely using bdds or else
it will fail immediately. See bdd.