---

Step * 1 1 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))
9. x1 : ℕ@i
10. x2 : Id@i
11. ↑is-run-event(pRun(S2;env;n2m;l2m);x1;x2)@i
⊢ 0 < x1
BY
{ (InstLemma `run-event-step-positive` [⌈M⌉;⌈S2⌉;⌈n2m⌉;⌈l2m⌉;⌈env⌉;⌈<x1, x2>⌉]⋅ THENA Auto) }

1
.....wf..... 
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. x1 : ℕ@i
10. x2 : Id@i
11. ↑is-run-event(pRun(S2;env;n2m;l2m);x1;x2)@i
⊢ <x1, x2> ∈ runEvents(pRun(S2;env;n2m;l2m))

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. x1 : ℕ@i
10. x2 : Id@i
11. ↑is-run-event(pRun(S2;env;n2m;l2m);x1;x2)@i
12. 0 < run-event-step(<x1, x2>)
⊢ 0 < x1

---

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
9.  x1  :  \mBbbN{}@i
10.  x2  :  Id@i
11.  \muparrow{}is-run-event(pRun(S2;env;n2m;l2m);x1;x2)@i
\mvdash{}  0  <  x1


By

---

Latex:
(InstLemma  `run-event-step-positive`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}S2\mkleeneclose{};\mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}<x1,  x2>\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index