{ 
[A,C:Type]. [n:
]. [B:n 
Type]. [F:k:n B[k] C].
[ds1,ds2:k:n dataflow(A;B[k])].
better-parallel-dataflow(
n;ds1;
F) 
better-parallel-dataflow(
n;ds2;
F)
supposing k:n. ds1 k ds2 k }
{ Proof }
Definitions occuring in Statement :
dataflow-equiv: d1 d2,
better-parallel-dataflow: better-parallel-dataflow,
dataflow: dataflow(A;B),
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
apply: f a,
function: x:A B[x],
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
all: x:A. B[x],
dataflow-equiv: d1 d2,
member: t 
T,
prop: 
,
le: A 
B,
squash: 
T,
true: True,
and: P 
Q,
not: 
A,
implies: P 
Q,
false: False,
top: Top,
subtype: S 
T,
rev_implies: P 
Q,
iff: P Q,
so_lambda: 
x.t[x],
nat: ,
int_seg: {i..j},
lelt: i j < k,
guard: {T}
Lemmas :
int_seg_wf,
dataflow-equiv_wf,
dataflow_wf,
nat_wf,
map_wf,
squash_wf,
true_wf,
length_wf1,
upto_wf,
select_wf,
le_wf,
length-data-stream,
top_wf,
better-parallel-data-stream
\mforall{}[A,C:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[B:\mBbbN{}n {}\mrightarrow{} Type]. \mforall{}[F:k:\mBbbN{}n {}\mrightarrow{} B[k] {}\mrightarrow{} C]. \mforall{}[ds1,ds2:k:\mBbbN{}n {}\mrightarrow{} dataflow(A;B[k])].
better-parallel-dataflow(
n;ds1;
F) \mequiv{} better-parallel-dataflow(
n;ds2;
F)
supposing \mforall{}k:\mBbbN{}n. ds1 k \mequiv{} ds2 k
Date html generated:
2011_08_10-AM-08_22_02
Last ObjectModification:
2011_06_18-AM-08_32_36
Home
Index