		Search-engine friendly clone of the ACL2 documentation.

Aig-or

Aig-binary-or

(aig-binary-or x y) constructs an AIG representing (or x y).

Signature
(aig-binary-or x y) → aig

Definitions and Theorems

Function: aig-binary-or

(defun aig-binary-or (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-binary-or))
    (declare (ignorable __function__))
    (cond ((eq x nil) y)
          ((eq y nil) x)
          (t (aig-not (aig-and (aig-not x) (aig-not y)))))))

Theorem: aig-eval-or

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

Theorem: aig-or-constants

(defthm aig-or-constants
  (and (equal (aig-binary-or nil x) x)
       (equal (aig-binary-or x nil) x)
       (equal (aig-binary-or x t) t)
       (equal (aig-binary-or t x) t)))