(vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev) → nrev
Function:
(defun vl-reportcard-revive-invalid-warnings-exec (x valid-fal nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-reportcard-p x))) (declare (xargs :guard (hons-assoc-equal :design valid-fal))) (let ((__function__ 'vl-reportcard-revive-invalid-warnings-exec)) (declare (ignorable __function__)) (b* ((x (vl-reportcard-fix x)) ((when (atom x)) (nrev-fix nrev)) ((cons name1 warnings1) (car x)) ((when (hons-get name1 valid-fal)) (vl-reportcard-revive-invalid-warnings-exec (cdr x) valid-fal nrev)) (nrev (vl-revive-invalid-warnings-nrev name1 warnings1 nrev))) (vl-reportcard-revive-invalid-warnings-exec (cdr x) valid-fal nrev))))
Theorem:
(defthm vl-reportcard-revive-invalid-warnings-exec-of-vl-reportcard-fix-x (equal (vl-reportcard-revive-invalid-warnings-exec (vl-reportcard-fix x) valid-fal nrev) (vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev)))
Theorem:
(defthm vl-reportcard-revive-invalid-warnings-exec-vl-reportcard-equiv-congruence-on-x (implies (vl-reportcard-equiv x x-equiv) (equal (vl-reportcard-revive-invalid-warnings-exec x valid-fal nrev) (vl-reportcard-revive-invalid-warnings-exec x-equiv valid-fal nrev))) :rule-classes :congruence)