		Search-engine friendly clone of the ACL2 documentation.

Rewriting

4veclist-quote

(4veclist-quote x) maps svex-quote across a list.

Signature
(4veclist-quote x) → svexes
Arguments: x — Guard (4veclist-p x).
Returns: svexes — Type (svexlist-p svexes).

This is an ordinary defprojection.

Definitions and Theorems

Function: 4veclist-quote-exec

(defun 4veclist-quote-exec (x acc)
  (declare (xargs :guard (4veclist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ '4veclist-quote-exec))
    (declare (ignorable __function__))
    (if (consp x)
        (4veclist-quote-exec (cdr x)
                             (cons (svex-quote (car x)) acc))
      acc)))

Function: 4veclist-quote-nrev

(defun 4veclist-quote-nrev (x acl2::nrev)
  (declare (xargs :stobjs (acl2::nrev)))
  (declare (xargs :guard (4veclist-p x)))
  (declare (xargs :guard t))
  (let ((__function__ '4veclist-quote-nrev))
    (declare (ignorable __function__))
    (if (atom x)
        (acl2::nrev-fix acl2::nrev)
      (let ((acl2::nrev (acl2::nrev-push (svex-quote (car x))
                                         acl2::nrev)))
        (4veclist-quote-nrev (cdr x)
                             acl2::nrev)))))

Function: 4veclist-quote

(defun 4veclist-quote (x)
 (declare (xargs :guard (4veclist-p x)))
 (declare (xargs :guard t))
 (let ((__function__ '4veclist-quote))
  (declare (ignorable __function__))
  (mbe
    :logic
    (if (consp x)
        (cons (svex-quote (car x))
              (4veclist-quote (cdr x)))
      nil)
    :exec
    (if (atom x)
        nil
      (acl2::with-local-nrev (4veclist-quote-nrev x acl2::nrev))))))

Theorem: svexlist-p-of-4veclist-quote

(defthm svexlist-p-of-4veclist-quote
  (b* ((svexes (4veclist-quote x)))
    (svexlist-p svexes))
  :rule-classes :rewrite)

Theorem: 4veclist-quote-of-4veclist-fix-x

(defthm 4veclist-quote-of-4veclist-fix-x
  (equal (4veclist-quote (4veclist-fix x))
         (4veclist-quote x)))

Theorem: 4veclist-quote-4veclist-equiv-congruence-on-x

(defthm 4veclist-quote-4veclist-equiv-congruence-on-x
  (implies (4veclist-equiv x x-equiv)
           (equal (4veclist-quote x)
                  (4veclist-quote x-equiv)))
  :rule-classes :congruence)

Theorem: set-equiv-congruence-over-4veclist-quote

(defthm set-equiv-congruence-over-4veclist-quote
  (implies (set-equiv x y)
           (set-equiv (4veclist-quote x)
                      (4veclist-quote y)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-4veclist-quote-when-subsetp

(defthm subsetp-of-4veclist-quote-when-subsetp
  (implies (subsetp x y)
           (subsetp (4veclist-quote x)
                    (4veclist-quote y)))
  :rule-classes ((:rewrite)))

Theorem: member-of-svex-quote-in-4veclist-quote

(defthm member-of-svex-quote-in-4veclist-quote
  (implies (member acl2::k x)
           (member (svex-quote acl2::k)
                   (4veclist-quote x)))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-nrev-removal

(defthm 4veclist-quote-nrev-removal
  (equal (4veclist-quote-nrev x acl2::nrev)
         (append acl2::nrev (4veclist-quote x)))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-exec-removal

(defthm 4veclist-quote-exec-removal
  (equal (4veclist-quote-exec x acl2::acc)
         (revappend (4veclist-quote x)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-of-rev

(defthm 4veclist-quote-of-rev
  (equal (4veclist-quote (rev x))
         (rev (4veclist-quote x)))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-of-list-fix

(defthm 4veclist-quote-of-list-fix
  (equal (4veclist-quote (list-fix x))
         (4veclist-quote x))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-of-append

(defthm 4veclist-quote-of-append
  (equal (4veclist-quote (append acl2::a acl2::b))
         (append (4veclist-quote acl2::a)
                 (4veclist-quote acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-4veclist-quote

(defthm cdr-of-4veclist-quote
  (equal (cdr (4veclist-quote x))
         (4veclist-quote (cdr x)))
  :rule-classes ((:rewrite)))

Theorem: car-of-4veclist-quote

(defthm car-of-4veclist-quote
  (equal (car (4veclist-quote x))
         (and (consp x) (svex-quote (car x))))
  :rule-classes ((:rewrite)))

Theorem: 4veclist-quote-under-iff

(defthm 4veclist-quote-under-iff
  (iff (4veclist-quote x) (consp x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-4veclist-quote

(defthm consp-of-4veclist-quote
  (equal (consp (4veclist-quote x))
         (consp x))
  :rule-classes ((:rewrite)))

Theorem: len-of-4veclist-quote

(defthm len-of-4veclist-quote
  (equal (len (4veclist-quote x)) (len x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-4veclist-quote

(defthm true-listp-of-4veclist-quote
  (true-listp (4veclist-quote x))
  :rule-classes :type-prescription)

Theorem: 4veclist-quote-when-not-consp

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

Theorem: 4veclist-quote-of-cons

(defthm 4veclist-quote-of-cons
  (equal (4veclist-quote (cons acl2::a acl2::b))
         (cons (svex-quote acl2::a)
               (4veclist-quote acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: vars-of-4veclist-quote

(defthm vars-of-4veclist-quote
  (b* ((?svexes (4veclist-quote x)))
    (equal (svexlist-vars svexes) nil)))