{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [ds:k:n dataflow(A;B[k])].
[F:k:n B[k] C].
(parallel-dataflow(
ds;
F) 
dataflow(A;C)) }
{ Proof }
Definitions occuring in Statement :
parallel-dataflow: parallel-dataflow,
dataflow: dataflow(A;B),
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
parallel-dataflow: parallel-dataflow,
so_lambda: 
x y.t[x; y],
top: Top,
all: x:A. B[x],
subtype: S 
T,
nat: ,
so_apply: x[s1;s2]
Lemmas :
rec-dataflow_wf,
pi1_wf_top,
dataflow_wf,
dataflow-ap_wf,
int_seg_wf,
dataflow-out_wf,
nat_wf
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C].
(parallel-dataflow(
ds;
F) \mmember{} dataflow(A;C))
Date html generated:
2011_08_10-AM-08_15_41
Last ObjectModification:
2011_06_18-AM-08_30_35
Home
Index