Nuprl Definition : cubic_converge
cubic_converge(b;m)==r if m ≤z b then 0 else eval r = iroot(3;m) + 1 in eval n = cubic_converge(b;r) in n + 1 fi
cubic_converge(b;m) ==
fix((λcubic_converge,m. if m ≤z b then 0 else eval r = iroot(3;m) + 1 in eval n = cubic_converge r in n + 1 fi )) m
Definitions occuring in Statement :
le_int: i ≤z j,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n,
iroot: iroot(n;x)
Definitions occuring in definition :
natural_number: $n,
add: n + m,
apply: f a,
callbyvalue: callbyvalue,
iroot: iroot(n;x),
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
fix: fix(F)
FDL editor aliases :
cubic_converge
Latex:
cubic\_converge(b;m)
==r if m \mleq{}z b then 0 else eval r = iroot(3;m) + 1 in eval n = cubic\_converge(b;r) in n + 1 fi
Latex:
cubic\_converge(b;m) ==
fix((\mlambda{}cubic$_{converge}$,m. if m \mleq{}z b
then 0
else eval r = iroot(3;m) + 1 in
eval n = cubic$_{converge}$ r in
n + 1
fi ))
m
Date html generated:
2016_10_26-PM-00_22_05
Last ObjectModification:
2016_09_12-PM-05_42_22
Theory : reals_2
Home
Index