(vl-aliaslist-immdeps x ans &key (ss 'ss)) → new-ans
Function:
(defun vl-aliaslist-immdeps-fn (x ans ss) (declare (xargs :guard (and (vl-aliaslist-p x) (vl-immdeps-p ans) (vl-scopestack-p ss)))) (let ((__function__ 'vl-aliaslist-immdeps)) (declare (ignorable __function__)) (b* (((when (atom x)) (vl-immdeps-fix ans)) (ans (vl-alias-immdeps (car x) ans))) (vl-aliaslist-immdeps (cdr x) ans))))
Theorem:
(defthm vl-immdeps-p-of-vl-aliaslist-immdeps (b* ((new-ans (vl-aliaslist-immdeps-fn x ans ss))) (vl-immdeps-p new-ans)) :rule-classes :rewrite)
Theorem:
(defthm vl-aliaslist-immdeps-fn-of-vl-aliaslist-fix-x (equal (vl-aliaslist-immdeps-fn (vl-aliaslist-fix x) ans ss) (vl-aliaslist-immdeps-fn x ans ss)))
Theorem:
(defthm vl-aliaslist-immdeps-fn-vl-aliaslist-equiv-congruence-on-x (implies (vl-aliaslist-equiv x x-equiv) (equal (vl-aliaslist-immdeps-fn x ans ss) (vl-aliaslist-immdeps-fn x-equiv ans ss))) :rule-classes :congruence)
Theorem:
(defthm vl-aliaslist-immdeps-fn-of-vl-immdeps-fix-ans (equal (vl-aliaslist-immdeps-fn x (vl-immdeps-fix ans) ss) (vl-aliaslist-immdeps-fn x ans ss)))
Theorem:
(defthm vl-aliaslist-immdeps-fn-vl-immdeps-equiv-congruence-on-ans (implies (vl-immdeps-equiv ans ans-equiv) (equal (vl-aliaslist-immdeps-fn x ans ss) (vl-aliaslist-immdeps-fn x ans-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-aliaslist-immdeps-fn-of-vl-scopestack-fix-ss (equal (vl-aliaslist-immdeps-fn x ans (vl-scopestack-fix ss)) (vl-aliaslist-immdeps-fn x ans ss)))
Theorem:
(defthm vl-aliaslist-immdeps-fn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-aliaslist-immdeps-fn x ans ss) (vl-aliaslist-immdeps-fn x ans ss-equiv))) :rule-classes :congruence)