		Search-engine friendly clone of the ACL2 documentation.

Faig-eval-alist

Faig-eval-alist-thms

Definitions and Theorems

Theorem: faig-eval-alist-append

(defthm faig-eval-alist-append
  (equal (faig-eval-alist (append a b) env)
         (append (faig-eval-alist a env)
                 (faig-eval-alist b env))))

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

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

Theorem: lookup-in-faig-eval-alist

(defthm lookup-in-faig-eval-alist
  (equal (hons-assoc-equal k (faig-eval-alist x env))
         (and (hons-assoc-equal k x)
              (cons k
                    (faig-eval (cdr (hons-assoc-equal k x))
                               env)))))

Theorem: faig-alist-equiv-implies-alist-equiv-faig-eval-alist-1

(defthm faig-alist-equiv-implies-alist-equiv-faig-eval-alist-1
  (implies (faig-alist-equiv x x-equiv)
           (alist-equiv (faig-eval-alist x env)
                        (faig-eval-alist x-equiv env)))
  :rule-classes (:congruence))

Theorem: alist-keys-faig-eval-alist

(defthm alist-keys-faig-eval-alist
  (equal (alist-keys (faig-eval-alist al env))
         (alist-keys al)))