Nuprl Definition : fan_26_6a
fan_26_6a{i:l}() ==
B:
List 
. R: List 
.
((a: List. Dec(R a))
(f:fin_spr(B). 
x:. (R mklist(x;f)))
(z:. f:fin_spr(B). x:. ((x 
z) 
(R mklist(x;f)))))
Definitions occuring in Statement :
fin_spr: fin_spr(B),
nat: ,
decidable: Dec(P),
prop: ,
le: A B,
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
function: x:A B[x],
mklist: mklist(n;f)
FDL editor aliases :
fan_26_6a
fan\_26\_6a\{i:l\}() ==
\mforall{}B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}R:\mBbbN{} List {}\mrightarrow{} \mBbbP{}.
((\mforall{}a:\mBbbN{} List. Dec(R a))
{}\mRightarrow{} (\mforall{}f:fin\_spr(B). \mexists{}x:\mBbbN{}. (R mklist(x;f)))
{}\mRightarrow{} (\mexists{}z:\mBbbN{}. \mforall{}f:fin\_spr(B). \mexists{}x:\mBbbN{}. ((x \mleq{} z) \mwedge{} (R mklist(x;f)))))
Date html generated:
2013_03_20-AM-10_34_53
Last ObjectModification:
2013_03_10-PM-08_52_24
Home
Index