---

{ [M,E:Type  Type].
    ([g:T:Type. (T  E[T])]. [f:T:Type. (M[T]  )].
     [P:process(P.M[P];P.E[P])].
       (forkable-process(f;g;P)  process(P.M[P];P.E[P]))) supposing 
       (Continuous+(T.E[T]) and 
       Continuous+(T.M[T])) }

{ Proof }

---

Definitions occuring in Statement :  forkable-process: forkable-process(f;g;P),  process: process(P.M[P];P.E[P]),  strong-type-continuous: Continuous+(T.F[T]),  bool: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  isect: x:A. B[x],  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  member: t  T,  forkable-process: forkable-process(f;g;P),  so_lambda: x.t[x],  so_lambda: x y.t[x; y],  so_lambda: so_lambda(x,y,z.t[x; y; z]),  all: x:A. B[x],  implies: P  Q,  so_apply: x[s1;s2],  so_apply: x[s1;s2;s3],  prop:
Lemmas :  recprocess_wf,  continuous-id,  process_wf,  ifthenelse_wf,  bool_wf,  strong-type-continuous_wf

---

\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}[g:\mcap{}T:Type.  (T  {}\mrightarrow{}  E[T])].  \mforall{}[f:\mcap{}T:Type.  (M[T]  {}\mrightarrow{}  \mBbbB{})].  \mforall{}[P:process(P.M[P];P.E[P])].
          (forkable-process(f;g;P)  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(T.E[T])  and 
          Continuous+(T.M[T]))


Date html generated: 2011_08_16-AM-09_54_08
Last ObjectModification: 2011_06_18-AM-08_36_19

Home Index