---

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

{ Proof }

---

Definitions occuring in Statement :  buffer-dataflow: buffer-dataflow(s;x.P[x]),  seq-dataflow: seq-dataflow(P;Q),  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 :  top_wf,  member_wf,  length-data-stream,  data-stream_wf,  Error :bag_wf,  buffer-data-stream,  nat_wf,  Error :bag-size_wf,  lt_int_wf,  buffer-dataflow_wf,  seq-data-stream,  dataflow_wf

---

\mforall{}[A,B:Type].  \mforall{}[ins:A  List].  \mforall{}[P:dataflow(A;bag(B))].  \mforall{}[init:bag(B)].
    (data-stream(seq-dataflow(P;buffer-dataflow(init;x.0  <z  bag-size(x)));ins) 
    \msim{}  map(\mlambda{}i.if  null(filter(\mlambda{}x.0  <z  bag-size(x);firstn(i;data-stream(P;ins))))
                      then  init
                      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_12
Last ObjectModification: 2011_06_29-PM-03_53_33

Home Index