---

Step * of Lemma stdEO_wf

∀[M:Type ⟶ Type]
  ∀[S0:InitialSystem(P.M[P])]. ∀[n2m:ℕ ⟶ pMsg(P.M[P])]. ∀[l2m:Id ⟶ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])].
    (stdEO(n2m;l2m;env;S0) ∈ EO+(pMsg(P.M[P]))) 
  supposing Continuous+(P.M[P])
BY
{ (ProveWfLemma
   THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN BLemma `std-initial-property`
   THEN Auto)⋅ }

1
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. S0 : InitialSystem(P.M[P])
4. n2m : ℕ ⟶ pMsg(P.M[P])
5. l2m : Id ⟶ pMsg(P.M[P])
6. env : pEnvType(P.M[P])
7. pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
⊢ std-initial(S0)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[S0:InitialSystem(P.M[P])].  \mforall{}[n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[l2m:Id  {}\mrightarrow{}  pMsg(P.M[P])].
    \mforall{}[env:pEnvType(P.M[P])].
        (stdEO(n2m;l2m;env;S0)  \mmember{}  EO+(pMsg(P.M[P]))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(ProveWfLemma
  THEN  (Assert  pRun(S0;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  BLemma  `std-initial-property`
  THEN  Auto)\mcdot{}

---

Home Index