---

Step * 1 of Lemma run-initialization-property


1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])
4. l2m : Id ─→ pMsg(P.M[P])
5. S1 : component(P.M[P]) List
6. S2 : LabeledDAG(pInTransit(P.M[P]))
7. env : pEnvType(P.M[P])
8. pRun(<S1, S2>;env;n2m;l2m) ∈ pRunType(P.M[P])
9. run-initialization(pRun(<S1, S2>;env;n2m;l2m);S2)
10. e : runEvents(pRun(<S1, S2>;env;n2m;l2m))
11. fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) < run-event-step(e) ∨ (∃m:ℕlg-size(S2). ((fst(run-info(pRun(<S1, S2\000C>;env;n2m;l2m);e))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
12. <S1, S2> ∈ System(P.M[P])
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) < run-event-step(e)
BY
{ (RepeatFor 2 ((D -2 THEN Auto)⋅) THEN ((With ⌈m⌉ (D (-5))⋅ THENA Auto) THEN InstHyp [⌈e⌉] (-1)⋅ THEN Auto)⋅) }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])
4. l2m : Id ─→ pMsg(P.M[P])
5. S1 : component(P.M[P]) List
6. S2 : LabeledDAG(pInTransit(P.M[P]))
7. env : pEnvType(P.M[P])
8. pRun(<S1, S2>;env;n2m;l2m) ∈ pRunType(P.M[P])
9. e : runEvents(pRun(<S1, S2>;env;n2m;l2m))
10. m : ℕlg-size(S2)
11. (fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)
12. <S1, S2> ∈ System(P.M[P])
13. ∀e:runEvents(pRun(<S1, S2>;env;n2m;l2m)). fst(fst(lg-label(S2;m))) < 1
14. fst(fst(lg-label(S2;m))) < 1
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) < run-event-step(e)

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])
5.  S1  :  component(P.M[P])  List
6.  S2  :  LabeledDAG(pInTransit(P.M[P]))
7.  env  :  pEnvType(P.M[P])
8.  pRun(<S1,  S2>env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
9.  run-initialization(pRun(<S1,  S2>env;n2m;l2m);S2)
10.  e  :  runEvents(pRun(<S1,  S2>env;n2m;l2m))
11.  fst(fst(run-info(pRun(<S1,  S2>env;n2m;l2m);e)))  <  run-event-step(e)
\mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(run-info(pRun(<S1,  S2>env;n2m;l2m);e)))  =  (fst(lg-label(S2;m)))))
12.  <S1,  S2>  \mmember{}  System(P.M[P])
\mvdash{}  fst(fst(run-info(pRun(<S1,  S2>env;n2m;l2m);e)))  <  run-event-step(e)


By

---

Latex:
(RepeatFor  2  ((D  -2  THEN  Auto)\mcdot{})
  THEN  ((With  \mkleeneopen{}m\mkleeneclose{}  (D  (-5))\mcdot{}  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)\mcdot{}
  )

---

Home Index