Nuprl Definition : log-from
log-from(a;b) == λn.eval m = 4 * n in eval m2 = 2 * m in eval N = cubic_converge(10;m2) in logseq(a;b;N) m ÷ 4
Definitions occuring in Statement :
logseq: logseq(a;b;n),
cubic_converge: cubic_converge(b;m),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
logseq: logseq(a;b;n),
apply: f a,
cubic_converge: cubic_converge(b;m),
callbyvalue: callbyvalue,
multiply: n * m,
divide: n ÷ m,
lambda: λx.A[x]
FDL editor aliases :
log-from
Latex:
log-from(a;b) ==
\mlambda{}n.eval m = 4 * n in
eval m2 = 2 * m in
eval N = cubic\_converge(10;m2) in
logseq(a;b;N) m \mdiv{} 4
Date html generated:
2016_10_26-PM-00_37_33
Last ObjectModification:
2016_09_18-PM-10_09_34
Theory : reals_2
Home
Index