---

{ [A,B,S:Type]. [F:S  A  (S  bag(B))]. [s:S]. [buf:bag(B)].
    (seq-dataflow(rec-dataflow(s;s,a.F s 
                                     a);buffer-dataflow(buf;x.0 <z bag-size(x)))
    = rec-dataflow(<s, buf>;s,a.let s1,buf = s 
                                in let s',out = F s1 a 
                                   in <<s'
                                       , if 0 <z bag-size(out)
                                         then out
                                         else buf
                                         fi 
                                       >
                                      , buf
                                      >)) }

{ Proof }

---

Definitions occuring in Statement :  buffer-dataflow: buffer-dataflow(s;x.P[x]),  seq-dataflow: seq-dataflow(P;Q),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  dataflow: dataflow(A;B),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  uall: [x:A]. B[x],  apply: f a,  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  natural_number: $n,  universe: Type,  equal: s = t
Lemmas :  member_wf,  top_wf,  data-stream-cons,  data-stream_wf,  squash_wf,  true_wf,  ifthenelse_wf,  dataflow_wf,  dataflow-extensionality,  seq-dataflow_wf,  rec-dataflow_wf,  buffer-dataflow_wf,  lt_int_wf,  Error :bag-size_wf,  nat_wf,  Error :bag_wf

---

\mforall{}[A,B,S:Type].  \mforall{}[F:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  bag(B))].  \mforall{}[s:S].  \mforall{}[buf:bag(B)].
    (seq-dataflow(rec-dataflow(s;s,a.F  s  a);buffer-dataflow(buf;x.0  <z  bag-size(x)))
    =  rec-dataflow(<s,  buf>s,a.let  s1,buf  =  s 
                                                            in  let  s',out  =  F  s1  a 
                                                                  in  <<s',  if  0  <z  bag-size(out)  then  out  else  buf  fi  >,  buf>))


Date html generated: 2011_08_10-AM-08_21_16
Last ObjectModification: 2011_06_29-PM-03_19_01

Home Index