---

{ [A,B,S:Type]. [s0:S]. [F:Top  Top  Top  P:Type
                                                    (S  P
                                                     S
                                                     A
                                                     (P  B))].
    (Y F s0  dataflow(A;B)) }

{ Proof }

---

Definitions occuring in Statement :  dataflow: dataflow(A;B),  uall: [x:A]. B[x],  top: Top,  ycomb: Y,  member: t  T,  apply: f a,  isect: x:A. B[x],  function: x:A  B[x],  product: x:A  B[x],  universe: Type,  isect2: T1  T2
Definitions :  uall: [x:A]. B[x],  member: t  T,  dataflow: dataflow(A;B),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  ycomb_wf_corec_parameter,  isect2_wf,  top_wf

---

\mforall{}[A,B,S:Type].  \mforall{}[s0:S].  \mforall{}[F:Top  {}\mrightarrow{}  Top  {}\mrightarrow{}  Top  \mcap{}  \mcap{}P:Type.  (S  {}\mrightarrow{}  P  {}\mrightarrow{}  S  {}\mrightarrow{}  A  {}\mrightarrow{}  (P  \mtimes{}  B))].
    (Y  F  s0  \mmember{}  dataflow(A;B))


Date html generated: 2011_08_10-AM-08_13_45
Last ObjectModification: 2011_06_18-AM-08_29_30

Home Index