Nuprl Definition : addrcos
addrcos(x) ==
λn.eval m = 16 * n in
eval xm = x m in
eval z = cosine((r(xm))/2 * m) m in
(((m * z) ÷ 4 * m) + (xm ÷ 4)) ÷ 4
Definitions occuring in Statement :
cosine: cosine(x),
int-rdiv: (a)/k1,
int-to-real: r(n),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
callbyvalue: callbyvalue,
apply: f a,
cosine: cosine(x),
int-rdiv: (a)/k1,
int-to-real: r(n),
add: n + m,
multiply: n * m,
divide: n ÷ m,
natural_number: $n
FDL editor aliases :
addrcos
Latex:
addrcos(x) ==
\mlambda{}n.eval m = 16 * n in
eval xm = x m in
eval z = cosine((r(xm))/2 * m) m in
(((m * z) \mdiv{} 4 * m) + (xm \mdiv{} 4)) \mdiv{} 4
Date html generated:
2017_10_04-PM-10_22_10
Last ObjectModification:
2017_03_01-PM-03_54_04
Theory : reals_2
Home
Index