• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
      • 4v-monotonicity
      • 4v-operations
        • 4v-ite
        • 4v-res
        • 4v-not-list
        • 4v-unfloat
        • 4v-wand
        • 4v-wor
        • 4v-zif
        • 4v-tristate
        • 4v-xdet
        • 4v-xor
        • 4v-iff
        • 4v-and
        • 4v-or
        • 4v-not
        • 4v-pullup
        • 4v-and-list
        • 4v-ite*
      • 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

• 4v-operations

4v-not-list

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

Signature

(4v-not-list x) → *

This is an ordinary std::defprojection.

Definitions and Theorems

Function: 4v-not-list-exec

(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: 4v-not-list-nrev

(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: 4v-not-list

(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: 4v-not-list-nrev-removal

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

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

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

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

(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: set-equiv-congruence-over-4v-not-list

(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: subsetp-of-4v-not-list-when-subsetp

(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: member-of-4v-not-in-4v-not-list

(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: 4v-not-list-of-rev

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

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

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

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

(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: cdr-of-4v-not-list

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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