(vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) → (mv vttree portinfo)
Function:
(defun vl-gate-plainarglist-portinfo (x portnames portdirs argindex ss scopes arraysize) (declare (xargs :guard (and (vl-plainarglist-p x) (string-listp portnames) (vl-directionlist-p portdirs) (natp argindex) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (maybe-posp arraysize)))) (declare (xargs :guard (and (eql (len x) (len portnames)) (eql (len x) (len portdirs))))) (let ((__function__ 'vl-gate-plainarglist-portinfo)) (declare (ignorable __function__)) (if (atom x) (mv nil nil) (b* ((vttree nil) ((vmv vttree portinfo1) (vl-gate-plainarg-portinfo (car x) (car portnames) (car portdirs) argindex ss scopes arraysize)) ((vmv vttree portinfo2) (vl-gate-plainarglist-portinfo (cdr x) (cdr portnames) (cdr portdirs) (1+ (lnfix argindex)) ss scopes arraysize))) (mv vttree (cons portinfo1 portinfo2))))))
Theorem:
(defthm return-type-of-vl-gate-plainarglist-portinfo.vttree (b* (((mv ?vttree ?portinfo) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm vl-portinfolist-p-of-vl-gate-plainarglist-portinfo.portinfo (b* (((mv ?vttree ?portinfo) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize))) (vl-portinfolist-p portinfo)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-gate-plainarglist-portinfo (b* (((mv ?vttree ?portinfo) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize))) (and (sv::svarlist-addr-p (vl-portinfolist-vars portinfo)))))
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-vl-plainarglist-fix-x (equal (vl-gate-plainarglist-portinfo (vl-plainarglist-fix x) portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-vl-plainarglist-equiv-congruence-on-x (implies (vl-plainarglist-equiv x x-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x-equiv portnames portdirs argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-string-list-fix-portnames (equal (vl-gate-plainarglist-portinfo x (string-list-fix portnames) portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-string-list-equiv-congruence-on-portnames (implies (str::string-list-equiv portnames portnames-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames-equiv portdirs argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-vl-directionlist-fix-portdirs (equal (vl-gate-plainarglist-portinfo x portnames (vl-directionlist-fix portdirs) argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-vl-directionlist-equiv-congruence-on-portdirs (implies (vl-directionlist-equiv portdirs portdirs-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs-equiv argindex ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-nfix-argindex (equal (vl-gate-plainarglist-portinfo x portnames portdirs (nfix argindex) ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-nat-equiv-congruence-on-argindex (implies (acl2::nat-equiv argindex argindex-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex-equiv ss scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-vl-scopestack-fix-ss (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex (vl-scopestack-fix ss) scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss-equiv scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-vl-elabscopes-fix-scopes (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss (vl-elabscopes-fix scopes) arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes-equiv arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-gate-plainarglist-portinfo-of-maybe-posp-fix-arraysize (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes (acl2::maybe-posp-fix arraysize)) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize)))
Theorem:
(defthm vl-gate-plainarglist-portinfo-maybe-pos-equiv-congruence-on-arraysize (implies (acl2::maybe-pos-equiv arraysize arraysize-equiv) (equal (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize) (vl-gate-plainarglist-portinfo x portnames portdirs argindex ss scopes arraysize-equiv))) :rule-classes :congruence)