		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-<<=

Definitions and Theorems

Theorem: svex-<<=-necc

(defthm svex-<<=-necc
  (implies (svex-<<= x y)
           (4vec-<<= (svex-eval x env)
                     (svex-eval y env))))

Theorem: svex-eval-equiv-implies-equal-svex-<<=-1

(defthm svex-eval-equiv-implies-equal-svex-<<=-1
  (implies (svex-eval-equiv x x-equiv)
           (equal (svex-<<= x y)
                  (svex-<<= x-equiv y)))
  :rule-classes (:congruence))

Theorem: svex-eval-equiv-implies-equal-svex-<<=-2

(defthm svex-eval-equiv-implies-equal-svex-<<=-2
  (implies (svex-eval-equiv y y-equiv)
           (equal (svex-<<= x y)
                  (svex-<<= x y-equiv)))
  :rule-classes (:congruence))

Theorem: svex-<<=-x

(defthm svex-<<=-x
  (svex-<<= (4vec-x) x))

Theorem: svex-<<=-refl

(defthm svex-<<=-refl (svex-<<= x x))

Theorem: svex-<<=-transitive-1

(defthm svex-<<=-transitive-1
  (implies (and (svex-<<= x y) (svex-<<= y z))
           (svex-<<= x z)))

Theorem: svex-<<=-transitive-2

(defthm svex-<<=-transitive-2
  (implies (and (svex-<<= y z) (svex-<<= x y))
           (svex-<<= x z)))

Theorem: svex-<<=-asymm

(defthm svex-<<=-asymm
  (implies (svex-<<= x y)
           (iff (svex-<<= y x)
                (svex-eval-equiv y x))))