Exponents of a list of roles of unsigned integer bits.
(uinteger-bit-roles-exponents roles) → exponents
We collect the list of exponents of the value bit roles, in the same order as they occur in the list of bit roles, skipping over the padding bit roles.
Function:
(defun uinteger-bit-roles-exponents (roles) (declare (xargs :guard (uinteger-bit-role-listp roles))) (let ((__function__ 'uinteger-bit-roles-exponents)) (declare (ignorable __function__)) (b* (((when (endp roles)) nil) (role (car roles)) ((unless (uinteger-bit-role-case role :value)) (uinteger-bit-roles-exponents (cdr roles)))) (cons (uinteger-bit-role-value->exp role) (uinteger-bit-roles-exponents (cdr roles))))))
Theorem:
(defthm nat-listp-of-uinteger-bit-roles-exponents (b* ((exponents (uinteger-bit-roles-exponents roles))) (nat-listp exponents)) :rule-classes :rewrite)
Theorem:
(defthm uinteger-bit-roles-exponents-of-append (equal (uinteger-bit-roles-exponents (append roles1 roles2)) (append (uinteger-bit-roles-exponents roles1) (uinteger-bit-roles-exponents roles2))))
Theorem:
(defthm uinteger-bit-roles-exponents-of-uinteger-bit-role-list-fix-roles (equal (uinteger-bit-roles-exponents (uinteger-bit-role-list-fix roles)) (uinteger-bit-roles-exponents roles)))
Theorem:
(defthm uinteger-bit-roles-exponents-uinteger-bit-role-list-equiv-congruence-on-roles (implies (uinteger-bit-role-list-equiv roles roles-equiv) (equal (uinteger-bit-roles-exponents roles) (uinteger-bit-roles-exponents roles-equiv))) :rule-classes :congruence)