		Search-engine friendly clone of the ACL2 documentation.

Bfr-not

Construct the NOT of a BFR.

Signature
(bfr-not x) → bfr

Definitions and Theorems

Function: bfr-not

(defun bfr-not (x)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-not))
    (declare (ignorable __function__))
    (mbe :logic
         (bfr-case :bdd (acl2::q-not x)
                   :aig (acl2::aig-not x))
         :exec
         (if (booleanp x)
             (not x)
           (bfr-case :bdd (acl2::q-not x)
                     :aig (acl2::aig-not x))))))

Theorem: bfr-eval-bfr-not

(defthm bfr-eval-bfr-not
  (equal (bfr-eval (bfr-not x) env)
         (not (bfr-eval x env))))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-not-1

(defthm bfr-equiv-implies-bfr-equiv-bfr-not-1
  (implies (bfr-equiv x x-equiv)
           (bfr-equiv (bfr-not x)
                      (bfr-not x-equiv)))
  :rule-classes (:congruence))