(i09 x) → *
Function: i09$inline
(defun i09$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (logext 9 x) :exec (fast-logext 9 x)))
