---

{ [M,E:Type  Type].
    (process(P.M[P];P.E[P]) r (M[process(P.M[P];P.E[P])]
        (process(P.M[P];P.E[P])  E[process(P.M[P];P.E[P])]))) supposing 
       (Continuous+(P.E[P]) and 
       Continuous+(P.M[P])) }

{ Proof }

---

Definitions occuring in Statement :  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[s],  function: x:A  B[x],  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  process: process(P.M[P];P.E[P]),  member: t  T,  so_lambda: x.t[x],  type-continuous: Continuous(T.F[T]),  strong-type-continuous: Continuous+(T.F[T]),  ext-eq: A  B,  and: P  Q,  prop:
Lemmas :  corec-subtype,  strong-type-continuous_wf,  continuous-function,  strong-continuous-product,  continuous-id,  nat_wf

---

\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (process(P.M[P];P.E[P])  \msubseteq{}r  (M[process(P.M[P];P.E[P])]
          {}\mrightarrow{}  (process(P.M[P];P.E[P])  \mtimes{}  E[process(P.M[P];P.E[P])])))  supposing 
          (Continuous+(P.E[P])  and 
          Continuous+(P.M[P]))


Date html generated: 2011_08_16-AM-09_53_14
Last ObjectModification: 2011_06_18-AM-08_35_41

Home Index