		Search-engine friendly clone of the ACL2 documentation.

Floating-point-comparison-specifications

Dp-sse-cmp

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

Definitions and Theorems

Function: dp-sse-cmp

(defun dp-sse-cmp (operation op1 op2 mxcsr)
  (declare (type (integer 0 38) operation)
           (type (unsigned-byte 64) op1)
           (type (unsigned-byte 64) op2)
           (type (unsigned-byte 32) mxcsr))
  (let ((__function__ 'dp-sse-cmp))
    (declare (ignorable __function__))
    (b* (((mv flg result mxcsr)
          (sse-cmp operation op1 op2 mxcsr 11 52))
         (result (n64 result)))
      (mv flg result mxcsr))))

Theorem: n64p-result-dp-sse-cmp

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

Theorem: n32p-mxcsr-dp-sse-cmp

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