---

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

{ Proof }

---

Definitions occuring in Statement :  dataflow: dataflow(A;B),  uall: [x:A]. B[x],  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
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

---

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


Date html generated: 2011_08_10-AM-08_13_42
Last ObjectModification: 2011_06_18-AM-08_29_27

Home Index