(vl-lucid-resolved-slices->bits x) → indices
Function:
(defun vl-lucid-resolved-slices->bits (x) (declare (xargs :guard (vl-lucidocclist-p x))) (declare (xargs :guard (and (vl-lucid-all-slices-p x) (vl-lucid-all-slices-resolved-p x)))) (let ((__function__ 'vl-lucid-resolved-slices->bits)) (declare (ignorable __function__)) (if (atom x) nil (union (vl-lucid-resolved-slice->bits (car x)) (vl-lucid-resolved-slices->bits (cdr x))))))
Theorem:
(defthm return-type-of-vl-lucid-resolved-slices->bits (b* ((indices (vl-lucid-resolved-slices->bits x))) (and (nat-listp indices) (setp indices))) :rule-classes :rewrite)
Theorem:
(defthm vl-lucid-resolved-slices->bits-of-vl-lucidocclist-fix-x (equal (vl-lucid-resolved-slices->bits (vl-lucidocclist-fix x)) (vl-lucid-resolved-slices->bits x)))
Theorem:
(defthm vl-lucid-resolved-slices->bits-vl-lucidocclist-equiv-congruence-on-x (implies (vl-lucidocclist-equiv x x-equiv) (equal (vl-lucid-resolved-slices->bits x) (vl-lucid-resolved-slices->bits x-equiv))) :rule-classes :congruence)