(sse-cvt-dp-to-sp op mxcsr) → (mv * * *)
Function:
(defun sse-cvt-dp-to-sp (op mxcsr) (declare (type (unsigned-byte 64) op) (type (unsigned-byte 32) mxcsr)) (let ((__function__ 'sse-cvt-dp-to-sp)) (declare (ignorable __function__)) (b* (((mv flg result mxcsr) (sse-cvt-fp1-to-fp2 op mxcsr 11 52 8 23)) (result (n32 result))) (mv flg result mxcsr))))
Theorem:
(defthm n32p-result-sse-cvt-dp-to-sp (unsigned-byte-p 32 (mv-nth 1 (sse-cvt-dp-to-sp op mxcsr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (sse-cvt-dp-to-sp op mxcsr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (sse-cvt-dp-to-sp op mxcsr))) (< (mv-nth 1 (sse-cvt-dp-to-sp op mxcsr)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm n32p-mxcsr-sse-cvt-dp-to-sp (unsigned-byte-p 32 (mv-nth 2 (sse-cvt-dp-to-sp op mxcsr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (sse-cvt-dp-to-sp op mxcsr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (sse-cvt-dp-to-sp op mxcsr))) (< (mv-nth 2 (sse-cvt-dp-to-sp op mxcsr)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))