---

Step * 1 1 1 of Lemma stdEO-E-property


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
8. e = e ∈ es-base-E(stdEO(n2m;l2m;env;S2))
⊢ runEvents(pRun(S2;env;n2m;l2m)) ⊆r (ℕ+ × Id)
BY
{ (RepUR ``runEvents`` 0 THEN D 0 THEN Auto) }

1
.....subterm..... T:t
1:n
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
8. e = e ∈ es-base-E(stdEO(n2m;l2m;env;S2))
9. x : {tx:ℕ × Id| ↑is-run-event(pRun(S2;env;n2m;l2m);fst(tx);snd(tx))} @i
⊢ x ∈ ℕ+ × Id

2
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
8. e = e ∈ es-base-E(stdEO(n2m;l2m;env;S2))
9. tx : ℕ × Id
⊢ is-run-event(pRun(S2;env;n2m;l2m);fst(tx);snd(tx)) ∈ 𝔹

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  S2  :  InitialSystem(P.M[P])@i
6.  env  :  pEnvType(P.M[P])@i
7.  e  :  E@i
8.  e  =  e
\mvdash{}  runEvents(pRun(S2;env;n2m;l2m))  \msubseteq{}r  (\mBbbN{}\msupplus{}  \mtimes{}  Id)


By

---

Latex:
(RepUR  ``runEvents``  0  THEN  D  0  THEN  Auto)

---

Home Index