• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
          • 4vs-not-list
          • 4vs-onehot
          • 4vs-ite*-list-dumb
          • 4vs-and-list-dumb
          • 4vs-not
          • 4vs-and-list
          • 4vs-and-dumb
          • 4vs-and
          • 4vs-zif-dumb
          • 4vs-z
          • 4vs-ite*-dumb
          • 4vs-x
          • 4vs-t
          • 4vs-f
          • 4vs-xor
          • 4vs-or
          • 4vs-iff
          • 4vs-buf
          • 4vs-implies-lists
          • 4vs-xor-lists
          • 4vs-or-lists
          • 4vs-or-list
          • 4vs-implies
          • 4vs-iff-lists
          • 4vs-and-lists
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 4vs-constructors

4vs-not-list

(4vs-not-list x) maps 4vs-not across a list.

Signature

(4vs-not-list x) → *

This is an ordinary std::defprojection.

Definitions and Theorems

Function: 4vs-not-list-exec

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

Function: 4vs-not-list-nrev

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

Function: 4vs-not-list

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

Theorem: 4vs-not-list-nrev-removal

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

Theorem: 4vs-not-list-exec-removal

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

Theorem: 4vs-not-list-of-take

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

Theorem: set-equiv-congruence-over-4vs-not-list

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

Theorem: subsetp-of-4vs-not-list-when-subsetp

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

Theorem: member-of-4vs-not-in-4vs-not-list

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

Theorem: 4vs-not-list-of-rev

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

Theorem: 4vs-not-list-of-list-fix

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

Theorem: 4vs-not-list-of-append

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

Theorem: cdr-of-4vs-not-list

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

Theorem: car-of-4vs-not-list

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

Theorem: 4vs-not-list-under-iff

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

Theorem: consp-of-4vs-not-list

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

Theorem: len-of-4vs-not-list

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

Theorem: true-listp-of-4vs-not-list

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

Theorem: 4vs-not-list-when-not-consp

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

Theorem: 4vs-not-list-of-cons

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