---

Step * 1 1 1 1 of Lemma pRun-invariant1

.....assertion..... 
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 : {1...}
11. x : Id@i
12. v1 : ℕ@i
13. v3 : ℕ@i
14. v4 : Id@i
15. (env t pRun(<S1, S2>;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
16. v5 : component(P.M[P]) List@i
17. v6 : LabeledDAG(pInTransit(P.M[P]))@i
18. (snd((pRun(<S1, S2>;env;n2m;l2m) (t - 1)))) = <v5, v6> ∈ System(P.M[P])@i
19. ↑null(lg-in-edges(v6;v1))
20. v1 < lg-size(v6)
21. v7 : ℤ × Id@i
22. v9 : Id@i
23. v10 : pCom(P.M[P])@i
24. lg-label(v6;v1) = <v7, v9, v10> ∈ pInTransit(P.M[P])@i
⊢ (↑x = v9) ⇒ (fst(v7) < t ∨ (∃m:ℕlg-size(S2). (v7 = (fst(lg-label(S2;m))) ∈ (ℤ × Id))))
BY
{ (DVar `S2' THEN (InstHyp [⌈t - 1⌉] 9⋅ THENA Auto)) }

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 : LabeledGraph(pInTransit(P.M[P]))@i
7. \\%30 : is-dag(S2)@i
8. env : pEnvType(P.M[P])@i
9. ∀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)))
10. <S1, S2> ∈ System(P.M[P])
11. t : {1...}
12. x : Id@i
13. v1 : ℕ@i
14. v3 : ℕ@i
15. v4 : Id@i
16. (env t pRun(<S1, S2>;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
17. v5 : component(P.M[P]) List@i
18. v6 : LabeledDAG(pInTransit(P.M[P]))@i
19. (snd((pRun(<S1, S2>;env;n2m;l2m) (t - 1)))) = <v5, v6> ∈ System(P.M[P])@i
20. ↑null(lg-in-edges(v6;v1))
21. v1 < lg-size(v6)
22. v7 : ℤ × Id@i
23. v9 : Id@i
24. v10 : pCom(P.M[P])@i
25. lg-label(v6;v1) = <v7, v9, v10> ∈ pInTransit(P.M[P])@i
26. let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) (t - 1) in 
∀x∈G.((fst(fst(x))) ≤ (t - 1)) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
⊢ (↑x = v9) ⇒ (fst(v7) < t ∨ (∃m:ℕlg-size(S2). (v7 = (fst(lg-label(S2;m))) ∈ (ℤ × Id))))

---

Latex:

---

Latex:
.....assertion..... 
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.  t  :  \{1...\}
11.  x  :  Id@i
12.  v1  :  \mBbbN{}@i
13.  v3  :  \mBbbN{}@i
14.  v4  :  Id@i
15.  (env  t  pRun(<S1,  S2>env;n2m;l2m))  =  <v1,  v3,  v4>@i
16.  v5  :  component(P.M[P])  List@i
17.  v6  :  LabeledDAG(pInTransit(P.M[P]))@i
18.  (snd((pRun(<S1,  S2>env;n2m;l2m)  (t  -  1))))  =  <v5,  v6>@i
19.  \muparrow{}null(lg-in-edges(v6;v1))
20.  v1  <  lg-size(v6)
21.  v7  :  \mBbbZ{}  \mtimes{}  Id@i
22.  v9  :  Id@i
23.  v10  :  pCom(P.M[P])@i
24.  lg-label(v6;v1)  =  <v7,  v9,  v10>@i
\mvdash{}  (\muparrow{}x  =  v9)  {}\mRightarrow{}  (fst(v7)  <  t  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  (v7  =  (fst(lg-label(S2;m))))))


By

---

Latex:
(DVar  `S2'  THEN  (InstHyp  [\mkleeneopen{}t  -  1\mkleeneclose{}]  9\mcdot{}  THENA  Auto))

---

Home Index