		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-ovmonotonic

Definitions and Theorems

Theorem: svex-ovmonotonic-necc

(defthm svex-ovmonotonic-necc
  (implies (svex-ovmonotonic x)
           (implies (svex-env-ov<<= env1 env2)
                    (4vec-<<= (svex-eval x env1)
                              (svex-eval x env2)))))

Theorem: svex-eval-equiv-implies-equal-svex-ovmonotonic-1

(defthm svex-eval-equiv-implies-equal-svex-ovmonotonic-1
  (implies (svex-eval-equiv x x-equiv)
           (equal (svex-ovmonotonic x)
                  (svex-ovmonotonic x-equiv)))
  :rule-classes (:congruence))