{ 
[A,B:Type]. [L:A List]. [P:dataflow(A;B)]. (data-stream(P;L) 
B List) }
{ Proof }
Definitions occuring in Statement :
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
data-stream: data-stream(P;L),
so_lambda: 
x.t[x],
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
int_seg: {i..j
},
so_apply: x[s],
lelt: i j < k,
uimplies: b supposing a,
and: P 
Q
Lemmas :
map_wf,
int_seg_wf,
length_wf2,
upto_wf,
pi2_wf,
dataflow-ap_wf,
iterate-dataflow_wf,
firstn_wf,
select_wf,
dataflow_wf,
length_wf1
\mforall{}[A,B:Type]. \mforall{}[L:A List]. \mforall{}[P:dataflow(A;B)]. (data-stream(P;L) \mmember{} B List)
Date html generated:
2011_08_10-AM-08_14_29
Last ObjectModification:
2011_06_18-AM-08_29_56
Home
Index