Basic theorems about aig-eval-alist.
Theorem:
(defthm aig-alist-equiv-implies-alist-equiv-aig-eval-alist-1 (implies (aig-alist-equiv x x-equiv) (alist-equiv (aig-eval-alist x env) (aig-eval-alist x-equiv env))) :rule-classes (:congruence))
Theorem:
(defthm aig-env-equiv-implies-equal-aig-eval-alist-2 (implies (aig-env-equiv env env-equiv) (equal (aig-eval-alist x env) (aig-eval-alist x env-equiv))) :rule-classes (:congruence))
Theorem:
(defthm aig-alist-equiv-implies-aig-alist-equiv-append-1 (implies (aig-alist-equiv a a-equiv) (aig-alist-equiv (append a b) (append a-equiv b))) :rule-classes (:congruence))
Theorem:
(defthm aig-alist-equiv-implies-aig-alist-equiv-append-2 (implies (aig-alist-equiv b b-equiv) (aig-alist-equiv (append a b) (append a b-equiv))) :rule-classes (:congruence))
Theorem:
(defthm aig-eval-alist-append (equal (aig-eval-alist (append a b) env) (append (aig-eval-alist a env) (aig-eval-alist b env))))
Theorem:
(defthm alist-keys-aig-eval-alist (equal (alist-keys (aig-eval-alist a b)) (alist-keys a)))