		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format-inc-sign-tcnpnt

The unsigned and signed integer format defined by a size greater than 1, increasing value bits, a sign bit at the end (for the signed format), two's complement signed format, no padding bits, and no trap representations.

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

Definitions and Theorems

Function: integer-format-inc-sign-tcnpnt

(defun integer-format-inc-sign-tcnpnt (size)
 (declare (xargs :guard (posp size)))
 (declare (xargs :guard (not (equal size 1))))
 (let ((__function__ 'integer-format-inc-sign-tcnpnt))
  (declare (ignorable __function__))
  (make-integer-format
      :pair
      (make-uinteger+sinteger-format
           :unsigned (uinteger-format-inc-npnt size)
           :signed
           (sinteger-format-inc-sign-tcnpnt (1- (pos-fix size)))))))

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

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

Theorem: uinteger-sinteger-bit-roles-wfp-of-integer-format-inc-sign-tcnpnt

(defthm
  uinteger-sinteger-bit-roles-wfp-of-integer-format-inc-sign-tcnpnt
  (implies
       (and (posp size) (not (equal size 1)))
       (uinteger-sinteger-bit-roles-wfp
            (uinteger-format->bits (uinteger-format-inc-npnt size))
            (sinteger-format->bits
                 (sinteger-format-inc-sign-tcnpnt (+ -1 size))))))

Theorem: integer-format->size-of-integer-format-inc-sign-tcnpnt

(defthm integer-format->size-of-integer-format-inc-sign-tcnpnt
 (implies
   (and (posp size) (not (equal size 1)))
   (equal
        (integer-format->size (integer-format-inc-sign-tcnpnt size))
        size)))

Theorem: integer-format-unsigned->max-of-integer-format-inc-sign-tcnpnt

(defthm
     integer-format-unsigned->max-of-integer-format-inc-sign-tcnpnt
 (implies
  (and (posp size) (not (equal size 1)))
  (equal
   (uinteger-format->max
    (uinteger+sinteger-format->unsigned
      (integer-format->pair (integer-format-inc-sign-tcnpnt size))))
   (1- (expt 2 size)))))

Theorem: integer-format-signed->max-of-integer-format-inc-sign-tcnpnt

(defthm integer-format-signed->max-of-integer-format-inc-sign-tcnpnt
 (implies
  (and (posp size) (not (equal size 1)))
  (equal
   (sinteger-format->max
    (uinteger+sinteger-format->signed
      (integer-format->pair (integer-format-inc-sign-tcnpnt size))))
   (1- (expt 2 (1- size))))))

Theorem: integer-format-signed->min-of-integer-format-inc-sign-tcnpnt

(defthm integer-format-signed->min-of-integer-format-inc-sign-tcnpnt
 (implies
  (and (posp size) (not (equal size 1)))
  (equal
   (sinteger-format->min
    (uinteger+sinteger-format->signed
      (integer-format->pair (integer-format-inc-sign-tcnpnt size))))
   (- (expt 2 (1- size))))))

Theorem: integer-format-inc-sign-tcnpnt-of-pos-fix-size

(defthm integer-format-inc-sign-tcnpnt-of-pos-fix-size
  (equal (integer-format-inc-sign-tcnpnt (pos-fix size))
         (integer-format-inc-sign-tcnpnt size)))

Theorem: integer-format-inc-sign-tcnpnt-pos-equiv-congruence-on-size

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