(vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc) → (mv warnings ports-acc portdecls-acc vardecls-acc)
Function:
(defun vl-process-subsequent-ansi-ports (x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc) (declare (xargs :guard (and (vl-parsed-ansi-portlist-p x) (booleanp prev-ifacep) (vl-warninglist-p warnings) (vl-portlist-p ports-acc) (vl-portdecllist-p portdecls-acc) (vl-vardecllist-p vardecls-acc)))) (declare (xargs :guard (and (consp ports-acc) (equal (vl-interfaceport-p (car ports-acc)) prev-ifacep) (equal (vl-regularport-p (car ports-acc)) (not prev-ifacep)) (implies (not prev-ifacep) (and (consp portdecls-acc) (consp vardecls-acc)))))) (let ((__function__ 'vl-process-subsequent-ansi-ports)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (vl-warninglist-fix warnings) (vl-portlist-fix ports-acc) (vl-portdecllist-fix portdecls-acc) (vl-vardecllist-fix vardecls-acc))) ((mv ifacep1 warnings ports-acc portdecls-acc vardecls-acc) (vl-process-subsequent-ansi-port (car x) prev-ifacep warnings ports-acc portdecls-acc vardecls-acc))) (vl-process-subsequent-ansi-ports (cdr x) ifacep1 warnings ports-acc portdecls-acc vardecls-acc))))
Theorem:
(defthm vl-warninglist-p-of-vl-process-subsequent-ansi-ports.warnings (b* (((mv ?warnings ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-portlist-p-of-vl-process-subsequent-ansi-ports.ports-acc (b* (((mv ?warnings ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc))) (vl-portlist-p ports-acc)) :rule-classes :rewrite)
Theorem:
(defthm vl-portdecllist-p-of-vl-process-subsequent-ansi-ports.portdecls-acc (b* (((mv ?warnings ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc))) (vl-portdecllist-p portdecls-acc)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-process-subsequent-ansi-ports.vardecls-acc (b* (((mv ?warnings ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc))) (vl-vardecllist-p vardecls-acc)) :rule-classes :rewrite)