		Search-engine friendly clone of the ACL2 documentation.

Aig-eval

Aig-eval-thms

Basic theorems about aig-eval.

Definitions and Theorems

Theorem: aig-equiv-implies-equal-aig-eval-1

(defthm aig-equiv-implies-equal-aig-eval-1
  (implies (aig-equiv x x-equiv)
           (equal (aig-eval x env)
                  (aig-eval x-equiv env)))
  :rule-classes (:congruence))

Theorem: aig-env-equiv-implies-iff-aig-env-lookup-2

(defthm aig-env-equiv-implies-iff-aig-env-lookup-2
  (implies (aig-env-equiv al al-equiv)
           (iff (aig-env-lookup key al)
                (aig-env-lookup key al-equiv)))
  :rule-classes (:congruence))

Theorem: aig-env-equiv-implies-equal-aig-eval-2

(defthm aig-env-equiv-implies-equal-aig-eval-2
  (implies (aig-env-equiv env env-equiv)
           (equal (aig-eval x env)
                  (aig-eval x env-equiv)))
  :rule-classes (:congruence))

Theorem: aig-eval-append-when-not-intersecting-alist-keys

(defthm aig-eval-append-when-not-intersecting-alist-keys
  (implies (not (intersectp-equal (alist-keys env)
                                  (aig-vars x)))
           (equal (aig-eval x (append env rest))
                  (aig-eval x rest))))