---

{ [A,S:Type]. [F:S  A  (S  Top)]. [G,P:Top]. [as:A List]. [s:S].
  [s2:Top].
    (data-stream(better-feedback-dataflow(1;k.[rec-dataflow(s;s,a.F[s;a])][k];
                 g,x.G[g 0;x];s2;s.P[s]);as) 
    ~ data-stream(rec-dataflow(<s, s2>;s,a.let s1,s2 = s 
                                           in let s',out = F[s1;a] 
                                              in <<s'
                                                  , if P[G[out;s2]]
                                                    then G[out;s2]
                                                    else s2
                                                    fi 
                                                  >
                                                 , G[out;s2]
                                                 >);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 ,  uall: [x:A]. B[x],  top: Top,  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 :  pi1: fst(t),  implies: P  Q,  subtype: S  T,  all: x:A. B[x],  member: t  T,  lt_int: i <z j,  bnot: b,  le_int: i z j,  bfalse: ff,  btrue: tt,  eq_int: (i = j),  ycomb: Y,  select-tuple: select-tuple,  primrec: primrec(n;b;c),  eval-parallel-dataflow: eval-parallel-dataflow(n;s;m),  dataflow-ap: df(a),  pi2: snd(t),  ifthenelse: if b then t else f fi ,  so_apply: x[s1;s2],  select: l[i],  better-feedback-dataflow: better-feedback-dataflow(n;ds;F;s;x.P[x]),  top: Top
Lemmas :  top_wf

---

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


Date html generated: 2011_08_10-AM-08_18_57
Last ObjectModification: 2011_06_18-AM-08_31_54

Home Index