Nuprl Definition : tsqrt
tsqrt(n) == eval r = isqrt(2 * n) in if (r * r) + r ≤z 2 * n then r else r - 1 fi
Definitions occuring in Statement :
isqrt: isqrt(x),
callbyvalue: callbyvalue,
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
subtract: n - m,
multiply: n * m,
add: n + m,
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
isqrt: isqrt(x),
callbyvalue: callbyvalue
FDL editor aliases :
tsqrt
Latex:
tsqrt(n) == eval r = isqrt(2 * n) in if (r * r) + r \mleq{}z 2 * n then r else r - 1 fi
Date html generated:
2019_06_20-PM-02_38_25
Last ObjectModification:
2019_06_12-PM-00_26_49
Theory : num_thy_1
Home
Index