(vl-initiallist-stmtrewrite x unroll-limit warnings) → (mv warnings new-x)
Function:
(defun vl-initiallist-stmtrewrite (x unroll-limit warnings) (declare (xargs :guard (and (vl-initiallist-p x) (natp unroll-limit) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-initiallist-stmtrewrite)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv warnings nil)) ((mv warnings car-prime) (vl-initial-stmtrewrite (car x) unroll-limit warnings)) ((mv warnings cdr-prime) (vl-initiallist-stmtrewrite (cdr x) unroll-limit warnings))) (mv warnings (if (vl-nullstmt-p (vl-initial->stmt car-prime)) cdr-prime (cons car-prime cdr-prime))))))
Theorem:
(defthm vl-warninglist-p-of-vl-initiallist-stmtrewrite.warnings (implies (and (force (vl-initiallist-p x)) (force (natp unroll-limit)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?new-x) (vl-initiallist-stmtrewrite x unroll-limit warnings))) (vl-warninglist-p warnings))) :rule-classes :rewrite)
Theorem:
(defthm vl-initiallist-p-of-vl-initiallist-stmtrewrite.new-x (implies (and (force (vl-initiallist-p x)) (force (natp unroll-limit)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?new-x) (vl-initiallist-stmtrewrite x unroll-limit warnings))) (vl-initiallist-p new-x))) :rule-classes :rewrite)