Nuprl Definition : fan_26_7a
fan_26_7a{i:l}() ==
g:
List 
. R: List 
.
(gen_fin_spr(g)
(a: List. (((g a) = 0) Dec(R a)))
(f: . ((x:. ((g mklist(x;f)) = 0)) (
x:. (R mklist(x;f)))))
(z:. f: . ((x:. ((g mklist(x;f)) = 0)) (x:. ((R mklist(x;f)) 
(x 
z))))))
Definitions occuring in Statement :
gen_fin_spr: gen_fin_spr(g),
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],
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
FDL editor aliases :
fan_26_7a
fan\_26\_7a\{i:l\}() ==
\mforall{}g:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}R:\mBbbN{} List {}\mrightarrow{} \mBbbP{}.
(gen\_fin\_spr(g)
{}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} Dec(R a)))
{}\mRightarrow{} (\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}x:\mBbbN{}. ((g mklist(x;f)) = 0)) {}\mRightarrow{} (\mexists{}x:\mBbbN{}. (R mklist(x;f)))))
{}\mRightarrow{} (\mexists{}z:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}x:\mBbbN{}. ((g mklist(x;f)) = 0)) {}\mRightarrow{} (\mexists{}x:\mBbbN{}. ((R mklist(x;f)) \mwedge{} (x \mleq{} z))))))
Date html generated:
2013_03_20-AM-10_37_24
Last ObjectModification:
2013_03_12-PM-03_12_13
Home
Index