		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-bit-roles-inc-n

List of n unsigned integer value bit roles, starting with exponent 0, in increasing exponent order.

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

The list of bit roles is well-formed, if n is not 0.

Definitions and Theorems

Function: uinteger-bit-roles-inc-n

(defun uinteger-bit-roles-inc-n (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'uinteger-bit-roles-inc-n))
    (declare (ignorable __function__))
    (b* (((when (zp n)) nil)
         (role (uinteger-bit-role-value (1- n)))
         (roles (uinteger-bit-roles-inc-n (1- n))))
      (append roles (list role)))))

Theorem: uinteger-bit-role-listp-of-uinteger-bit-roles-inc-n

(defthm uinteger-bit-role-listp-of-uinteger-bit-roles-inc-n
  (b* ((roles (uinteger-bit-roles-inc-n n)))
    (uinteger-bit-role-listp roles))
  :rule-classes :rewrite)

Theorem: len-of-uinteger-bit-roles-inc-n

(defthm len-of-uinteger-bit-roles-inc-n
  (b* ((?roles (uinteger-bit-roles-inc-n n)))
    (equal (len roles) (nfix n))))

Theorem: uinteger-bit-roles-exponents-of-uinteger-bit-roles-inc-n

(defthm uinteger-bit-roles-exponents-of-uinteger-bit-roles-inc-n
  (equal (uinteger-bit-roles-exponents (uinteger-bit-roles-inc-n n))
         (integers-from-to 0 (1- (nfix n)))))

Theorem: uinteger-bit-roles-value-count-of-uinteger-bit-roles-inc-n

(defthm uinteger-bit-roles-value-count-of-uinteger-bit-roles-inc-n
  (equal
       (uinteger-bit-roles-value-count (uinteger-bit-roles-inc-n n))
       (nfix n)))

Theorem: uinteger-bit-roles-wfp-of-uinteger-bit-roles-inc-n

(defthm uinteger-bit-roles-wfp-of-uinteger-bit-roles-inc-n
  (implies (not (zp n))
           (uinteger-bit-roles-wfp (uinteger-bit-roles-inc-n n))))

Theorem: uinteger-bit-roles-inc-n-of-nfix-n

(defthm uinteger-bit-roles-inc-n-of-nfix-n
  (equal (uinteger-bit-roles-inc-n (nfix n))
         (uinteger-bit-roles-inc-n n)))

Theorem: uinteger-bit-roles-inc-n-nat-equiv-congruence-on-n

(defthm uinteger-bit-roles-inc-n-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (uinteger-bit-roles-inc-n n)
                  (uinteger-bit-roles-inc-n n-equiv)))
  :rule-classes :congruence)