Nuprl Definition : ratbound
ratbound(x) ==
let a,b = x
in eval a' = |a| in
eval r = a' rem b in
eval q = a' ÷ b in
if r=0 then if q=0 then 1 else q else (q + 1)
Definitions occuring in Statement :
absval: |i|,
callbyvalue: callbyvalue,
int_eq: if a=b then c else d,
spread: spread def,
remainder: n rem m,
divide: n ÷ m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
spread: spread def,
absval: |i|,
remainder: n rem m,
callbyvalue: callbyvalue,
divide: n ÷ m,
int_eq: if a=b then c else d,
add: n + m,
natural_number: $n
FDL editor aliases :
ratbound
Latex:
ratbound(x) ==
let a,b = x
in eval a' = |a| in
eval r = a' rem b in
eval q = a' \mdiv{} b in
if r=0 then if q=0 then 1 else q else (q + 1)
Date html generated:
2019_10_30-AM-09_32_47
Last ObjectModification:
2019_01_11-PM-00_31_34
Theory : reals
Home
Index