Nuprl Lemma : better-parallel-data-stream

{

[A,C:Type].

[n:

].

[B:

n

Type].

[ds:k:

n

dataflow(A;B[k])].

[F:k:

n

B[k]

C].

[L:A List].
    (data-stream(better-parallel-dataflow(
                 n;ds;
                 F);L)
    = map(

i.(F (

k.data-stream(ds k;L)[i]));upto(||L||))) }

{ Proof }

Definitions occuring in Statement : better-parallel-dataflow: better-parallel-dataflow, data-stream: data-stream(P;L), dataflow: dataflow(A;B), select: l[i], map: map(f;as), length: ||as||, int_seg: {i..j

}, nat:

, uall:

[x:A]. B[x], so_apply: x[s], apply: f a, lambda:

x.A[x], function: x:A

B[x], list: type List, natural_number: $n, universe: Type, equal: s = t, upto: upto(n)
Definitions : uall:

[x:A]. B[x], so_apply: x[s], better-parallel-dataflow: better-parallel-dataflow, member: t

T, parallel-dataflow: parallel-dataflow, top: Top, all:

x:A. B[x], subtype: S

T, pi2: snd(t), pi1: fst(t), prop:

, so_lambda:

x y.t[x; y], so_lambda:

x.t[x], nat:

, so_apply: x[s1;s2], guard: {T}
Lemmas : parallel-data-stream, top_wf, int_seg_wf, dataflow_wf, nat_wf, eval-parallel-dataflow-property, dataflow-out_wf, data-stream_wf, pi1_wf_top, rec-dataflow_wf, eval-parallel-dataflow_wf, parallel-dataflow_wf, dataflow-ap_wf, nat_properties, data-stream-cons

\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]. \mforall{}[L:A List]. (data-stream(better-parallel-dataflow( n;ds; F);L) = map(\mlambda{}i.(F (\mlambda{}k.data-stream(ds k;L)[i]));upto(||L||))) Date html generated: 2011_08_10-AM-08_16_29 Last ObjectModification: 2011_06_18-AM-08_31_02 Home Index