(sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr) → (mv * * *)
Function:
(defun sp-sse-add/sub/mul/div/max/min (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-add/sub/mul/div/max/min)) (declare (ignorable __function__)) (if (or (int= operation 34) (int= operation 36)) (sp-sse-max/min operation op1 op2 mxcsr) (sp-sse-add/sub/mul/div operation op1 op2 mxcsr))))
Theorem:
(defthm n32p-result-sp-sse-add/sub/mul/div/max/min (unsigned-byte-p 32 (mv-nth 1 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) (< (mv-nth 1 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm n32p-mxcsr-sp-sse-add/sub/mul/div/max/min (unsigned-byte-p 32 (mv-nth 2 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr))) (< (mv-nth 2 (sp-sse-add/sub/mul/div/max/min operation op1 op2 mxcsr)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))