`(4v-not-list x)` maps 4v-not across a list.

- Signature
(4v-not-list x) → *

This is an ordinary std::defprojection.

**Function: **

(defun 4v-not-list-exec (x acc) (declare (xargs :guard t)) (let ((__function__ '4v-not-list-exec)) (declare (ignorable __function__)) (if (consp x) (4v-not-list-exec (cdr x) (cons (4v-not (car x)) acc)) acc)))

**Function: **

(defun 4v-not-list-nrev (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard t)) (let ((__function__ '4v-not-list-nrev)) (declare (ignorable __function__)) (if (atom x) (nrev-fix nrev) (let ((nrev (nrev-push (4v-not (car x)) nrev))) (4v-not-list-nrev (cdr x) nrev)))))

**Function: **

(defun 4v-not-list (x) (declare (xargs :guard t)) (let ((__function__ '4v-not-list)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (cons (4v-not (car x)) (4v-not-list (cdr x))) nil) :exec (if (atom x) nil (with-local-nrev (4v-not-list-nrev x nrev))))))

**Theorem: **

(defthm 4v-not-list-nrev-removal (equal (4v-not-list-nrev x nrev) (append nrev (4v-not-list x))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-exec-removal (equal (4v-not-list-exec x acc) (revappend (4v-not-list x) acc)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-of-take (implies (<= (nfix n) (len x)) (equal (4v-not-list (take n x)) (take n (4v-not-list x)))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm set-equiv-congruence-over-4v-not-list (implies (set-equiv x y) (set-equiv (4v-not-list x) (4v-not-list y))) :rule-classes ((:congruence)))

**Theorem: **

(defthm subsetp-of-4v-not-list-when-subsetp (implies (subsetp x y) (subsetp (4v-not-list x) (4v-not-list y))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm member-of-4v-not-in-4v-not-list (implies (member k x) (member (4v-not k) (4v-not-list x))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-of-rev (equal (4v-not-list (rev x)) (rev (4v-not-list x))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-of-list-fix (equal (4v-not-list (list-fix x)) (4v-not-list x)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-of-append (equal (4v-not-list (append a b)) (append (4v-not-list a) (4v-not-list b))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm cdr-of-4v-not-list (equal (cdr (4v-not-list x)) (4v-not-list (cdr x))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm car-of-4v-not-list (equal (car (4v-not-list x)) (and (consp x) (4v-not (car x)))) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-under-iff (iff (4v-not-list x) (consp x)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm consp-of-4v-not-list (equal (consp (4v-not-list x)) (consp x)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm len-of-4v-not-list (equal (len (4v-not-list x)) (len x)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm true-listp-of-4v-not-list (true-listp (4v-not-list x)) :rule-classes :type-prescription)

**Theorem: **

(defthm 4v-not-list-when-not-consp (implies (not (consp x)) (equal (4v-not-list x) nil)) :rule-classes ((:rewrite)))

**Theorem: **

(defthm 4v-not-list-of-cons (equal (4v-not-list (cons a b)) (cons (4v-not a) (4v-not-list b))) :rule-classes ((:rewrite)))