Basic theorems about aig-partial-eval-alist.
Theorem:
(defthm lookup-in-aig-partial-eval-alist (equal (hons-assoc-equal k (aig-partial-eval-alist x env)) (and (hons-assoc-equal k x) (cons k (aig-partial-eval (cdr (hons-assoc-equal k x)) env)))))
Theorem:
(defthm aig-alist-equiv-implies-aig-alist-equiv-aig-partial-eval-alist-1 (implies (aig-alist-equiv x x-equiv) (aig-alist-equiv (aig-partial-eval-alist x al) (aig-partial-eval-alist x-equiv al))) :rule-classes (:congruence))
Theorem:
(defthm aig-eval-alist-of-aig-partial-eval-alist (equal (aig-eval-alist (aig-partial-eval-alist x al1) al2) (aig-eval-alist x (append al1 al2))))
Theorem:
(defthm aig-partial-eval-alist-aig-partial-eval-alist (aig-alist-equiv (aig-partial-eval-alist (aig-partial-eval-alist x al1) al2) (aig-partial-eval-alist x (append al1 al2))))