---

Step * 1 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. 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)
BY
{ (Assert ⌈0 < run-event-step(e)⌉⋅ THEN Auto') }

1
.....assertion..... 
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
⊢ 0 < run-event-step(e)

2
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
15. 0 < run-event-step(e)
⊢ 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.  e  :  runEvents(pRun(<S1,  S2>env;n2m;l2m))
10.  m  :  \mBbbN{}lg-size(S2)
11.  (fst(run-info(pRun(<S1,  S2>env;n2m;l2m);e)))  =  (fst(lg-label(S2;m)))
12.  <S1,  S2>  \mmember{}  System(P.M[P])
13.  \mforall{}e:runEvents(pRun(<S1,  S2>env;n2m;l2m)).  fst(fst(lg-label(S2;m)))  <  1
14.  fst(fst(lg-label(S2;m)))  <  1
\mvdash{}  fst(fst(run-info(pRun(<S1,  S2>env;n2m;l2m);e)))  <  run-event-step(e)


By

---

Latex:
(Assert  \mkleeneopen{}0  <  run-event-step(e)\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index