(vl-portinfo-vars x) → vars
Function:
(defun vl-portinfo-vars (x) (declare (xargs :guard (vl-portinfo-p x))) (let ((__function__ 'vl-portinfo-vars)) (declare (ignorable __function__)) (vl-portinfo-case x :regular (append (sv::lhs-vars x.port-lhs) (sv::svex-vars x.conn-svex)) :otherwise nil)))
Theorem:
(defthm svarlist-p-of-vl-portinfo-vars (b* ((vars (vl-portinfo-vars x))) (sv::svarlist-p vars)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-portinfo-vars-implies (implies (sv::svarlist-addr-p (vl-portinfo-vars x)) (and (implies (vl-portinfo-case x :regular) (b* (((vl-portinfo-regular x))) (and (sv::svarlist-addr-p (sv::lhs-vars x.port-lhs)) (sv::svarlist-addr-p (sv::svex-vars x.conn-svex))))))))
Theorem:
(defthm true-listp-of-vl-portinfo-vars (b* ((?vars (vl-portinfo-vars x))) (true-listp vars)) :rule-classes :type-prescription)
Theorem:
(defthm vl-portinfo-vars-of-vl-portinfo-fix-x (equal (vl-portinfo-vars (vl-portinfo-fix x)) (vl-portinfo-vars x)))
Theorem:
(defthm vl-portinfo-vars-vl-portinfo-equiv-congruence-on-x (implies (vl-portinfo-equiv x x-equiv) (equal (vl-portinfo-vars x) (vl-portinfo-vars x-equiv))) :rule-classes :congruence)