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),
le_int: i ≤z j,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
isqrt: isqrt(x),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
add: n + m,
multiply: n * m,
subtract: n - m,
natural_number: $n
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:
2016_05_15-PM-05_20_12
Last ObjectModification:
2015_09_23-AM-07_53_16
Theory : general
Home
Index