---

Step * of Lemma run-initialization-property

∀[M:Type ⟶ Type]
  ∀[n2m:ℕ ⟶ pMsg(P.M[P])]. ∀[l2m:Id ⟶ pMsg(P.M[P])]. ∀[S0:System(P.M[P])]. ∀[env:pEnvType(P.M[P])].
    ∀[e:runEvents(pRun(S0;env;n2m;l2m))]. fst(fst(run-info(pRun(S0;env;n2m;l2m);e))) < run-event-step(e) 
    supposing run-initialization(pRun(S0;env;n2m;l2m);snd(S0)) 
  supposing Continuous+(P.M[P])
BY
{ (BasicUniformUnivCD Auto
   THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN Auto
   THEN Try ((DVar `S0' THEN Reduce 0 THEN Complete (Auto))⋅)
   THEN (InstLemma `pRun-invariant1` [⌜M⌝;⌜n2m⌝;⌜l2m⌝;⌜S0⌝;⌜env⌝]⋅ THENA Auto)
   THEN RepUR ``let`` -1
   THEN (InstHyp [⌜e⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN (Assert S0 ∈ System(P.M[P]) BY
               Trivial)
   THEN DVar `S0'
   THEN All Reduce) }

1
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ⟶ pMsg(P.M[P])
4. l2m : Id ⟶ pMsg(P.M[P])
5. S1 : component(P.M[P]) List
6. S2 : LabeledDAG(pInTransit(P.M[P]))
7. env : pEnvType(P.M[P])
8. pRun(<S1, S2>;env;n2m;l2m) ∈ pRunType(P.M[P])
9. run-initialization(pRun(<S1, S2>;env;n2m;l2m);S2)
10. e : runEvents(pRun(<S1, S2>;env;n2m;l2m))
11. fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) < run-event-step(e) ∨ (∃m:ℕlg-size(S2). ((fst(run-info(pRun(<S1, S2\000C>;env;n2m;l2m);e))) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))
12. <S1, S2> ∈ System(P.M[P])
⊢ fst(fst(run-info(pRun(<S1, S2>;env;n2m;l2m);e))) < run-event-step(e)

---

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])].
        \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))]
            fst(fst(run-info(pRun(S0;env;n2m;l2m);e)))  <  run-event-step(e) 
        supposing  run-initialization(pRun(S0;env;n2m;l2m);snd(S0)) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (Assert  pRun(S0;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  Auto
  THEN  Try  ((DVar  `S0'  THEN  Reduce  0  THEN  Complete  (Auto))\mcdot{})
  THEN  (InstLemma  `pRun-invariant1`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}S0\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``let``  -1
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  (Assert  S0  \mmember{}  System(P.M[P])  BY
                          Trivial)
  THEN  DVar  `S0'
  THEN  All  Reduce)

---

Home Index