		Search-engine friendly clone of the ACL2 documentation.

Integer-format-templates

Sinteger-bit-roles-inc-n-and-sign

List of n signed integer value bit roles, starting with exponent 0, in increasing exponent order, and with a sign bit added at the end.

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

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

Definitions and Theorems

Function: sinteger-bit-roles-inc-n-and-sign

(defun sinteger-bit-roles-inc-n-and-sign (n)
  (declare (xargs :guard (natp n)))
  (append (sinteger-bit-roles-inc-n n)
          (list (sinteger-bit-role-sign))))

Theorem: sinteger-bit-role-listp-of-sinteger-bit-roles-inc-n-and-sign

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

Theorem: sinteger-bit-roles-wfp-of-sinteger-bit-roles-inc-n-and-sign

(defthm sinteger-bit-roles-wfp-of-sinteger-bit-roles-inc-n-and-sign
 (implies
    (not (zp n))
    (sinteger-bit-roles-wfp (sinteger-bit-roles-inc-n-and-sign n))))

Theorem: sinteger-bit-roles-exponents-of-sinteger-bit-roles-inc-n-and-sign

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

Theorem: sinteger-bit-roles-value-count-of-sinteger-bit-roles-inc-n-and-sign

(defthm
 sinteger-bit-roles-value-count-of-sinteger-bit-roles-inc-n-and-sign
 (equal (sinteger-bit-roles-value-count
             (sinteger-bit-roles-inc-n-and-sign n))
        (nfix n)))

Theorem: sinteger-bit-roles-inc-n-and-sign-of-nfix-n

(defthm sinteger-bit-roles-inc-n-and-sign-of-nfix-n
  (equal (sinteger-bit-roles-inc-n-and-sign (nfix n))
         (sinteger-bit-roles-inc-n-and-sign n)))

Theorem: sinteger-bit-roles-inc-n-and-sign-nat-equiv-congruence-on-n

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