(!mmx i v x86) → x86
Function:
(defun !mmx$inline (i v x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 7) i) (type (unsigned-byte 64) v)) (let ((val80 (mbe :logic (part-install 65535 v :low 64 :high 79) :exec (the (unsigned-byte 80) (logior 1208907372870555465154560 v))))) (!fp-datai i val80 x86)))
Theorem:
(defthm x86p-!mmx (implies (x86p x86) (x86p (!mmx i v x86))))