{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [F:k:n B[k] C]. [G:Top].
[as:A List]. [ds:k:n dataflow(A;B[k])].
(data-stream(better-parallel-dataflow(
1;
k.[better-parallel-dataflow(n;ds;F)][k];
g.G[g 0]);as) ~ data-stream(better-parallel-dataflow(
n;ds;
s.G[F s]);as)) }
{ Proof }
Definitions occuring in Statement :
better-parallel-dataflow: better-parallel-dataflow,
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
select: l[i],
int_seg: {i..j
},
nat: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s],
apply: f a,
lambda: x.A[x],
function: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
natural_number: $n,
universe: Type,
sqequal: s ~ t
Definitions :
so_apply: x[s],
top: Top,
better-parallel-dataflow: better-parallel-dataflow,
member: t 
T,
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
all: x:A. B[x],
subtype: S 
T,
pi2: snd(t),
pi1: fst(t),
implies: P 
Q,
nat: ,
uall: [x:A]. B[x],
so_apply: x[s1;s2]
Lemmas :
parallel-1-rec-dataflow,
eval-parallel-dataflow_wf,
int_seg_wf,
dataflow_wf,
top_wf,
nat_wf,
data-stream-cons
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C]. \mforall{}[G:Top]. \mforall{}[as:A List].
\mforall{}[ds:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])].
(data-stream(better-parallel-dataflow(
1;\mlambda{}k.[better-parallel-dataflow(n;ds;F)][k];
\mlambda{}g.G[g 0]);as) \msim{} data-stream(better-parallel-dataflow(
n;ds;
\mlambda{}s.G[F s]);as))
Date html generated:
2011_08_10-AM-08_16_20
Last ObjectModification:
2011_06_18-AM-08_30_56
Home
Index