N512-to-i512
- Signature
(n512-to-i512 x) → *
- Arguments
- x — Guard (n512p x).
Definitions and Theorems
Function: n512-to-i512$inline
(defun n512-to-i512$inline (x)
(declare (type (unsigned-byte 512) x))
(declare (xargs :guard (n512p x)))
(mbe
:logic (logext 512 x)
:exec
(if
(<
x
6703903964971298549787012499102923063739682910296196688861780721860882015036773488400937149083451713845015929093243025426876941405973284973216824503042048)
x
(-
x
13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096))))
