(vl-portinfolist-to-svex-assigns/aliases x instname range) → (mv warnings assigns aliases)
Function:
(defun vl-portinfolist-to-svex-assigns/aliases (x instname range) (declare (xargs :guard (and (vl-portinfolist-p x) (stringp instname) (vl-maybe-range-p range)))) (declare (xargs :guard (and (sv::svarlist-addr-p (vl-portinfolist-vars x)) (vl-maybe-range-resolved-p range)))) (let ((__function__ 'vl-portinfolist-to-svex-assigns/aliases)) (declare (ignorable __function__)) (b* ((warnings nil) ((when (atom x)) (mv (ok) nil nil)) ((wmv warnings assigns1 aliases1) (vl-portinfo-to-svex-assign-or-alias (car x) instname range)) ((wmv warnings assigns2 aliases2) (vl-portinfolist-to-svex-assigns/aliases (cdr x) instname range))) (mv warnings (append assigns1 assigns2) (append aliases1 aliases2)))))
Theorem:
(defthm vl-warninglist-p-of-vl-portinfolist-to-svex-assigns/aliases.warnings (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfolist-to-svex-assigns/aliases x instname range))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-portinfolist-to-svex-assigns/aliases.assigns (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfolist-to-svex-assigns/aliases x instname range))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-portinfolist-to-svex-assigns/aliases.aliases (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfolist-to-svex-assigns/aliases x instname range))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm var-of-vl-portinfolist-to-svex-assigns/aliases (b* (((mv ?warnings ?assigns ?aliases) (vl-portinfolist-to-svex-assigns/aliases x instname range))) (implies (sv::svarlist-addr-p (vl-portinfolist-vars x)) (and (sv::svarlist-addr-p (sv::assigns-vars assigns)) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))))
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-mvtypes-1 (true-listp (mv-nth 1 (vl-portinfolist-to-svex-assigns/aliases x instname range))) :rule-classes :type-prescription)
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-mvtypes-2 (true-listp (mv-nth 2 (vl-portinfolist-to-svex-assigns/aliases x instname range))) :rule-classes :type-prescription)
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-of-vl-portinfolist-fix-x (equal (vl-portinfolist-to-svex-assigns/aliases (vl-portinfolist-fix x) instname range) (vl-portinfolist-to-svex-assigns/aliases x instname range)))
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-vl-portinfolist-equiv-congruence-on-x (implies (vl-portinfolist-equiv x x-equiv) (equal (vl-portinfolist-to-svex-assigns/aliases x instname range) (vl-portinfolist-to-svex-assigns/aliases x-equiv instname range))) :rule-classes :congruence)
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-of-str-fix-instname (equal (vl-portinfolist-to-svex-assigns/aliases x (str-fix instname) range) (vl-portinfolist-to-svex-assigns/aliases x instname range)))
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-streqv-congruence-on-instname (implies (streqv instname instname-equiv) (equal (vl-portinfolist-to-svex-assigns/aliases x instname range) (vl-portinfolist-to-svex-assigns/aliases x instname-equiv range))) :rule-classes :congruence)
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-of-vl-maybe-range-fix-range (equal (vl-portinfolist-to-svex-assigns/aliases x instname (vl-maybe-range-fix range)) (vl-portinfolist-to-svex-assigns/aliases x instname range)))
Theorem:
(defthm vl-portinfolist-to-svex-assigns/aliases-vl-maybe-range-equiv-congruence-on-range (implies (vl-maybe-range-equiv range range-equiv) (equal (vl-portinfolist-to-svex-assigns/aliases x instname range) (vl-portinfolist-to-svex-assigns/aliases x instname range-equiv))) :rule-classes :congruence)