		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svexlist-<<=

Definitions and Theorems

Theorem: svexlist-<<=-necc

(defthm svexlist-<<=-necc
  (implies (svexlist-<<= x y)
           (4veclist-<<= (svexlist-eval x env)
                         (svexlist-eval y env))))

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

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

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

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

Theorem: svex-<<=-car-when-svexlist-<<=

(defthm svex-<<=-car-when-svexlist-<<=
  (implies (svexlist-<<= x y)
           (svex-<<= (car x) (car y))))

Theorem: svexlist-<<=-cdr-when-svexlist-<<=

(defthm svexlist-<<=-cdr-when-svexlist-<<=
  (implies (svexlist-<<= x y)
           (svexlist-<<= (cdr x) (cdr y))))

Theorem: svex-<<=-nth-when-svexlist-<<=

(defthm svex-<<=-nth-when-svexlist-<<=
  (implies (svexlist-<<= x y)
           (svex-<<= (nth n x) (nth n y))))

Theorem: svexlist-<<=-of-cons

(defthm svexlist-<<=-of-cons
  (implies (and (svex-<<= x1 x2)
                (svexlist-<<= y1 y2))
           (svexlist-<<= (cons x1 y1)
                         (cons x2 y2))))

Theorem: svexlist-<<=-refl

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

Theorem: svexlist-<<=-transitive-1

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

Theorem: svexlist-<<=-transitive-2

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

Theorem: svexlist-<<=-asymm

(defthm svexlist-<<=-asymm
  (implies (and (svexlist-<<= x y)
                (equal (len x) (len y)))
           (iff (svexlist-<<= y x)
                (svexlist-eval-equiv y x))))