		Search-engine friendly clone of the ACL2 documentation.

Svexlist-eval

Svexlist-eval-basics

Very basic list lemmas for svexlist-eval.

Definitions and Theorems

Theorem: svexlist-eval-when-atom-cheap

(defthm svexlist-eval-when-atom-cheap
  (implies (atom x)
           (equal (svexlist-eval x env) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: svexlist-eval-nil

(defthm svexlist-eval-nil
  (equal (svexlist-eval nil env) nil))

Theorem: car-of-svexlist-eval

(defthm car-of-svexlist-eval
  (4vec-equiv (car (svexlist-eval x env))
              (svex-eval (car x) env)))

Theorem: cdr-of-svexlist-eval

(defthm cdr-of-svexlist-eval
  (4veclist-equiv (cdr (svexlist-eval x env))
                  (svexlist-eval (cdr x) env)))

Theorem: svexlist-eval-of-cons

(defthm svexlist-eval-of-cons
  (equal (svexlist-eval (cons a b) env)
         (cons (svex-eval a env)
               (svexlist-eval b env))))

Theorem: consp-of-svexlist-eval

(defthm consp-of-svexlist-eval
  (equal (consp (svexlist-eval x env))
         (consp x)))

Theorem: svexlist-eval-under-iff

(defthm svexlist-eval-under-iff
  (iff (svexlist-eval x env) (consp x)))

Theorem: len-of-svexlist-eval

(defthm len-of-svexlist-eval
  (equal (len (svexlist-eval x env))
         (len x)))

Theorem: svexlist-eval-of-append

(defthm svexlist-eval-of-append
  (equal (svexlist-eval (append a b) env)
         (append (svexlist-eval a env)
                 (svexlist-eval b env))))

Theorem: svex-eval-of-nth

(defthm svex-eval-of-nth
  (4vec-equiv (nth n (svexlist-eval x env))
              (svex-eval (nth n x) env)))

Theorem: nthcdr-of-svexlist-eval

(defthm nthcdr-of-svexlist-eval
  (equal (nthcdr n (svexlist-eval x env))
         (svexlist-eval (nthcdr n x) env)))