(n21 x) → *
Function: n21$inline
(defun n21$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 21 x) :exec (logand 2097151 x)))
