---

{ [A,B:Type]. [ins:A List]. [P:dataflow(A;bag(B))].
    (data-stream(delay-dataflow(P);ins) 
    ~ map(i.if null(filter(x.0 <z bag-size(x);firstn(i;data-stream(P;ins))))
             then {}
             else last(filter(x.0 <z bag-size(x);firstn(i;data-stream(P;ins))))
             fi ;upto(||ins||))) }

{ Proof }

---

Definitions occuring in Statement :  delay-dataflow: delay-dataflow(P),  data-stream: data-stream(P;L),  dataflow: dataflow(A;B),  firstn: firstn(n;as),  map: map(f;as),  length: ||as||,  null: null(as),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  lambda: x.A[x],  list: type List,  natural_number: $n,  universe: Type,  sqequal: s ~ t,  filter: filter(P;l),  last: last(L),  upto: upto(n)
Lemmas :  Error :empty-bag_wf,  delay-data-stream1,  Error :bag_wf,  dataflow_wf,  list_subtype_base,  subtype_base_sq,  data-stream_wf,  delay-dataflow_wf

---

\mforall{}[A,B:Type].  \mforall{}[ins:A  List].  \mforall{}[P:dataflow(A;bag(B))].
    (data-stream(delay-dataflow(P);ins) 
    \msim{}  map(\mlambda{}i.if  null(filter(\mlambda{}x.0  <z  bag-size(x);firstn(i;data-stream(P;ins))))
                      then  \{\}
                      else  last(filter(\mlambda{}x.0  <z  bag-size(x);firstn(i;data-stream(P;ins))))
                      fi  ;upto(||ins||)))


Date html generated: 2011_08_10-AM-08_18_15
Last ObjectModification: 2011_06_29-PM-03_54_25

Home Index