		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-bit-roles-exponents

Exponents of a list of roles of unsigned integer bits.

Signature
(uinteger-bit-roles-exponents roles) → exponents
Arguments: roles — Guard (uinteger-bit-role-listp roles).
Returns: exponents — Type (nat-listp 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.

Definitions and Theorems

Function: uinteger-bit-roles-exponents

(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: nat-listp-of-uinteger-bit-roles-exponents

(defthm nat-listp-of-uinteger-bit-roles-exponents
  (b* ((exponents (uinteger-bit-roles-exponents roles)))
    (nat-listp exponents))
  :rule-classes :rewrite)

Theorem: uinteger-bit-roles-exponents-of-uinteger-bit-role-list-fix-roles

(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: uinteger-bit-roles-exponents-uinteger-bit-role-list-equiv-congruence-on-roles

(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)