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