(vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) → (mv vttree portinfo)
Function:
(defun vl-plainarglist-portinfo (x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (declare (xargs :guard (and (vl-plainarglist-p x) (vl-portlist-p y) (natp argindex) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (stringp inst-modname) (vl-scopestack-p inst-ss) (vl-elabscopes-p inst-scopes) (maybe-posp arraysize)))) (declare (xargs :guard (eql (len x) (len y)))) (let ((__function__ 'vl-plainarglist-portinfo)) (declare (ignorable __function__)) (if (atom x) (mv nil nil) (b* ((vttree nil) ((vmv vttree portinfo1) (vl-plainarg-portinfo (car x) (car y) argindex ss scopes inst-modname inst-ss inst-scopes arraysize)) ((vmv vttree portinfo2) (vl-plainarglist-portinfo (cdr x) (cdr y) (1+ (lnfix argindex)) ss scopes inst-modname inst-ss inst-scopes arraysize))) (mv vttree (cons portinfo1 portinfo2))))))
Theorem:
(defthm return-type-of-vl-plainarglist-portinfo.vttree (b* (((mv ?vttree ?portinfo) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-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-plainarglist-portinfo.portinfo (b* (((mv ?vttree ?portinfo) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) (vl-portinfolist-p portinfo)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-plainarglist-portinfo (b* (((mv ?vttree ?portinfo) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) (and (sv::svarlist-addr-p (vl-portinfolist-vars portinfo)))))
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-plainarglist-fix-x (equal (vl-plainarglist-portinfo (vl-plainarglist-fix x) y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-plainarglist-equiv-congruence-on-x (implies (vl-plainarglist-equiv x x-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x-equiv y argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-portlist-fix-y (equal (vl-plainarglist-portinfo x (vl-portlist-fix y) argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-portlist-equiv-congruence-on-y (implies (vl-portlist-equiv y y-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y-equiv argindex ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-nfix-argindex (equal (vl-plainarglist-portinfo x y (nfix argindex) ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-nat-equiv-congruence-on-argindex (implies (acl2::nat-equiv argindex argindex-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex-equiv ss scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-scopestack-fix-ss (equal (vl-plainarglist-portinfo x y argindex (vl-scopestack-fix ss) scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss-equiv scopes inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-elabscopes-fix-scopes (equal (vl-plainarglist-portinfo x y argindex ss (vl-elabscopes-fix scopes) inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes-equiv inst-modname inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-str-fix-inst-modname (equal (vl-plainarglist-portinfo x y argindex ss scopes (str-fix inst-modname) inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-streqv-congruence-on-inst-modname (implies (streqv inst-modname inst-modname-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname-equiv inst-ss inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-scopestack-fix-inst-ss (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname (vl-scopestack-fix inst-ss) inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-scopestack-equiv-congruence-on-inst-ss (implies (vl-scopestack-equiv inst-ss inst-ss-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss-equiv inst-scopes arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-vl-elabscopes-fix-inst-scopes (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss (vl-elabscopes-fix inst-scopes) arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-vl-elabscopes-equiv-congruence-on-inst-scopes (implies (vl-elabscopes-equiv inst-scopes inst-scopes-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes-equiv arraysize))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-portinfo-of-maybe-posp-fix-arraysize (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes (acl2::maybe-posp-fix arraysize)) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize)))
Theorem:
(defthm vl-plainarglist-portinfo-maybe-pos-equiv-congruence-on-arraysize (implies (acl2::maybe-pos-equiv arraysize arraysize-equiv) (equal (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize) (vl-plainarglist-portinfo x y argindex ss scopes inst-modname inst-ss inst-scopes arraysize-equiv))) :rule-classes :congruence)