---

Step * 1 of Lemma pRun-invariant1


1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
     let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in 
     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
9. <S1, S2> ∈ System(P.M[P])
10. pRun(<S1, S2>;env;n2m;l2m) ∈ pRunType(P.M[P])
11. t : ℕ@i
12. x : Id@i
13. ↑is-run-event(pRun(<S1, S2>;env;n2m;l2m);t;x)
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);<t, x>))) < t ∨ (∃m:ℕlg-size(S2). ((fst(run-info(pRun(<S1, S2>;env;n2m;l2m\000C);<t, x>))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
BY
{ Thin 10⋅ }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
     let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in 
     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
9. <S1, S2> ∈ System(P.M[P])
10. t : ℕ@i
11. x : Id@i
12. ↑is-run-event(pRun(<S1, S2>;env;n2m;l2m);t;x)
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);<t, x>))) < t ∨ (∃m:ℕlg-size(S2). ((fst(run-info(pRun(<S1, S2>;env;n2m;l2m\000C);<t, x>))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  S1  :  component(P.M[P])  List@i
6.  S2  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  env  :  pEnvType(P.M[P])@i
8.  \mforall{}t:\mBbbN{}
          let  info,Cs,G  =  pRun(<S1,  S2>env;n2m;l2m)  t  in 
          \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(x))  =  (fst(lg-label(S2;m)))))
9.  <S1,  S2>  \mmember{}  System(P.M[P])
10.  pRun(<S1,  S2>env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
11.  t  :  \mBbbN{}@i
12.  x  :  Id@i
13.  \muparrow{}is-run-event(pRun(<S1,  S2>env;n2m;l2m);t;x)
\mvdash{}  fst(fst(run-info(pRun(<S1,  S2>env;n2m;l2m);<t,  x>)))  <  t  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(run-info(pRun(\000C<S1,  S2>env;n2m;l2m);<t,  x>)))  =  (fst(lg-label(S2;m)))))


By

---

Latex:
Thin  10\mcdot{}

---

Home Index