Nuprl Definition : fb-to-cantor
fb-to-cantor(b;f;n) ==
eval m = mu(λm.n <z Σ(b j | j < m)) - 1 in
eval k = Σ(b j | j < m) in
eval i = n - k in
(i =z f m)
Definitions occuring in Statement :
sum: Σ(f[x] | x < k),
mu: mu(f),
callbyvalue: callbyvalue,
lt_int: i <z j,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
mu: mu(f),
lambda: λx.A[x],
lt_int: i <z j,
natural_number: $n,
sum: Σ(f[x] | x < k),
callbyvalue: callbyvalue,
subtract: n - m,
eq_int: (i =z j),
apply: f a
FDL editor aliases :
fb-to-cantor
Latex:
fb-to-cantor(b;f;n) ==
eval m = mu(\mlambda{}m.n <z \mSigma{}(b j | j < m)) - 1 in
eval k = \mSigma{}(b j | j < m) in
eval i = n - k in
(i =\msubz{} f m)
Date html generated:
2016_05_15-PM-05_26_39
Last ObjectModification:
2015_09_23-AM-07_54_15
Theory : general
Home
Index