Nuprl Definition : spr
spr(g) == 
a:
List. ((((g a) = 0) 
(
s:. ((g (a @ [s])) = 0))) 
(((g a) > 0) (s:. ((g (a @ [s])) > 0))))
Definitions occuring in Statement :
append: as @ bs,
nat: ,
gt: i > j,
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 :
spr
spr
spr(g) ==
\mforall{}a:\mBbbN{} List
((((g a) = 0) {}\mRightarrow{} (\mexists{}s:\mBbbN{}. ((g (a @ [s])) = 0))) \mwedge{} (((g a) > 0) {}\mRightarrow{} (\mforall{}s:\mBbbN{}. ((g (a @ [s])) > 0))))
Date html generated:
2013_03_20-AM-10_32_08
Last ObjectModification:
2013_03_01-PM-05_37_04
Home
Index