Theorem:
(defthm svex-alist-monotonic-on-vars-necc (implies (svex-alist-monotonic-on-vars vars x) (implies (and (svex-env-<<= env1 env2) (svex-envs-agree-except vars env1 env2)) (svex-env-<<= (svex-alist-eval x env1) (svex-alist-eval x env2)))))
Theorem:
(defthm svex-alist-monotonic-on-vars-of-svarlist-fix-vars (equal (svex-alist-monotonic-on-vars (svarlist-fix vars) x) (svex-alist-monotonic-on-vars vars x)))
Theorem:
(defthm svex-alist-monotonic-on-vars-svarlist-equiv-congruence-on-vars (implies (svarlist-equiv vars vars-equiv) (equal (svex-alist-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars-equiv x))) :rule-classes :congruence)
Theorem:
(defthm set-equiv-implies-equal-svex-alist-monotonic-on-vars-1 (implies (set-equiv vars vars-equiv) (equal (svex-alist-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars-equiv x))) :rule-classes (:congruence))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-monotonic-on-vars-2 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm lookup-when-svex-alist-monotonic-on-vars (implies (svex-alist-monotonic-on-vars vars x) (svex-monotonic-on-vars vars (svex-lookup k x))))
Theorem:
(defthm svex-compose-lookup-when-svex-alist-monotonic-on-vars (implies (svex-alist-monotonic-on-vars vars x) (svex-monotonic-on-vars vars (svex-compose-lookup k x))))
Theorem:
(defthm svex-compose-preserves-svex-monotonic-on-vars (implies (and (svex-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars a) (subsetp-equal (svex-alist-keys a) (svarlist-fix vars))) (svex-monotonic-on-vars vars (svex-compose x a))))
Theorem:
(defthm svexlist-compose-preserves-svexlist-monotonic-on-vars (implies (and (svexlist-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars a) (subsetp-equal (svex-alist-keys a) (svarlist-fix vars))) (svexlist-monotonic-on-vars vars (svexlist-compose x a))))
Theorem:
(defthm svex-alist-compose-preserves-svex-alist-monotonic-on-vars (implies (and (svex-alist-monotonic-on-vars vars x) (svex-alist-monotonic-on-vars vars a) (subsetp-equal (svex-alist-keys a) (svarlist-fix vars))) (svex-alist-monotonic-on-vars vars (svex-alist-compose x a))))