		Search-engine friendly clone of the ACL2 documentation.

Aig-implies

Aig-implies-fn

Signature
(aig-implies-fn x y) → aig

Definitions and Theorems

Function: aig-implies-fn

(defun aig-implies-fn (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-implies-fn))
    (declare (ignorable __function__))
    (aig-not (aig-and x (aig-not y)))))

Theorem: aig-eval-implies

(defthm aig-eval-implies
  (equal (aig-eval (aig-implies-fn x y) env)
         (implies (aig-eval x env)
                  (aig-eval y env))))

Theorem: aig-eval-implies-nil

(defthm aig-eval-implies-nil
  (equal (aig-implies-fn nil x) t))