		Search-engine friendly clone of the ACL2 documentation.

Rflag-specifications

Cf-spec16

Signature
(cf-spec16 raw-result) → *

Definitions and Theorems

Function: cf-spec16$inline

(defun cf-spec16$inline (raw-result)
  (declare (type (unsigned-byte 17) raw-result))
  (bool->bit (mbe :logic (not (unsigned-byte-p 16 raw-result))
                  :exec (not (< raw-result 65536)))))

Theorem: n01p-cf-spec16

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