Theorem:
(defthm svex-alist-ovmonotonic-necc (implies (svex-alist-ovmonotonic x) (implies (svex-env-ov<<= env1 env2) (svex-env-<<= (svex-alist-eval x env1) (svex-alist-eval x env2)))))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-ovmonotonic-1 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-ovmonotonic x) (svex-alist-ovmonotonic x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm lookup-when-svex-alist-ovmonotonic (implies (svex-alist-ovmonotonic x) (svex-ovmonotonic (svex-lookup k x))))
Theorem:
(defthm svex-compose-lookup-when-svex-alist-ovmonotonic (implies (and (svex-alist-ovmonotonic x) (not (svar-override-p k :test))) (svex-ovmonotonic (svex-compose-lookup k x))))
Theorem:
(defthm svex-env-ov<<=-of-append-<<= (implies (and (svex-env-ov<<= c d) (svex-env-<<= a b) (set-equiv (alist-keys (svex-env-fix a)) (alist-keys (svex-env-fix b))) (svarlist-nonoverride-p (alist-keys (svex-env-fix a)) :test)) (svex-env-ov<<= (append a c) (append b d))))
Theorem:
(defthm svex-compose-preserves-svex-ovmonotonic (implies (and (svex-ovmonotonic x) (svex-alist-ovmonotonic a) (svarlist-nonoverride-p (svex-alist-keys a) :test)) (svex-ovmonotonic (svex-compose x a))))
Theorem:
(defthm svexlist-compose-preserves-svexlist-ovmonotonic (implies (and (svexlist-ovmonotonic x) (svex-alist-ovmonotonic a) (svarlist-nonoverride-p (svex-alist-keys a) :test)) (svexlist-ovmonotonic (svexlist-compose x a))))
Theorem:
(defthm svex-alist-compose-preserves-svex-alist-ovmonotonic (implies (and (svex-alist-ovmonotonic x) (svex-alist-ovmonotonic a) (svarlist-nonoverride-p (svex-alist-keys a) :test)) (svex-alist-ovmonotonic (svex-alist-compose x a))))