Nuprl Definition : nat-star-retract
nat-star-retract(s) == λn.if (∃i∈upto(n).0 <z s i)_b then 0 else s n fi
Definitions occuring in Statement :
bl-exists: (∃x∈L.P[x])_b,
upto: upto(n),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
apply: f a,
natural_number: $n,
lt_int: i <z j,
upto: upto(n),
bl-exists: (∃x∈L.P[x])_b,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x]
FDL editor aliases :
nat-star-retract
Latex:
nat-star-retract(s) == \mlambda{}n.if (\mexists{}i\mmember{}upto(n).0 <z s i)\_b then 0 else s n fi
Date html generated:
2016_12_12-AM-09_24_09
Last ObjectModification:
2016_11_18-AM-10_09_21
Theory : continuity
Home
Index