{ 
[A:Type]. [F:A 
Top]. [G:Top]. [as:A List].
(data-stream(better-parallel-dataflow(
1;
k.[stateless-dataflow(a.F[a])][k];
g.G[g 0]);as)
~ data-stream(stateless-dataflow(a.G[F[a]]);as)) }
{ Proof }
Definitions occuring in Statement :
better-parallel-dataflow: better-parallel-dataflow,
data-stream: data-stream(P;L),
stateless-dataflow: stateless-dataflow(m.f[m]),
select: l[i],
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 :
dataflow-ap: df(a),
select-tuple: Error :select-tuple,
pi1: fst(t),
stateless_dataflow_ap: stateless_dataflow_ap{stateless_dataflow_ap_compseq_tag_def:o}(a; v21.f[v21]),
eq_int: (i =
j),
pi2: snd(t),
void: Void,
subtype: S 
T,
rec_dataflow_ap: rec_dataflow_ap_compseq_tag_def,
natural_number: $n,
eval-parallel-dataflow: eval-parallel-dataflow(n;s;m),
spread: spread def,
nil: [],
stateless-dataflow: stateless-dataflow(m.f[m]),
cons: [car / cdr],
select: l[i],
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
data-stream: data-stream(P;L),
data_stream_nil: data_stream_nil{data_stream_nil_compseq_tag_def:o}(P),
better-parallel-dataflow: better-parallel-dataflow,
apply: f a,
lambda: x.A[x],
all: x:A. B[x],
equal: s = t,
universe: Type,
function: x:A B[x],
sqequal: s ~ t,
top: Top,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
member: t 
T,
list: type List,
Try: Error :Try,
CollapseTHEN: Error :CollapseTHEN,
Auto: Error :Auto,
THENM: Error :THENM,
CollapseTHENA: Error :CollapseTHENA,
Unfold: Error :Unfold,
it: 
,
so_apply: x[s],
pair: <a, b>,
so_lambda: 
x y.t[x; y],
unit: Unit,
tactic: Error :tactic,
ifthenelse: if b then t else f fi
Lemmas :
parallel-1-rec-dataflow,
unit_wf,
it_wf,
data-stream-cons,
member_wf,
top_wf
\mforall{}[A:Type]. \mforall{}[F:A {}\mrightarrow{} Top]. \mforall{}[G:Top]. \mforall{}[as:A List].
(data-stream(better-parallel-dataflow(
1;\mlambda{}k.[stateless-dataflow(a.F[a])][k];
\mlambda{}g.G[g 0]);as) \msim{} data-stream(stateless-dataflow(a.G[F[a]]);as))
Date html generated:
2011_08_10-AM-08_16_16
Last ObjectModification:
2011_06_18-AM-08_30_53
Home
Index