• 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-tristate
        • 4v-zif
        • 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)))