(mmx i x86) → *
Function:
(defun mmx$inline (i x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 7) i)) (let ((reg80 (the (unsigned-byte 80) (fp-datai i x86)))) (mbe :logic (part-select reg80 :low 0 :width 64) :exec (logand 18446744073709551615 reg80))))
Theorem:
(defthm n64p-mmx (unsigned-byte-p 64 (mmx i x86)) :rule-classes (:rewrite (:type-prescription :corollary (natp (mmx i x86)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mmx i x86)) (< (mmx i x86) 18446744073709551616)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))