---

{ [S,A,B:Type  Type].
    (let Proc = corec(P.A[P]  (P  B[P])) in
         s0:S[Proc]. next:T:{T:Type| Proc r T} 
                              (S[A[T]  (T  B[T])]  A[T]  (S[T]  B[T])).
           (rec-dataflow(s0;s,m.next[s;m])  Proc)) supposing 
       (Continuous+(T.B[T]) and 
       Continuous+(T.A[T]) and 
       Continuous+(T.S[T])) }

{ Proof }

---

Definitions occuring in Statement :  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  strong-type-continuous: Continuous+(T.F[T]),  subtype_rel: A r B,  let: let,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  all: x:A. B[x],  member: t  T,  set: {x:A| B[x]} ,  isect: x:A. B[x],  function: x:A  B[x],  product: x:A  B[x],  universe: Type,  corec: corec(T.F[T])
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  strong-type-continuous: Continuous+(T.F[T]),  so_apply: x[s],  let: let,  all: x:A. B[x],  member: t  T,  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  so_apply: x[s1;s2],  ext-eq: A  B,  and: P  Q,  isect2: T1  T2,  top: Top,  so_lambda: x.t[x],  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  implies: P  Q,  bool: ,  unit: Unit,  it: ,  prop:
Lemmas :  nat_wf,  ycomb_wf_corec_parameter3,  top_wf,  bool_wf,  corec_wf,  strong-type-continuous_wf

---

\mforall{}[S,A,B:Type  {}\mrightarrow{}  Type].
    (let  Proc  =  corec(P.A[P]  {}\mrightarrow{}  (P  \mtimes{}  B[P]))  in
              \mforall{}s0:S[Proc].  \mforall{}next:\mcap{}T:\{T:Type|  Proc  \msubseteq{}r  T\}  .  (S[A[T]  {}\mrightarrow{}  (T  \mtimes{}  B[T])]  {}\mrightarrow{}  A[T]  {}\mrightarrow{}  (S[T]  \mtimes{}  B[T])).
                  (rec-dataflow(s0;s,m.next[s;m])  \mmember{}  Proc))  supposing 
          (Continuous+(T.B[T])  and 
          Continuous+(T.A[T])  and 
          Continuous+(T.S[T]))


Date html generated: 2011_08_10-AM-08_14_00
Last ObjectModification: 2011_06_18-AM-08_29_41

Home Index