Nuprl Definition : gen_fin_spr
gen_fin_spr(g) == spr(g) 
(
a:
List. (((g a) = 0) 
(
b:. s:. (((g (a @ [s])) = 0) (s 
b)))))
Definitions occuring in Statement :
append: as @ bs,
nat: ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
natural_number: $n,
equal: s = t
FDL editor aliases :
gen_fin_spr
gen\_fin\_spr(g) ==
spr(g) \mwedge{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} (\mexists{}b:\mBbbN{}. \mforall{}s:\mBbbN{}. (((g (a @ [s])) = 0) {}\mRightarrow{} (s \mleq{} b)))))
Date html generated:
2013_03_20-AM-10_37_18
Last ObjectModification:
2013_03_12-PM-06_55_43
Home
Index