---

Step * 3 of Lemma pRun-intransit-invariant


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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
     (((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. ∀env:pEnvType(P.M[P]). ∀t:ℕ.
      let Cs,G = snd((pRun(<Cs0, G0>;env;n2m;l2m) t)) 
      in ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⊢ let info,Cs,G = pRun(<Cs0, G0>;env;n2m;l2m) t in 
∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
BY
{ ((InstHyp [⌈env⌉;⌈t⌉] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddr [1;1;1] THENA (Auto THEN Fold `fulpRunType` 0 THEN Auto THEN Unfold `System` 0 THEN Auto))
   THEN RepeatFor 2 (D -2)
   THEN RepUR ``let`` 0
   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.  Cs0  :  component(P.M[P])  List@i
6.  G0  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  env  :  pEnvType(P.M[P])@i
8.  t  :  \mBbbN{}@i
9.  \mforall{}x:pInTransit(P.M[P]).  \mforall{}t:\mBbbZ{}.
          (((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))  \mmember{}  \mBbbP{})
10.  \mforall{}env:pEnvType(P.M[P]).  \mforall{}t:\mBbbN{}.
            let  Cs,G  =  snd((pRun(<Cs0,  G0>env;n2m;l2m)  t)) 
            in  \mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))
\mvdash{}  let  info,Cs,G  =  pRun(<Cs0,  G0>env;n2m;l2m)  t  in 
\mforall{}x\mmember{}G.((fst(fst(x)))  \mleq{}  t)  \mvee{}  (\mexists{}m:\mBbbN{}lg-size(G0).  ((fst(x))  =  (fst(lg-label(G0;m)))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddr  [1;1;1]
              THENA  (Auto  THEN  Fold  `fulpRunType`  0  THEN  Auto  THEN  Unfold  `System`  0  THEN  Auto)
              )
  THEN  RepeatFor  2  (D  -2)
  THEN  RepUR  ``let``  0
  THEN  Auto)

---

Home Index