		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-monotonic-on-vars

Definitions and Theorems

Theorem: svex-monotonic-on-vars-necc

(defthm svex-monotonic-on-vars-necc
  (implies (svex-monotonic-on-vars vars x)
           (implies (and (svex-env-<<= env1 env2)
                         (svex-envs-agree-except vars env1 env2))
                    (4vec-<<= (svex-eval x env1)
                              (svex-eval x env2)))))

Theorem: svex-monotonic-on-vars-of-svarlist-fix-vars

(defthm svex-monotonic-on-vars-of-svarlist-fix-vars
  (equal (svex-monotonic-on-vars (svarlist-fix vars)
                                 x)
         (svex-monotonic-on-vars vars x)))

Theorem: svex-monotonic-on-vars-svarlist-equiv-congruence-on-vars

(defthm svex-monotonic-on-vars-svarlist-equiv-congruence-on-vars
  (implies (svarlist-equiv vars vars-equiv)
           (equal (svex-monotonic-on-vars vars x)
                  (svex-monotonic-on-vars vars-equiv x)))
  :rule-classes :congruence)

Theorem: set-equiv-implies-equal-svex-monotonic-on-vars-1

(defthm set-equiv-implies-equal-svex-monotonic-on-vars-1
  (implies (set-equiv vars vars-equiv)
           (equal (svex-monotonic-on-vars vars x)
                  (svex-monotonic-on-vars vars-equiv x)))
  :rule-classes (:congruence))

Theorem: svex-eval-equiv-implies-equal-svex-monotonic-on-vars-2

(defthm svex-eval-equiv-implies-equal-svex-monotonic-on-vars-2
  (implies (svex-eval-equiv x x-equiv)
           (equal (svex-monotonic-on-vars vars x)
                  (svex-monotonic-on-vars vars x-equiv)))
  :rule-classes (:congruence))