		Search-engine friendly clone of the ACL2 documentation.

Aig-ite

Aig-ite-fn

Signature
(aig-ite-fn a b c) → aig

Definitions and Theorems

Function: aig-ite-fn

(defun aig-ite-fn (a b c)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-ite-fn))
    (declare (ignorable __function__))
    (cond ((eq a t) b)
          ((eq a nil) c)
          ((hons-equal b c) b)
          ((eq b t) (aig-or a c))
          (t (aig-or (aig-and a b)
                     (aig-and (aig-not a) c))))))

Theorem: aig-eval-ite

(defthm aig-eval-ite
  (iff (aig-eval (aig-ite-fn a b c) env)
       (if (aig-eval a env)
           (aig-eval b env)
         (aig-eval c env))))

Theorem: aig-ite-of-constants

(defthm aig-ite-of-constants
  (and (equal (aig-ite-fn t b c) b)
       (equal (aig-ite-fn nil b c) c)))