(vl-selfassign-bits-from-indices name bits) → bits
Function:
(defun vl-selfassign-bits-from-indices (name bits) (declare (xargs :guard (and (stringp name) (integer-listp bits)))) (let ((__function__ 'vl-selfassign-bits-from-indices)) (declare (ignorable __function__)) (if (atom bits) nil (cons (vl-selfassign-bit name (car bits)) (vl-selfassign-bits-from-indices name (cdr bits))))))
Theorem:
(defthm string-listp-of-vl-selfassign-bits-from-indices (b* ((bits (vl-selfassign-bits-from-indices name bits))) (string-listp bits)) :rule-classes :rewrite)
Theorem:
(defthm vl-selfassign-bits-from-indices-of-str-fix-name (equal (vl-selfassign-bits-from-indices (str-fix name) bits) (vl-selfassign-bits-from-indices name bits)))
Theorem:
(defthm vl-selfassign-bits-from-indices-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-selfassign-bits-from-indices name bits) (vl-selfassign-bits-from-indices name-equiv bits))) :rule-classes :congruence)
Theorem:
(defthm vl-selfassign-bits-from-indices-of-integer-list-fix-bits (equal (vl-selfassign-bits-from-indices name (acl2::integer-list-fix bits)) (vl-selfassign-bits-from-indices name bits)))
Theorem:
(defthm vl-selfassign-bits-from-indices-integer-list-equiv-congruence-on-bits (implies (acl2::integer-list-equiv bits bits-equiv) (equal (vl-selfassign-bits-from-indices name bits) (vl-selfassign-bits-from-indices name bits-equiv))) :rule-classes :congruence)