		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*))