---

Step * of Lemma stdEO-E-property

∀[M:Type ─→ Type]
  ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S2:InitialSystem(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e:E.
    (e ∈ ℕ+ × Id) 
  supposing Continuous+(P.M[P])
BY
{ Auto }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. S2 : InitialSystem(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. e : E@i
⊢ e ∈ ℕ+ × Id

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S2:InitialSystem(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
    \mforall{}e:E.
        (e  \mmember{}  \mBbbN{}\msupplus{}  \mtimes{}  Id) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
Auto

---

Home Index