		Search-engine friendly clone of the ACL2 documentation.

Bfr-or

Bfr-binary-or

Signature
(bfr-binary-or x y) → *

Definitions and Theorems

Function: bfr-binary-or

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

Theorem: bfr-eval-bfr-binary-or

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

Theorem: bfr-or-of-t

(defthm bfr-or-of-t
  (and (equal (bfr-binary-or t y) t)
       (equal (bfr-binary-or y t) t)))

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

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

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

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