Nuprl Lemma : system-strongly-realizes_wf

[M:Type ─→ Type]
  ∀[S:InitialSystem(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[A:pEnvType(P.M[P])
                                                                                       ─→ pRunType(P.M[P])
                                                                                       ─→ ℙ].
  ∀[B:EO+(pMsg(P.M[P])) ─→ ℙ].
    (assuming(env,r.A[env;r])
      |= eo.B[eo] ∈ ℙ
  supposing Continuous+(P.M[P])


Proof




Definitions occuring in Statement :  system-strongly-realizes: system-strongly-realizes InitialSystem: InitialSystem(P.M[P]) pEnvType: pEnvType(T.M[T]) pRunType: pRunType(T.M[T]) pMsg: pMsg(P.M[P]) event-ordering+: EO+(Info) Id: Id strong-type-continuous: Continuous+(T.F[T]) nat: uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  all_wf sub-system_wf system-realizes_wf pRunType_wf pEnvType_wf event-ordering+_wf pMsg_wf Id_wf nat_wf InitialSystem_wf strong-type-continuous_wf

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[S:InitialSystem(P.M[P])].  \mforall{}[n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[l2m:Id  {}\mrightarrow{}  pMsg(P.M[P])].
    \mforall{}[A:pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}].
        (assuming(env,r.A[env;r])
            S  |=  eo.B[eo]  \mmember{}  \mBbbP{}) 
    supposing  Continuous+(P.M[P])



Date html generated: 2015_07_23-AM-11_19_55
Last ObjectModification: 2015_01_28-PM-11_17_08

Home Index