		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-negation-p

(aig-negation-p x y) determines if the AIGs x and y are (syntactically) negations of one another.

Signature
(aig-negation-p x y) → *

Definitions and Theorems

Function: aig-negation-p$inline

(defun aig-negation-p$inline (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-negation-p))
    (declare (ignorable __function__))
    (or (and (consp y)
             (eq (cdr y) nil)
             (hons-equal (car y) x))
        (and (consp x)
             (eq (cdr x) nil)
             (hons-equal (car x) y)))))

Theorem: aig-negation-p-symmetric

(defthm aig-negation-p-symmetric
  (equal (aig-negation-p x y)
         (aig-negation-p y x)))

Theorem: aig-negation-p-correct-1

(defthm aig-negation-p-correct-1
  (implies (and (aig-negation-p x y)
                (aig-eval x env))
           (equal (aig-eval y env) nil)))

Theorem: aig-negation-p-correct-2

(defthm aig-negation-p-correct-2
  (implies (and (aig-negation-p x y)
                (not (aig-eval x env)))
           (equal (aig-eval y env) t)))