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