		Search-engine friendly clone of the ACL2 documentation.

Floating-point-comparison-specifications

Sp-sse-cmp

Signature
(sp-sse-cmp operation op1 op2 mxcsr) → (mv * * *)

Definitions and Theorems

Function: sp-sse-cmp

(defun sp-sse-cmp (operation op1 op2 mxcsr)
  (declare (type (integer 0 38) operation)
           (type (unsigned-byte 32) op1)
           (type (unsigned-byte 32) op2)
           (type (unsigned-byte 32) mxcsr))
  (let ((__function__ 'sp-sse-cmp))
    (declare (ignorable __function__))
    (b* (((mv flg result mxcsr)
          (sse-cmp operation op1 op2 mxcsr 8 23))
         (result (n32 result)))
      (mv flg result mxcsr))))

Theorem: n32p-result-sp-sse-cmp

(defthm n32p-result-sp-sse-cmp
 (unsigned-byte-p 32
                  (mv-nth 1 (sp-sse-cmp operation op1 op2 mxcsr)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary (natp (mv-nth 1 (sp-sse-cmp operation op1 op2 mxcsr)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 1 (sp-sse-cmp operation op1 op2 mxcsr)))
        (< (mv-nth 1 (sp-sse-cmp operation op1 op2 mxcsr))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: n32p-mxcsr-sp-sse-cmp

(defthm n32p-mxcsr-sp-sse-cmp
 (unsigned-byte-p 32
                  (mv-nth 2 (sp-sse-cmp operation op1 op2 mxcsr)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary (natp (mv-nth 2 (sp-sse-cmp operation op1 op2 mxcsr)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and (<= 0
            (mv-nth 2 (sp-sse-cmp operation op1 op2 mxcsr)))
        (< (mv-nth 2 (sp-sse-cmp operation op1 op2 mxcsr))
           4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))