(n80 x) → *
Function: n80$inline
(defun n80$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 80 x) :exec (logand 1208925819614629174706175 x)))
