(n20 x) → *
Function: n20$inline
(defun n20$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 20 x) :exec (logand 1048575 x)))
