		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-and-list-dumb

(4vs-and-list-dumb sexprs) reduction ands together all the sexprs in the list x, producing a single sexpr representing their conjunction.

This is dumb in that it doesn't do the simple optimizations of 4vs-and-list, but it has a nicer 4v-sexpr-vars theorem because of this.

Definitions and Theorems

Function: 4vs-and-list-dumb

(defun 4vs-and-list-dumb (sexprs)
       (declare (xargs :guard t))
       (if (atom sexprs)
           *4vt-sexpr*
           (4vs-and-dumb (car sexprs)
                         (4vs-and-list-dumb (cdr sexprs)))))

Theorem: 4v-sexpr-eval-of-4vs-and-list-dumb

(defthm 4v-sexpr-eval-of-4vs-and-list-dumb
        (equal (4v-sexpr-eval (4vs-and-list-dumb sexprs)
                              env)
               (4v-and-list (4v-sexpr-eval-list sexprs env))))

Theorem: 4v-sexpr-vars-of-4vs-and-list-dumb

(defthm 4v-sexpr-vars-of-4vs-and-list-dumb
        (equal (4v-sexpr-vars (4vs-and-list-dumb x))
               (4v-sexpr-vars-list x)))