---

Step * of Lemma pRun-invariant1

∀[M:Type ⟶ Type]
  ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
    let r = pRun(S0;env;n2m;l2m) in
        ∀e:runEvents(r)
          (fst(fst(run-info(r;e))) < run-event-step(e)
          ∨ (∃m:ℕlg-size(snd(S0)). ((fst(run-info(r;e))) = (fst(lg-label(snd(S0);m))) ∈ (ℤ × Id)))) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `pRun-intransit-invariant` []⋅
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (InstHyp [⌜S1⌝;⌜S2⌝] (-3)⋅ THENA Auto)
   THEN Thin (-4)
   THEN ParallelLast'
   THEN All (RepUR ``let``)
   THEN (Assert <S1, S2> ∈ System(P.M[P]) BY
               (Unfold `System` 0 THEN Auto))
   THEN (Assert pRun(<S1, S2>;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               Auto)
   THEN Auto
   THEN (D -1
         THEN (Decide ↑is-run-event(pRun(<S1, S2>;env;n2m;l2m);fst(e);snd(e)) THENA Auto)
         THEN Try ((D -1 THEN Unhide THEN Auto))
         THEN Thin (-2)
         THEN D -2
         THEN All Reduce
         THEN RenameVar `t' (-3)
         THEN RenameVar `x' (-2)
         THEN RepUR ``run-event-step`` 0)⋅) }

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. 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)))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S0:System(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
        let  r  =  pRun(S0;env;n2m;l2m)  in
                \mforall{}e:runEvents(r)
                    (fst(fst(run-info(r;e)))  <  run-event-step(e)
                    \mvee{}  (\mexists{}m:\mBbbN{}lg-size(snd(S0)).  ((fst(run-info(r;e)))  =  (fst(lg-label(snd(S0);m)))))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `pRun-intransit-invariant`  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}S1\mkleeneclose{};\mkleeneopen{}S2\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Thin  (-4)
  THEN  ParallelLast'
  THEN  All  (RepUR  ``let``)
  THEN  (Assert  <S1,  S2>  \mmember{}  System(P.M[P])  BY
                          (Unfold  `System`  0  THEN  Auto))
  THEN  (Assert  pRun(<S1,  S2>env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          Auto)
  THEN  Auto
  THEN  (D  -1
              THEN  (Decide  \muparrow{}is-run-event(pRun(<S1,  S2>env;n2m;l2m);fst(e);snd(e))  THENA  Auto)
              THEN  Try  ((D  -1  THEN  Unhide  THEN  Auto))
              THEN  Thin  (-2)
              THEN  D  -2
              THEN  All  Reduce
              THEN  RenameVar  `t'  (-3)
              THEN  RenameVar  `x'  (-2)
              THEN  RepUR  ``run-event-step``  0)\mcdot{})

---

Home Index