Extends vl-gateinst-gate-elim to a list of gate instances.
(vl-gateinstlist-gate-elim x primalist warnings) → (mv warnings gateinsts modinsts addmods)
Function:
(defun vl-gateinstlist-gate-elim (x primalist warnings) (declare (xargs :guard (and (vl-gateinstlist-p x) (vl-primalist-p primalist) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-gateinstlist-gate-elim)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (ok) nil nil nil)) ((mv warnings car-gateinsts car-modinsts car-addmods) (vl-gateinst-gate-elim (car x) primalist warnings)) ((mv warnings cdr-gateinsts cdr-modinsts cdr-addmods) (vl-gateinstlist-gate-elim (cdr x) primalist warnings))) (mv warnings (append car-gateinsts cdr-gateinsts) (append car-modinsts cdr-modinsts) (append car-addmods cdr-addmods)))))
Theorem:
(defthm vl-warninglist-p-of-vl-gateinstlist-gate-elim.warnings (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods) (vl-gateinstlist-gate-elim x primalist warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-gateinstlist-gate-elim.gateinsts (implies (force (vl-gateinstlist-p x)) (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods) (vl-gateinstlist-gate-elim x primalist warnings))) (vl-gateinstlist-p gateinsts))) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-gateinstlist-gate-elim.modinsts (implies (force (vl-gateinstlist-p x)) (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods) (vl-gateinstlist-gate-elim x primalist warnings))) (vl-modinstlist-p modinsts))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-gateinstlist-gate-elim.addmods (implies (force (vl-gateinstlist-p x)) (b* (((mv ?warnings ?gateinsts ?modinsts ?addmods) (vl-gateinstlist-gate-elim x primalist warnings))) (vl-modulelist-p addmods))) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-gate-elim-mvtypes-1 (true-listp (mv-nth 1 (vl-gateinstlist-gate-elim x primalist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-gateinstlist-gate-elim-mvtypes-2 (true-listp (mv-nth 2 (vl-gateinstlist-gate-elim x primalist warnings))) :rule-classes :type-prescription)
Theorem:
(defthm vl-gateinstlist-gate-elim-mvtypes-3 (true-listp (mv-nth 3 (vl-gateinstlist-gate-elim x primalist warnings))) :rule-classes :type-prescription)