• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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-x
          • 4vs-t
          • 4vs-ite*-dumb
          • 4vs-f
          • 4vs-iff
          • 4vs-buf
          • 4vs-xor
          • 4vs-or
          • 4vs-implies-lists
          • 4vs-implies
          • 4vs-xor-lists
          • 4vs-or-lists
          • 4vs-or-list
          • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

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