---

{ [A,C:Type]. [n:]. [B:n  Type]. [ds:k:n  dataflow(A;B[k])].
  [F:k:n  B[k]  C]. [L:A List].
    (better-parallel-dataflow(
     n;ds;
     F)*(L)
    = better-parallel-dataflow(
      n;if null(L) then ds else k.ds k*(L) fi ;
      F)) }

{ Proof }

---

Definitions occuring in Statement :  better-parallel-dataflow: better-parallel-dataflow,  iterate-dataflow: P*(inputs),  dataflow: dataflow(A;B),  null: null(as),  ifthenelse: if b then t else f fi ,  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
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  better-parallel-dataflow: better-parallel-dataflow,  ifthenelse: if b then t else f fi ,  null: null(as),  member: t  T,  all: x:A. B[x],  btrue: tt,  bfalse: ff,  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  pi1: fst(t),  top: Top,  true: True,  subtype: S  T,  rev_implies: P  Q,  iff: P  Q,  and: P  Q,  implies: P  Q,  squash: T,  nat: ,  so_apply: x[s1;s2],  prop:
Lemmas :  rec-dataflow_wf,  eval-parallel-dataflow_wf,  int_seg_wf,  dataflow_wf,  nat_wf,  better-parallel-dataflow_wf,  pi1_wf_top,  dataflow-ap_wf,  iterate-dataflow_wf,  squash_wf,  true_wf,  top_wf,  eval-parallel-dataflow-property

---

\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].
    (better-parallel-dataflow(
      n;ds;
      F)*(L)
    =  better-parallel-dataflow(
        n;if  null(L)  then  ds  else  \mlambda{}k.ds  k*(L)  fi  ;
        F))


Date html generated: 2011_08_10-AM-08_16_25
Last ObjectModification: 2011_06_18-AM-08_30_59

Home Index