Nuprl Definition : fib
fib(n) == fix((λfib,n. if (n =z 0) ∨b(n =z 1) then 1 else (fib (n - 1)) + (fib (n - 2)) fi )) n
Definitions occuring in Statement :
bor: p ∨bq
,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
apply: f a
,
fix: fix(F)
,
lambda: λx.A[x]
,
subtract: 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
,
bor: p ∨bq
,
eq_int: (i =z j)
,
add: n + m
,
apply: f a
,
subtract: n - m
,
natural_number: $n
FDL editor aliases :
fib
Latex:
fib(n) == fix((\mlambda{}fib,n. if (n =\msubz{} 0) \mvee{}\msubb{}(n =\msubz{} 1) then 1 else (fib (n - 1)) + (fib (n - 2)) fi )) n
Date html generated:
2016_05_14-PM-04_25_06
Last ObjectModification:
2015_09_22-PM-06_02_47
Theory : num_thy_1
Home
Index