---

Step * of 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])
      S |= eo.B[eo] ∈ ℙ) 
  supposing Continuous+(P.M[P])
BY
{ ProveWfLemma }

---

Latex:

---

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])


By

---

Latex:
ProveWfLemma

---

Home Index