		Search-engine friendly clone of the ACL2 documentation.

Bfr-and

Bfr-binary-and

Signature
(bfr-binary-and x y) → bfr

Definitions and Theorems

Function: bfr-binary-and

(defun bfr-binary-and (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-binary-and))
    (declare (ignorable __function__))
    (mbe :logic (bfr-case :bdd (acl2::q-binary-and x y)
                          :aig (acl2::aig-and x y))
         :exec (cond ((not x) nil)
                     ((not y) nil)
                     ((and (eq x t) (eq y t)) t)
                     (t (bfr-case :bdd (acl2::q-binary-and x y)
                                  :aig (acl2::aig-and x y)))))))

Theorem: bfr-eval-bfr-binary-and

(defthm bfr-eval-bfr-binary-and
  (equal (bfr-eval (bfr-binary-and x y) env)
         (and (bfr-eval x env)
              (bfr-eval y env))))

Theorem: bfr-and-of-nil

(defthm bfr-and-of-nil
  (and (equal (bfr-binary-and nil y) nil)
       (equal (bfr-binary-and x nil) nil)))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-binary-and-1

(defthm bfr-equiv-implies-bfr-equiv-bfr-binary-and-1
  (implies (bfr-equiv x x-equiv)
           (bfr-equiv (bfr-binary-and x y)
                      (bfr-binary-and x-equiv y)))
  :rule-classes (:congruence))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-binary-and-2

(defthm bfr-equiv-implies-bfr-equiv-bfr-binary-and-2
  (implies (bfr-equiv y y-equiv)
           (bfr-equiv (bfr-binary-and x y)
                      (bfr-binary-and x y-equiv)))
  :rule-classes (:congruence))