		Search-engine friendly clone of the ACL2 documentation.

Faig-partial-eval-alist

Faig-partial-eval-alist-thms

Basic theorems about faig-partial-eval-alist.

Definitions and Theorems

Theorem: faig-eval-alist-of-faig-partial-eval-alist

(defthm faig-eval-alist-of-faig-partial-eval-alist
  (equal (faig-eval-alist (faig-partial-eval-alist x al1)
                          al2)
         (faig-eval-alist x (append al1 al2))))

Theorem: lookup-in-faig-partial-eval-alist

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

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

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

Theorem: alist-equiv-implies-equal-faig-partial-eval-alist-2

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

Theorem: faig-partial-eval-alist-faig-partial-eval-alist

(defthm faig-partial-eval-alist-faig-partial-eval-alist
  (faig-alist-equiv
       (faig-partial-eval-alist (faig-partial-eval-alist x al1)
                                al2)
       (faig-partial-eval-alist x (append al1 al2))))

Theorem: alist-keys-faig-partial-eval-alist

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