(n512 x) → *
Function:
(defun n512$inline (x) (declare (xargs :guard (integerp x))) (mbe :logic (loghead 512 x) :exec (logand 13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084095 x)))