		Search-engine friendly clone of the ACL2 documentation.

Sexpr-rewriting

sexpr-rewrites

A useful set of 4v-s-expression rewrite rules, proven correct.

Definitions and Theorems

Theorem: nth-4v-sexpr-eval-list

(defthm nth-4v-sexpr-eval-list
  (equal (nth n (4v-sexpr-eval-list x env))
         (if (< (nfix n) (len x))
             (4v-sexpr-eval (nth n x) env)
           nil)))

Theorem: 4v-sexpr-rewritesp-sexpr-rewrites

(defthm 4v-sexpr-rewritesp-sexpr-rewrites
  (4v-sexpr-rewrite-alistp *sexpr-rewrites*))