---

{ [A,S1,S2:Type]. [F1:S1  A  (S1  Top)]. [F2:S2  A  (S2  Top)].
  [G,P:Top]. [as:A List]. [s1:S1]. [s2:S2]. [buf:Top].
    (data-stream(better-feedback-dataflow(2;k.[rec-dataflow(s1;s,a.F1[s;a]); 
                                                
                                                rec-dataflow(s2;
                                                s,a.F2[s;a])][k];
                 g,x.G[g 0;g 1;x];buf;s.P[s]);as) 
    ~ data-stream(rec-dataflow(<s1, s2, buf>;s,a.let s1,s2,buf = s in 
                  let s1',out1 = F1[s1;a] 
                  in let s2',out2 = F2[s2;a] 
                     in let x = G[out1;out2;buf] in
                            <<s1', s2', if P[x] then x else buf fi >, x>);as)) }

{ Proof }

---

Definitions occuring in Statement :  better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),  data-stream: data-stream(P;L),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  select: l[i],  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread3,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  so_apply: x[s],  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  product: x:A  B[x],  cons: [car / cdr],  nil: [],  list: type List,  natural_number: $n,  universe: Type,  sqequal: s ~ t
Definitions :  uall: [x:A]. B[x],  top: Top,  member: t  T,  all: x:A. B[x],  subtype: S  T,  better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),  select: l[i],  so_apply: x[s1;s2],  spreadn: spread3,  let: let,  ifthenelse: if b then t else f fi ,  pi2: snd(t),  dataflow-ap: df(a),  eval-parallel-dataflow: eval-parallel-dataflow(n;s;m),  primrec: primrec(n;b;c),  select-tuple: select-tuple,  ycomb: Y,  eq_int: (i = j),  btrue: tt,  bfalse: ff,  le_int: i z j,  bnot: b,  lt_int: i <z j,  implies: P  Q,  pi1: fst(t),  rec-dataflow: rec-dataflow(s0;s,m.next[s; m])
Lemmas :  top_wf,  data-stream-cons,  pi1_wf_top

---

\mforall{}[A,S1,S2:Type].  \mforall{}[F1:S1  {}\mrightarrow{}  A  {}\mrightarrow{}  (S1  \mtimes{}  Top)].  \mforall{}[F2:S2  {}\mrightarrow{}  A  {}\mrightarrow{}  (S2  \mtimes{}  Top)].  \mforall{}[G,P:Top].  \mforall{}[as:A  List].
\mforall{}[s1:S1].  \mforall{}[s2:S2].  \mforall{}[buf:Top].
    (data-stream(better-feedback-dataflow(2;\mlambda{}k.[rec-dataflow(s1;s,a.F1[s;a]); 
                                                                                           
                                                                                            rec-dataflow(s2;s,a.F2[s;a])][k];
                              \mlambda{}g,x.G[g  0;g  1;x];buf;s.P[s]);as) 
    \msim{}  data-stream(rec-dataflow(<s1,  s2,  buf>s,a.let  s1,s2,buf  =  s  in 
                                let  s1',out1  =  F1[s1;a] 
                                in  let  s2',out2  =  F2[s2;a] 
                                      in  let  x  =  G[out1;out2;buf]  in
                                                    <<s1',  s2',  if  P[x]  then  x  else  buf  fi  >,  x>);as))


Date html generated: 2011_08_10-AM-08_19_03
Last ObjectModification: 2011_06_18-AM-08_31_57

Home Index