		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-and-list

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

Definitions and Theorems

Function: 4vs-and-list

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

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

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

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

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