---

Step * of Lemma system-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
{ (RepUR ``system-realizes let`` 0
   THEN (UnivCD THENA Auto)
   THEN DVar `S'
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN (Assert pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN Auto
   THEN (BLemma `run-initialization-property` THEN Auto THEN BLemma `std-initial-property` THEN Auto)⋅) }

---

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:
(RepUR  ``system-realizes  let``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  DVar  `S'
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  (Assert  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  Auto
  THEN  (BLemma  `run-initialization-property`  THEN  Auto  THEN  BLemma  `std-initial-property`  THEN  Auto)
  \mcdot{})

---

Home Index