		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Uinteger-format-inc-npnt

The unsigned integer format defined by n increasing value bits, no padding bits, and no trap representations.

Signature
(uinteger-format-inc-npnt n) → format
Arguments: n — Guard (posp n).
Returns: format — Type (uinteger-formatp format).

This is parameterized over n, which must be positiive.

Definitions and Theorems

Function: uinteger-format-inc-npnt

(defun uinteger-format-inc-npnt (n)
 (declare (xargs :guard (posp n)))
 (let ((__function__ 'uinteger-format-inc-npnt))
  (declare (ignorable __function__))
  (make-uinteger-format :bits (uinteger-bit-roles-inc-n (pos-fix n))
                        :traps nil)))

Theorem: uinteger-formatp-of-uinteger-format-inc-npnt

(defthm uinteger-formatp-of-uinteger-format-inc-npnt
  (b* ((format (uinteger-format-inc-npnt n)))
    (uinteger-formatp format))
  :rule-classes :rewrite)

Theorem: uinteger-format->max-of-uinteger-format-inc-npnt

(defthm uinteger-format->max-of-uinteger-format-inc-npnt
  (equal (uinteger-format->max (uinteger-format-inc-npnt n))
         (1- (expt 2 (pos-fix n)))))

Theorem: uinteger-format-inc-npnt-of-pos-fix-n

(defthm uinteger-format-inc-npnt-of-pos-fix-n
  (equal (uinteger-format-inc-npnt (pos-fix n))
         (uinteger-format-inc-npnt n)))

Theorem: uinteger-format-inc-npnt-pos-equiv-congruence-on-n

(defthm uinteger-format-inc-npnt-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (uinteger-format-inc-npnt n)
                  (uinteger-format-inc-npnt n-equiv)))
  :rule-classes :congruence)