(vl-assignlist-check-selfassigns x ss) applies vl-assign-check-selfassigns to every member of the list
This is an ordinary defmapappend.
Function:
(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))))
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)))