		Search-engine friendly clone of the ACL2 documentation.

Bfr-ite

Bfr-ite-fn

Signature
(bfr-ite-fn x y z) → bfr

Definitions and Theorems

Function: bfr-ite-fn

(defun bfr-ite-fn (x y z)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-ite-fn))
    (declare (ignorable __function__))
    (mbe :logic
         (bfr-case :bdd (acl2::q-ite x y z)
                   :aig (cond ((eq x t) y)
                              ((eq x nil) z)
                              (t (acl2::aig-ite x y z))))
         :exec
         (if (booleanp x)
             (if x y z)
           (bfr-case :bdd (acl2::q-ite x y z)
                     :aig (acl2::aig-ite x y z))))))

Theorem: bfr-eval-bfr-ite-fn

(defthm bfr-eval-bfr-ite-fn
  (equal (bfr-eval (bfr-ite-fn x y z) env)
         (if (bfr-eval x env)
             (bfr-eval y env)
           (bfr-eval z env))))

Theorem: bfr-ite-fn-bools

(defthm bfr-ite-fn-bools
  (and (equal (bfr-ite-fn t y z) y)
       (equal (bfr-ite-fn nil y z) z)))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-ite-fn-1

(defthm bfr-equiv-implies-bfr-equiv-bfr-ite-fn-1
  (implies (bfr-equiv x x-equiv)
           (bfr-equiv (bfr-ite-fn x y z)
                      (bfr-ite-fn x-equiv y z)))
  :rule-classes (:congruence))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-ite-fn-2

(defthm bfr-equiv-implies-bfr-equiv-bfr-ite-fn-2
  (implies (bfr-equiv y y-equiv)
           (bfr-equiv (bfr-ite-fn x y z)
                      (bfr-ite-fn x y-equiv z)))
  :rule-classes (:congruence))

Theorem: bfr-equiv-implies-bfr-equiv-bfr-ite-fn-3

(defthm bfr-equiv-implies-bfr-equiv-bfr-ite-fn-3
  (implies (bfr-equiv z z-equiv)
           (bfr-equiv (bfr-ite-fn x y z)
                      (bfr-ite-fn x y z-equiv)))
  :rule-classes (:congruence))