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