Basic theorems about faig-partial-eval-alist.
Theorem:
(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:
(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:
(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:
(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:
(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:
(defthm alist-keys-faig-partial-eval-alist (equal (alist-keys (faig-partial-eval-alist al env)) (alist-keys al)))