Nuprl Definition : weak_fan_th
weak_fan_th() ==
  R: List  
    (((l1,l2: List.  (((R l1))  ((R (l1 @ l2)))))  (A:  . n:. ((R mklist(n;A)))))
     (n:. A:  . ((R mklist(n;A)))))
Definitions occuring in Statement : 
append: as @ bs, 
assert: b, 
bool: , 
nat: , 
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 : 
weak_fan_th
weak\_fan\_th()  ==
    \mforall{}R:\mBbbB{}  List  {}\mrightarrow{}  \mBbbB{}
        (((\mforall{}l1,l2:\mBbbB{}  List.    ((\muparrow{}(R  l1))  {}\mRightarrow{}  (\muparrow{}(R  (l1  @  l2)))))  \mwedge{}  (\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  mklist(n;A)))))
        {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\muparrow{}(R  mklist(n;A)))))
Date html generated:
2013_03_20-AM-09_50_45
Last ObjectModification:
2012_11_27-AM-10_32_07
Home
Index