(vl-interfaceports->svex x ss self-lsb context-mod) → (mv warnings wires insts aliases modalist width)
Function:
(defun vl-interfaceports->svex (x ss self-lsb context-mod) (declare (xargs :guard (and (vl-interfaceportlist-p x) (vl-scopestack-p ss) (maybe-natp self-lsb) (sv::modname-p context-mod)))) (let ((__function__ 'vl-interfaceports->svex)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil nil nil nil 0)) (warnings nil) (self-lsb (maybe-natp-fix self-lsb)) ((wmv warnings wires2 insts2 aliases2 modalist2 width2) (vl-interfaceports->svex (cdr x) ss self-lsb context-mod)) ((wmv warnings wires1 insts1 aliases1 modalist1 width1) (vl-interfaceport->svex (car x) ss (and self-lsb (+ width2 self-lsb)) context-mod))) (mv warnings (append-without-guard wires1 wires2) (append-without-guard insts1 insts2) (append-without-guard aliases1 aliases2) (append-without-guard modalist1 modalist2) (+ width1 width2)))))
Theorem:
(defthm vl-warninglist-p-of-vl-interfaceports->svex.warnings (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm wirelist-p-of-vl-interfaceports->svex.wires (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (sv::wirelist-p wires)) :rule-classes :rewrite)
Theorem:
(defthm modinstlist-p-of-vl-interfaceports->svex.insts (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (sv::modinstlist-p insts)) :rule-classes :rewrite)
Theorem:
(defthm lhspairs-p-of-vl-interfaceports->svex.aliases (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm modalist-p-of-vl-interfaceports->svex.modalist (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (sv::modalist-p modalist)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-vl-interfaceports->svex.width (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (natp width)) :rule-classes :type-prescription)
Theorem:
(defthm vars-of-vl-interfaceports->svex (b* (((mv ?warnings ?wires ?insts ?aliases ?modalist ?width) (vl-interfaceports->svex x ss self-lsb context-mod))) (and (sv::svarlist-addr-p (sv::lhspairs-vars aliases)) (sv::svarlist-addr-p (sv::modalist-vars modalist)))))
Theorem:
(defthm vl-interfaceports->svex-of-vl-interfaceportlist-fix-x (equal (vl-interfaceports->svex (vl-interfaceportlist-fix x) ss self-lsb context-mod) (vl-interfaceports->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceports->svex-vl-interfaceportlist-equiv-congruence-on-x (implies (vl-interfaceportlist-equiv x x-equiv) (equal (vl-interfaceports->svex x ss self-lsb context-mod) (vl-interfaceports->svex x-equiv ss self-lsb context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceports->svex-of-vl-scopestack-fix-ss (equal (vl-interfaceports->svex x (vl-scopestack-fix ss) self-lsb context-mod) (vl-interfaceports->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceports->svex-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-interfaceports->svex x ss self-lsb context-mod) (vl-interfaceports->svex x ss-equiv self-lsb context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceports->svex-of-maybe-natp-fix-self-lsb (equal (vl-interfaceports->svex x ss (maybe-natp-fix self-lsb) context-mod) (vl-interfaceports->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceports->svex-maybe-nat-equiv-congruence-on-self-lsb (implies (acl2::maybe-nat-equiv self-lsb self-lsb-equiv) (equal (vl-interfaceports->svex x ss self-lsb context-mod) (vl-interfaceports->svex x ss self-lsb-equiv context-mod))) :rule-classes :congruence)
Theorem:
(defthm vl-interfaceports->svex-of-modname-fix-context-mod (equal (vl-interfaceports->svex x ss self-lsb (sv::modname-fix context-mod)) (vl-interfaceports->svex x ss self-lsb context-mod)))
Theorem:
(defthm vl-interfaceports->svex-modname-equiv-congruence-on-context-mod (implies (sv::modname-equiv context-mod context-mod-equiv) (equal (vl-interfaceports->svex x ss self-lsb context-mod) (vl-interfaceports->svex x ss self-lsb context-mod-equiv))) :rule-classes :congruence)