		Search-engine friendly clone of the ACL2 documentation.

Aig-and

Aig-and-pass1

Level 1 simplifications.

Signature
(aig-and-pass1 x y) → (mv hit ans)

See also aig-and-dumb, which tries to apply these same reductions, but otherwise just gives up, and doesn't report whether it has succeded or not.

Definitions and Theorems

Function: aig-and-pass1$inline

(defun aig-and-pass1$inline (x y)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-and-pass1))
    (declare (ignorable __function__))
    (cond ((eq x nil) (mv t nil))
          ((eq y nil) (mv t nil))
          ((eq x t) (mv t y))
          ((eq y t) (mv t x))
          ((hons-equal x y) (mv t x))
          ((aig-negation-p x y) (mv t nil))
          (t (mv nil nil)))))

Theorem: aig-and-pass1-correct

(defthm aig-and-pass1-correct
  (b* (((mv ?hit ?ans)
        (aig-and-pass1$inline x y)))
    (implies hit
             (equal (aig-eval ans env)
                    (and (aig-eval x env)
                         (aig-eval y env)))))
  :rule-classes nil)