		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-assignlist-check-selfassigns

(vl-assignlist-check-selfassigns x ss) applies vl-assign-check-selfassigns to every member of the list x, and appends together all the resulting lists.

This is an ordinary defmapappend.

Function: vl-assignlist-check-selfassigns

(defun vl-assignlist-check-selfassigns (x ss)
 (declare (xargs :guard (and (vl-assignlist-p x)
                             (vl-scopestack-p ss))))
 (mbe
   :logic
   (if (consp x)
       (append (vl-assign-check-selfassigns (car x) ss)
               (vl-assignlist-check-selfassigns (cdr x)
                                                ss))
     nil)
   :exec (reverse (vl-assignlist-check-selfassigns-exec x ss nil))))

Definitions and Theorems

Function: vl-assignlist-check-selfassigns-exec

(defun vl-assignlist-check-selfassigns-exec (x ss acc)
  (declare (xargs :guard (and (vl-assignlist-p x)
                              (vl-scopestack-p ss))))
  (if (consp x)
      (vl-assignlist-check-selfassigns-exec
           (cdr x)
           ss
           (revappend (vl-assign-check-selfassigns (car x) ss)
                      acc))
    acc))

Function: vl-assignlist-check-selfassigns

(defun vl-assignlist-check-selfassigns (x ss)
 (declare (xargs :guard (and (vl-assignlist-p x)
                             (vl-scopestack-p ss))))
 (mbe
   :logic
   (if (consp x)
       (append (vl-assign-check-selfassigns (car x) ss)
               (vl-assignlist-check-selfassigns (cdr x)
                                                ss))
     nil)
   :exec (reverse (vl-assignlist-check-selfassigns-exec x ss nil))))

Theorem: vl-assignlist-check-selfassigns-exec-removal

(defthm vl-assignlist-check-selfassigns-exec-removal
  (equal (vl-assignlist-check-selfassigns-exec acl2::x ss acl2::acc)
         (revappend (vl-assignlist-check-selfassigns acl2::x ss)
                    acl2::acc))
  :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-vl-assignlist-check-selfassigns

(defthm set-equiv-congruence-over-vl-assignlist-check-selfassigns
  (implies (set-equiv acl2::x acl2::y)
           (set-equiv (vl-assignlist-check-selfassigns acl2::x ss)
                      (vl-assignlist-check-selfassigns acl2::y ss)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-vl-assignlist-check-selfassigns-when-subsetp

(defthm subsetp-of-vl-assignlist-check-selfassigns-when-subsetp
  (implies (subsetp acl2::x acl2::y)
           (subsetp (vl-assignlist-check-selfassigns acl2::x ss)
                    (vl-assignlist-check-selfassigns acl2::y ss)))
  :rule-classes ((:rewrite)))

Theorem: member-in-vl-assignlist-check-selfassigns

(defthm member-in-vl-assignlist-check-selfassigns
  (implies (and (member acl2::k
                        (vl-assign-check-selfassigns acl2::j ss))
                (member acl2::j acl2::x))
           (member acl2::k
                   (vl-assignlist-check-selfassigns acl2::x ss)))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-list-fix

(defthm vl-assignlist-check-selfassigns-of-list-fix
  (equal (vl-assignlist-check-selfassigns (list-fix acl2::x)
                                          ss)
         (vl-assignlist-check-selfassigns acl2::x ss))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-append

(defthm vl-assignlist-check-selfassigns-of-append
  (equal (vl-assignlist-check-selfassigns (append acl2::a acl2::b)
                                          ss)
         (append (vl-assignlist-check-selfassigns acl2::a ss)
                 (vl-assignlist-check-selfassigns acl2::b ss)))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-when-not-consp

(defthm vl-assignlist-check-selfassigns-when-not-consp
  (implies (not (consp acl2::x))
           (equal (vl-assignlist-check-selfassigns acl2::x ss)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: vl-assignlist-check-selfassigns-of-cons

(defthm vl-assignlist-check-selfassigns-of-cons
  (equal (vl-assignlist-check-selfassigns (cons acl2::a acl2::b)
                                          ss)
         (append (vl-assign-check-selfassigns acl2::a ss)
                 (vl-assignlist-check-selfassigns acl2::b ss)))
  :rule-classes ((:rewrite)))