(vl-assignlist-check-selfassigns x mod ialist) applies vl-assign-check-selfassigns to every member of the list
This is an ordinary defmapappend.
Function:
(defun vl-assignlist-check-selfassigns (x mod ialist) (declare (xargs :guard (and (vl-assignlist-p x) (vl-module-p mod) (equal ialist (vl-make-moditem-alist mod))))) (mbe :logic (if (consp x) (append (vl-assign-check-selfassigns (car x) mod ialist) (vl-assignlist-check-selfassigns (cdr x) mod ialist)) nil) :exec (reverse (vl-assignlist-check-selfassigns-exec x mod ialist nil))))
Function:
(defun vl-assignlist-check-selfassigns-exec (x mod ialist acc) (declare (xargs :guard (and (vl-assignlist-p x) (vl-module-p mod) (equal ialist (vl-make-moditem-alist mod))))) (if (consp x) (vl-assignlist-check-selfassigns-exec (cdr x) mod ialist (revappend (vl-assign-check-selfassigns (car x) mod ialist) acc)) acc))
Function:
(defun vl-assignlist-check-selfassigns (x mod ialist) (declare (xargs :guard (and (vl-assignlist-p x) (vl-module-p mod) (equal ialist (vl-make-moditem-alist mod))))) (mbe :logic (if (consp x) (append (vl-assign-check-selfassigns (car x) mod ialist) (vl-assignlist-check-selfassigns (cdr x) mod ialist)) nil) :exec (reverse (vl-assignlist-check-selfassigns-exec x mod ialist nil))))
Theorem:
(defthm vl-assignlist-check-selfassigns-exec-removal (equal (vl-assignlist-check-selfassigns-exec acl2::x mod ialist acl2::acc) (revappend (vl-assignlist-check-selfassigns acl2::x mod ialist) acl2::acc)) :rule-classes ((:rewrite)))
Theorem:
(defthm set-equiv-congruence-over-vl-assignlist-check-selfassigns (implies (set-equiv acl2::x acl2::y) (set-equiv (vl-assignlist-check-selfassigns acl2::x mod ialist) (vl-assignlist-check-selfassigns acl2::y mod ialist))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-vl-assignlist-check-selfassigns-when-subsetp (implies (subsetp acl2::x acl2::y) (subsetp (vl-assignlist-check-selfassigns acl2::x mod ialist) (vl-assignlist-check-selfassigns acl2::y mod ialist))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-in-vl-assignlist-check-selfassigns (implies (and (member acl2::k (vl-assign-check-selfassigns acl2::j mod ialist)) (member acl2::j acl2::x)) (member acl2::k (vl-assignlist-check-selfassigns acl2::x mod ialist))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-assignlist-check-selfassigns-of-list-fix (equal (vl-assignlist-check-selfassigns (list-fix acl2::x) mod ialist) (vl-assignlist-check-selfassigns acl2::x mod ialist)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-assignlist-check-selfassigns-of-append (equal (vl-assignlist-check-selfassigns (append acl2::a acl2::b) mod ialist) (append (vl-assignlist-check-selfassigns acl2::a mod ialist) (vl-assignlist-check-selfassigns acl2::b mod ialist))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-assignlist-check-selfassigns-when-not-consp (implies (not (consp acl2::x)) (equal (vl-assignlist-check-selfassigns acl2::x mod ialist) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-assignlist-check-selfassigns-of-cons (equal (vl-assignlist-check-selfassigns (cons acl2::a acl2::b) mod ialist) (append (vl-assign-check-selfassigns acl2::a mod ialist) (vl-assignlist-check-selfassigns acl2::b mod ialist))) :rule-classes ((:rewrite)))