		Search-engine friendly clone of the ACL2 documentation.

Faig-eval

Faig-eval-thms

Basic theorems about faig-eval.

Definitions and Theorems

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

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

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

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