---

{ [A,B,S:Type]. [F:S  A  (S  bag(B))]. [s:S].
    (delay-dataflow(rec-dataflow(s;s,a.F s a))
    = rec-dataflow(<s, {}>;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 :  delay-dataflow: delay-dataflow(P),  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 :  iff_wf,  rev_implies_wf,  delay-equiv1,  delay-dataflow_wf,  rec-dataflow_wf,  Error :empty-bag_wf,  dataflow_wf,  Error :bag_wf

---

\mforall{}[A,B,S:Type].  \mforall{}[F:S  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  bag(B))].  \mforall{}[s:S].
    (delay-dataflow(rec-dataflow(s;s,a.F  s  a))
    =  rec-dataflow(<s,  \{\}>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_19
Last ObjectModification: 2011_06_29-PM-03_22_04

Home Index