Nuprl Definition : rsum'
rsum'(n;m;k.x[k]) ==
eval n' = n in
eval m' = m in
eval k = (m' - n') + 1 in
if (k) < (1) then r0 else eval k2 = 2 * k in λj.eval m = k2 * j in Σ(x[n + i] m | i < k) ÷ k2
Definitions occuring in Statement :
int-to-real: r(n),
sum: Σ(f[x] | x < k),
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
subtract: n - m,
less: if (a) < (b) then c else d,
int-to-real: r(n),
natural_number: $n,
lambda: λx.A[x],
callbyvalue: callbyvalue,
multiply: n * m,
divide: n ÷ m,
sum: Σ(f[x] | x < k),
apply: f a,
add: n + m
FDL editor aliases :
rsum'
Latex:
rsum'(n;m;k.x[k]) ==
eval n' = n in
eval m' = m in
eval k = (m' - n') + 1 in
if (k) < (1) then r0 else eval k2 = 2 * k in \mlambda{}j.eval m = k2 * j in \mSigma{}(x[n + i] m | i < k) \mdiv{} k2
Date html generated:
2016_05_18-AM-07_41_23
Last ObjectModification:
2015_09_23-AM-09_02_27
Theory : reals
Home
Index