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