Nuprl Definition : mu-ge
mu-ge(f;n)==r if f n then n else eval m = n + 1 in mu-ge(f;m) fi
mu-ge(f;n) == fix((λmu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi )) n
Definitions occuring in Statement :
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
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
callbyvalue: callbyvalue,
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
mu-ge
Latex:
mu-ge(f;n)==r if f n then n else eval m = n + 1 in mu-ge(f;m) fi
Latex:
mu-ge(f;n) == fix((\mlambda{}mu-ge,n. if f n then n else eval m = n + 1 in mu-ge m fi )) n
Date html generated:
2016_05_14-AM-07_28_32
Last ObjectModification:
2015_09_22-PM-05_46_29
Theory : int_2
Home
Index