For each Bi in BADS, we compute the transitive dependencies of Bi, and then blame Bi for ruining them all.
(vl-blame-alist-aux2 bads design alist) → new-alist
Function:
(defun vl-blame-alist-aux2 (bads design alist) (declare (xargs :guard (and (string-listp bads) (vl-design-p design) (vl-blamealist-p alist)))) (let ((__function__ 'vl-blame-alist-aux2)) (declare (ignorable __function__)) (b* (((when (atom bads)) (vl-blamealist-fix alist)) (deps (vl-dependent-elements-transitive (list (car bads)) design)) (alist (vl-blame-alist-aux1 (car bads) deps alist))) (vl-blame-alist-aux2 (cdr bads) design alist))))
Theorem:
(defthm vl-blamealist-p-of-vl-blame-alist-aux2 (b* ((new-alist (vl-blame-alist-aux2 bads design alist))) (vl-blamealist-p new-alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-blame-alist-aux2-when-not-consp (implies (not (consp bads)) (equal (vl-blame-alist-aux2 bads design alist) (vl-blamealist-fix alist))))
Theorem:
(defthm vl-blame-alist-aux2-of-string-list-fix-bads (equal (vl-blame-alist-aux2 (string-list-fix bads) design alist) (vl-blame-alist-aux2 bads design alist)))
Theorem:
(defthm vl-blame-alist-aux2-string-list-equiv-congruence-on-bads (implies (str::string-list-equiv bads bads-equiv) (equal (vl-blame-alist-aux2 bads design alist) (vl-blame-alist-aux2 bads-equiv design alist))) :rule-classes :congruence)
Theorem:
(defthm vl-blame-alist-aux2-of-vl-design-fix-design (equal (vl-blame-alist-aux2 bads (vl-design-fix design) alist) (vl-blame-alist-aux2 bads design alist)))
Theorem:
(defthm vl-blame-alist-aux2-vl-design-equiv-congruence-on-design (implies (vl-design-equiv design design-equiv) (equal (vl-blame-alist-aux2 bads design alist) (vl-blame-alist-aux2 bads design-equiv alist))) :rule-classes :congruence)
Theorem:
(defthm vl-blame-alist-aux2-of-vl-blamealist-fix-alist (equal (vl-blame-alist-aux2 bads design (vl-blamealist-fix alist)) (vl-blame-alist-aux2 bads design alist)))
Theorem:
(defthm vl-blame-alist-aux2-vl-blamealist-equiv-congruence-on-alist (implies (vl-blamealist-equiv alist alist-equiv) (equal (vl-blame-alist-aux2 bads design alist) (vl-blame-alist-aux2 bads design alist-equiv))) :rule-classes :congruence)