		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-bit-roles-value-count

Number of value bit roles in a list of roles of unsigned integer bits.

Signature
(uinteger-bit-roles-value-count roles) → n
Arguments: roles — Guard (uinteger-bit-role-listp roles).
Returns: n — Type (natp n).

If the list of bit roles is well-formed (see uinteger-bit-roles-wfp), this is the number N of value bits [C17:6.2.6.2/1], whose associated exponents go from 0 to N-1.

Definitions and Theorems

Function: uinteger-bit-roles-value-count

(defun uinteger-bit-roles-value-count (roles)
  (declare (xargs :guard (uinteger-bit-role-listp roles)))
  (let ((__function__ 'uinteger-bit-roles-value-count))
    (declare (ignorable __function__))
    (cond ((endp roles) 0)
          ((uinteger-bit-role-case (car roles)
                                   :value)
           (1+ (uinteger-bit-roles-value-count (cdr roles))))
          (t (uinteger-bit-roles-value-count (cdr roles))))))

Theorem: natp-of-uinteger-bit-roles-value-count

(defthm natp-of-uinteger-bit-roles-value-count
  (b* ((n (uinteger-bit-roles-value-count roles)))
    (natp n))
  :rule-classes :rewrite)

Theorem: uinteger-bit-roles-value-count-alt-def

(defthm uinteger-bit-roles-value-count-alt-def
  (equal (uinteger-bit-roles-value-count roles)
         (len (uinteger-bit-roles-exponents roles))))

Theorem: posp-of-uinteger-bit-roles-value-count

(defthm posp-of-uinteger-bit-roles-value-count
  (implies (uinteger-bit-roles-wfp roles)
           (b* ((n (uinteger-bit-roles-value-count roles)))
             (posp n)))
  :rule-classes (:rewrite :type-prescription))

Theorem: uinteger-bit-roles-value-count-of-append

(defthm uinteger-bit-roles-value-count-of-append
  (equal (uinteger-bit-roles-value-count (append roles1 roles2))
         (+ (uinteger-bit-roles-value-count roles1)
            (uinteger-bit-roles-value-count roles2))))

Theorem: uinteger-bit-roles-value-count-of-uinteger-bit-role-list-fix-roles

(defthm
 uinteger-bit-roles-value-count-of-uinteger-bit-role-list-fix-roles
 (equal (uinteger-bit-roles-value-count
             (uinteger-bit-role-list-fix roles))
        (uinteger-bit-roles-value-count roles)))

Theorem: uinteger-bit-roles-value-count-uinteger-bit-role-list-equiv-congruence-on-roles

(defthm
 uinteger-bit-roles-value-count-uinteger-bit-role-list-equiv-congruence-on-roles
 (implies (uinteger-bit-role-list-equiv roles roles-equiv)
          (equal (uinteger-bit-roles-value-count roles)
                 (uinteger-bit-roles-value-count roles-equiv)))
 :rule-classes :congruence)