		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Sinteger-bit-roles-sign-count

Number of sign bit roles in a list of roles of signed integer bits.

Signature
(sinteger-bit-roles-sign-count roles) → count
Arguments: roles — Guard (sinteger-bit-role-listp roles).
Returns: count — Type (natp count).

We count the number of sign bit roles. Note that the sign bit roles in a list are all the same.

Definitions and Theorems

Function: sinteger-bit-roles-sign-count

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

Theorem: natp-of-sinteger-bit-roles-sign-count

(defthm natp-of-sinteger-bit-roles-sign-count
  (b* ((count (sinteger-bit-roles-sign-count roles)))
    (natp count))
  :rule-classes :rewrite)

Theorem: sinteger-bit-roles-sign-count-of-sinteger-bit-role-list-fix-roles

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

Theorem: sinteger-bit-roles-sign-count-sinteger-bit-role-list-equiv-congruence-on-roles

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