Nuprl Definition : log
log(b;n) == fix((λlog,n. if n <z b then 0 else (log (n ÷ b)) + 1 fi )) n
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
divide: n ÷ m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
add: n + m,
apply: f a,
divide: n ÷ m,
natural_number: $n
FDL editor aliases :
log
Latex:
log(b;n) == fix((\mlambda{}log,n. if n <z b then 0 else (log (n \mdiv{} b)) + 1 fi )) n
Date html generated:
2016_05_15-PM-04_48_57
Last ObjectModification:
2015_09_23-AM-07_50_34
Theory : general
Home
Index