		Search-engine friendly clone of the ACL2 documentation.

4v-and-list

(4v-and-list x) conjoins a list of 4vp constants.

Function: 4v-and-list

(defun 4v-and-list (x)
       (declare (xargs :guard t))
       (if (atom x)
           (4vt)
           (4v-and (car x) (4v-and-list (cdr x)))))

Theorem: 4v-and-list-when-atom

(defthm 4v-and-list-when-atom
        (implies (atom x)
                 (equal (4v-and-list x) (4vt))))

Theorem: 4v-and-list-of-cons

(defthm 4v-and-list-of-cons
        (equal (4v-and-list (cons a x))
               (4v-and a (4v-and-list x))))

Theorem: 4v-and-list-never-z

(defthm 4v-and-list-never-z
        (equal (equal (4v-and-list x) (4vz))
               nil))