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