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