---

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


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 : runEvents(pRun(<S1, S2>;env;n2m;l2m))
⊢ 0 < run-event-step(e)
BY
{ (D -1
   THEN RecUnfold `pRun` (-1)
   THEN RepUR ``is-run-event`` -1
   THEN Unfold `run-event-step` 0
   THEN SplitOnHypITE -1 
   THEN Auto
   THEN Auto') }

1
.....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)

---

Latex:

---

Latex:

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  :  runEvents(pRun(<S1,  S2>env;n2m;l2m))
\mvdash{}  0  <  run-event-step(e)


By

---

Latex:
(D  -1
  THEN  RecUnfold  `pRun`  (-1)
  THEN  RepUR  ``is-run-event``  -1
  THEN  Unfold  `run-event-step`  0
  THEN  SplitOnHypITE  -1 
  THEN  Auto
  THEN  Auto')

---

Home Index