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