Nuprl Lemma : recprocess_wf

∀[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]))]. ∀[ext:∩T:Type
                                                                                                        (E[T]
                                                                                                        ─→ M[T]
                                                                                                        ─→ T
                                                                                                        ─→ E[T])].
     (recprocess(s0;s,m.next[s;m];e,m,p.ext[e;m;p]) ∈ 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 :  recprocess: recprocess(s0;s,m.next[s; m];e,m,p.ext[e; m; p]),  process: process(P.M[P];P.E[P]),  strong-type-continuous: Continuous+(T.F[T]),  uimplies: b supposing a,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3],  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
Lemmas :  fix_wf_corec_parameter3,  top_wf,  subtype_rel_wf,  corec_wf,  bool_wf,  process_wf,  strong-type-continuous_wf
\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]))].
      \mforall{}[ext:\mcap{}T:Type.  (E[T]  {}\mrightarrow{}  M[T]  {}\mrightarrow{}  T  {}\mrightarrow{}  E[T])].
          (recprocess(s0;s,m.next[s;m];e,m,p.ext[e;m;p])  \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: 2015_07_17-AM-11_19_59
Last ObjectModification: 2015_01_28-AM-07_36_24

Home Index