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