		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

Of-spec32

Signature
(of-spec32 signed-raw-result) → *

Definitions and Theorems

Function: of-spec32$inline

(defun of-spec32$inline (signed-raw-result)
  (declare (type (signed-byte 33)
                 signed-raw-result))
  (bool->bit
       (mbe :logic (not (signed-byte-p 32 signed-raw-result))
            :exec (or (not (<= -2147483648 signed-raw-result))
                      (not (< signed-raw-result 2147483648))))))

Theorem: n01p-of-spec32

(defthm n01p-of-spec32
 (unsigned-byte-p 1 (of-spec32 signed-raw-result))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (natp (of-spec32 signed-raw-result))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary (and (<= 0 (of-spec32 signed-raw-result))
                   (< (of-spec32 signed-raw-result) 2))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))