---

{ [S,M,E:Type  Type].
    ([s0:S[process(P.M[P];P.E[P])]]. [next:T:{T:Type| 
                                                 process(P.M[P];P.E[P]) r T} 
                                               (S[M[T]  (T  E[T])]
                                                M[T]
                                                (S[T]  E[T]))].
       (RecProcess(s0;s,m.next[s;m])  process(P.M[P];P.E[P]))) supposing 
       (Continuous+(T.E[T]) and 
       Continuous+(T.M[T]) and 
       Continuous+(T.S[T])) }

{ Proof }

---

Definitions occuring in Statement :  rec-process: RecProcess(s0;s,m.next[s; m]),  process: process(P.M[P];P.E[P]),  strong-type-continuous: Continuous+(T.F[T]),  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  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
Definitions :  and: P  Q,  ext-eq: A  B,  bool: ,  corec: corec(T.F[T]),  let: let,  rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),  implies: P  Q,  axiom: Ax,  so_apply: x[s1;s2],  rec-process: RecProcess(s0;s,m.next[s; m]),  subtype_rel: A r B,  set: {x:A| B[x]} ,  product: x:A  B[x],  process: process(P.M[P];P.E[P]),  apply: f a,  so_apply: x[s],  lambda: x.A[x],  universe: Type,  uimplies: b supposing a,  prop: ,  equal: s = t,  so_lambda: x.t[x],  strong-type-continuous: Continuous+(T.F[T]),  all: x:A. B[x],  function: x:A  B[x],  uall: [x:A]. B[x],  isect: x:A. B[x],  member: t  T,  RepUR: Error :RepUR,  CollapseTHEN: Error :CollapseTHEN,  MaAuto: Error :MaAuto,  CollapseTHENA: Error :CollapseTHENA,  RepeatFor: Error :RepeatFor,  Unfold: Error :Unfold,  Repeat: Error :Repeat
Lemmas :  process_wf,  member_wf,  strong-type-continuous_wf,  subtype_rel_wf,  rec-dataflow_wf2

---

\mforall{}[S,M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}[s0:S[process(P.M[P];P.E[P])]].  \mforall{}[next:\mcap{}T:\{T:Type|  process(P.M[P];P.E[P])  \msubseteq{}r  T\} 
                                                                                          (S[M[T]  {}\mrightarrow{}  (T  \mtimes{}  E[T])]  {}\mrightarrow{}  M[T]  {}\mrightarrow{}  (S[T]  \mtimes{}  E[T]))].
          (RecProcess(s0;s,m.next[s;m])  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(T.E[T])  and 
          Continuous+(T.M[T])  and 
          Continuous+(T.S[T]))


Date html generated: 2011_08_16-AM-09_53_43
Last ObjectModification: 2011_06_18-AM-08_35_55

Home Index