		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Sinteger-bit-roles-exponents

Exponents of a list of roles of signed integer bits.

Signature
(sinteger-bit-roles-exponents roles) → exponents
Arguments: roles — Guard (sinteger-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 and sign bit roles.

Definitions and Theorems

Function: sinteger-bit-roles-exponents

(defun sinteger-bit-roles-exponents (roles)
  (declare (xargs :guard (sinteger-bit-role-listp roles)))
  (let ((__function__ 'sinteger-bit-roles-exponents))
    (declare (ignorable __function__))
    (b* (((when (endp roles)) nil)
         (role (car roles))
         ((unless (sinteger-bit-role-case role :value))
          (sinteger-bit-roles-exponents (cdr roles))))
      (cons (sinteger-bit-role-value->exp role)
            (sinteger-bit-roles-exponents (cdr roles))))))

Theorem: nat-listp-of-sinteger-bit-roles-exponents

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

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

(defthm
   sinteger-bit-roles-exponents-of-sinteger-bit-role-list-fix-roles
 (equal
   (sinteger-bit-roles-exponents (sinteger-bit-role-list-fix roles))
   (sinteger-bit-roles-exponents roles)))

Theorem: sinteger-bit-roles-exponents-sinteger-bit-role-list-equiv-congruence-on-roles

(defthm
 sinteger-bit-roles-exponents-sinteger-bit-role-list-equiv-congruence-on-roles
 (implies (sinteger-bit-role-list-equiv roles roles-equiv)
          (equal (sinteger-bit-roles-exponents roles)
                 (sinteger-bit-roles-exponents roles-equiv)))
 :rule-classes :congruence)