---

Step * 1 of Lemma run-event-step-positive

.....truecase..... 
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : System(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])
8. e1 : ℕ
9. e2 : Id
10. ↑let info,S = <inr ⋅ , S0> 
     in isl(info) ∧b let ev,z,m = outl(info) in e2 = z
11. e1 = 0 ∈ ℤ
⊢ 0 < e1
BY
{ (Reduce (-2) THEN Auto)⋅ }

---

Latex:

---

Latex:
.....truecase..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  S0  :  System(P.M[P])
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])
5.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])
6.  env  :  pEnvType(P.M[P])
7.  pRun(S0;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
8.  e1  :  \mBbbN{}
9.  e2  :  Id
10.  \muparrow{}let  info,S  =  <inr  \mcdot{}  ,  S0> 
          in  isl(info)  \mwedge{}\msubb{}  let  ev,z,m  =  outl(info)  in  e2  =  z
11.  e1  =  0
\mvdash{}  0  <  e1


By

---

Latex:
(Reduce  (-2)  THEN  Auto)\mcdot{}

---

Home Index