		Search-engine friendly clone of the ACL2 documentation.

Integer-format-templates

Sinteger-format-inc-sign-tcnpnt

The signed integer format defined by n increasing value bits, a sign bit at the end, two's complement signed format, no padding bits, and no trap representations.

Signature
(sinteger-format-inc-sign-tcnpnt n) → format
Arguments: n — Guard (posp n).
Returns: format — Type (sinteger-formatp format).

This is parameterized over n, which must be positiive.

Definitions and Theorems

Function: sinteger-format-inc-sign-tcnpnt

(defun sinteger-format-inc-sign-tcnpnt (n)
  (declare (xargs :guard (posp n)))
  (make-sinteger-format
       :bits (sinteger-bit-roles-inc-n-and-sign (pos-fix n))
       :signed (signed-format-twos-complement)
       :traps nil))

Theorem: sinteger-formatp-of-sinteger-format-inc-sign-tcnpnt

(defthm sinteger-formatp-of-sinteger-format-inc-sign-tcnpnt
  (b* ((format (sinteger-format-inc-sign-tcnpnt n)))
    (sinteger-formatp format))
  :rule-classes :rewrite)

Theorem: sinteger-format->max-of-sinteger-format-inc-sign-tcnpnt

(defthm sinteger-format->max-of-sinteger-format-inc-sign-tcnpnt
  (equal (sinteger-format->max (sinteger-format-inc-sign-tcnpnt n))
         (1- (expt 2 (pos-fix n)))))

Theorem: sinteger-format->min-of-sinteger-format-inc-sign-tcnpnt

(defthm sinteger-format->min-of-sinteger-format-inc-sign-tcnpnt
  (equal (sinteger-format->min (sinteger-format-inc-sign-tcnpnt n))
         (- (expt 2 (pos-fix n)))))

Theorem: sinteger-format-inc-sign-tcnpnt-of-pos-fix-n

(defthm sinteger-format-inc-sign-tcnpnt-of-pos-fix-n
  (equal (sinteger-format-inc-sign-tcnpnt (pos-fix n))
         (sinteger-format-inc-sign-tcnpnt n)))

Theorem: sinteger-format-inc-sign-tcnpnt-pos-equiv-congruence-on-n

(defthm sinteger-format-inc-sign-tcnpnt-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (sinteger-format-inc-sign-tcnpnt n)
                  (sinteger-format-inc-sign-tcnpnt n-equiv)))
  :rule-classes :congruence)