Theorem:
(defthm svexlist-monotonic-on-vars-necc (implies (svexlist-monotonic-on-vars vars x) (implies (and (svex-env-<<= env1 env2) (svex-envs-agree-except vars env1 env2)) (4veclist-<<= (svexlist-eval x env1) (svexlist-eval x env2)))))
Theorem:
(defthm svexlist-monotonic-on-vars-of-svarlist-fix-vars (equal (svexlist-monotonic-on-vars (svarlist-fix vars) x) (svexlist-monotonic-on-vars vars x)))
Theorem:
(defthm svexlist-monotonic-on-vars-svarlist-equiv-congruence-on-vars (implies (svarlist-equiv vars vars-equiv) (equal (svexlist-monotonic-on-vars vars x) (svexlist-monotonic-on-vars vars-equiv x))) :rule-classes :congruence)
Theorem:
(defthm set-equiv-implies-equal-svexlist-monotonic-on-vars-1 (implies (set-equiv vars vars-equiv) (equal (svexlist-monotonic-on-vars vars x) (svexlist-monotonic-on-vars vars-equiv x))) :rule-classes (:congruence))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-monotonic-on-vars-2 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-monotonic-on-vars vars x) (svexlist-monotonic-on-vars vars x-equiv))) :rule-classes (:congruence))