---

Step * 1 1 1 1 1 of Lemma run-initialization-property

.....truecase..... 
1. M : Type ─→ Type
2. n2m : ℕ ─→ pMsg(P.M[P])
3. l2m : Id ─→ pMsg(P.M[P])
4. S1 : component(P.M[P]) List
5. S2 : LabeledDAG(pInTransit(P.M[P]))
6. env : pEnvType(P.M[P])
7. e : ℕ × Id
8. ↑let info,S = <inr ⋅ , S1, S2> 
    in isl(info) ∧b let ev,z,m = outl(info) in snd(e) = z
9. (fst(e)) = 0 ∈ ℤ
⊢ 0 < fst(e)
BY
{ (Reduce (-2) THEN Auto) }

---

Latex:

---

Latex:
.....truecase..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])
3.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])
4.  S1  :  component(P.M[P])  List
5.  S2  :  LabeledDAG(pInTransit(P.M[P]))
6.  env  :  pEnvType(P.M[P])
7.  e  :  \mBbbN{}  \mtimes{}  Id
8.  \muparrow{}let  info,S  =  <inr  \mcdot{}  ,  S1,  S2> 
        in  isl(info)  \mwedge{}\msubb{}  let  ev,z,m  =  outl(info)  in  snd(e)  =  z
9.  (fst(e))  =  0
\mvdash{}  0  <  fst(e)


By

---

Latex:
(Reduce  (-2)  THEN  Auto)

---

Home Index