Nuprl Lemma : better-parallel-dataflow

{

[A,C:Type].

[n:

].

[B:

n

Type].

[ds:k:

n

dataflow(A;B[k])].

[F:k:

n

B[k]

C].
    (better-parallel-dataflow(
     n;ds;
     F)

dataflow(A;C)) }

{ Proof }

Definitions occuring in Statement : better-parallel-dataflow: better-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, better-parallel-dataflow: better-parallel-dataflow, so_lambda:

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

x.t[x], nat:

, so_apply: x[s1;s2]
Lemmas : rec-dataflow_wf, eval-parallel-dataflow_wf, int_seg_wf, dataflow_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]. (better-parallel-dataflow( n;ds; F) \mmember{} dataflow(A;C)) Date html generated: 2011_08_10-AM-08_15_55 Last ObjectModification: 2011_06_18-AM-08_30_44 Home Index