---

Step * 1 1 1 1 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 : 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))))
BY
{ (MoveToConcl 19
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;1] THENA (Auto THEN Fold `fulpRunType` 0 THEN Auto))
   THEN RepeatFor 3 (D (-2))
   THEN Reduce 0
   THEN Unfold `System` 0
   THEN Auto
   THEN Decide ⌈fst(v7) < t⌉⋅
   THEN Auto
   THEN (With ⌈v1⌉ (D (-4))⋅ THENA Auto)
   THEN (D (-1)
         THEN Auto
         THEN (Subst' (fst(lg-label(v14;v1))) = v7 ∈ (ℤ × Id) -1⋅
               THEN Auto
               THEN SubsumeC ⌈LabeledDAG(pInTransit(P.M[P]))⌉⋅
               THEN Auto)⋅)⋅) }

---

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  :  LabeledGraph(pInTransit(P.M[P]))@i
7.  \mbackslash{}\mbackslash{}\%30  :  is-dag(S2)@i
8.  env  :  pEnvType(P.M[P])@i
9.  \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)))))
10.  <S1,  S2>  \mmember{}  System(P.M[P])
11.  t  :  \{1...\}
12.  x  :  Id@i
13.  v1  :  \mBbbN{}@i
14.  v3  :  \mBbbN{}@i
15.  v4  :  Id@i
16.  (env  t  pRun(<S1,  S2>env;n2m;l2m))  =  <v1,  v3,  v4>@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>@i
20.  \muparrow{}null(lg-in-edges(v6;v1))
21.  v1  <  lg-size(v6)
22.  v7  :  \mBbbZ{}  \mtimes{}  Id@i
23.  v9  :  Id@i
24.  v10  :  pCom(P.M[P])@i
25.  lg-label(v6;v1)  =  <v7,  v9,  v10>@i
26.  let  info,Cs,G  =  pRun(<S1,  S2>env;n2m;l2m)  (t  -  1)  in 
\mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  (t  -  1))  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  ((fst(x))  =  (fst(lg-label(S2;m)))))
\mvdash{}  (\muparrow{}x  =  v9)  {}\mRightarrow{}  (fst(v7)  <  t  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(S2).  (v7  =  (fst(lg-label(S2;m))))))


By

---

Latex:
(MoveToConcl  19
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;1]  THENA  (Auto  THEN  Fold  `fulpRunType`  0  THEN  Auto))
  THEN  RepeatFor  3  (D  (-2))
  THEN  Reduce  0
  THEN  Unfold  `System`  0
  THEN  Auto
  THEN  Decide  \mkleeneopen{}fst(v7)  <  t\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (With  \mkleeneopen{}v1\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  Auto)
  THEN  (D  (-1)
              THEN  Auto
              THEN  (Subst'  (fst(lg-label(v14;v1)))  =  v7  -1\mcdot{}
                          THEN  Auto
                          THEN  SubsumeC  \mkleeneopen{}LabeledDAG(pInTransit(P.M[P]))\mkleeneclose{}\mcdot{}
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index