---

Step * 1 2 2 1 of Lemma adjacent-run-states

.....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. S : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. x : Id@i
8. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
9. n : ℤ@i
10. \\%3 : 0 < n@i
11. ∀t:ℕ+
      ((∀a:runEvents(pRun(S;env;n2m;l2m))
          ((run-event-loc(a) = x ∈ Id) ⇒ (¬((t ≤ run-event-step(a)) ∧ run-event-step(a) < t + (n - 1)))))
      ⇒ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + (n - 1), x>))@\000Ci
12. t : ℕ+@i
13. ∀a:runEvents(pRun(S;env;n2m;l2m))
      ((run-event-loc(a) = x ∈ Id) ⇒ (¬((t ≤ run-event-step(a)) ∧ run-event-step(a) < t + n)))@i
⊢ ∀[M:Type ─→ Type]
    ∀x:Id. ∀v3:component(P.M[P]) List. ∀v11:Id. ∀k:ℕ. ∀ms:pMsg(P.M[P]). ∀G:LabeledDAG(pInTransit(P.M[P])).
      (Continuous+(P.M[P])
      ⇒ (¬↑x = v11)
      ⇒ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = deliver-msg(k;ms;v11;v3;G) 
                                                   in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))
BY
{ (All Thin THEN Auto) }

1
1. [M] : Type ─→ Type
2. x : Id@i
3. v3 : component(P.M[P]) List@i
4. v11 : Id@i
5. k : ℕ@i
6. ms : pMsg(P.M[P])@i
7. G : LabeledDAG(pInTransit(P.M[P]))@i
8. Continuous+(P.M[P])@i'
9. ¬↑x = v11@i
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = deliver-msg(k;ms;v11;v3;G) 
                                            in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)

---

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.  S  :  System(P.M[P])@i
6.  env  :  pEnvType(P.M[P])@i
7.  x  :  Id@i
8.  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
9.  n  :  \mBbbZ{}@i
10.  \mbackslash{}\mbackslash{}\%3  :  0  <  n@i
11.  \mforall{}t:\mBbbN{}\msupplus{}
            ((\mforall{}a:runEvents(pRun(S;env;n2m;l2m))
                    ((run-event-loc(a)  =  x)
                    {}\mRightarrow{}  (\mneg{}((t  \mleq{}  run-event-step(a))  \mwedge{}  run-event-step(a)  <  t  +  (n  -  1)))))
            {}\mRightarrow{}  run-event-state-when(pRun(S;env;n2m;l2m);<t,  x>)  \msubseteq{}  run-event-state-when(pRun(S;env;n2m;l2m)\000C;<t  +  (n  -  1),  x>))@i
12.  t  :  \mBbbN{}\msupplus{}@i
13.  \mforall{}a:runEvents(pRun(S;env;n2m;l2m))
            ((run-event-loc(a)  =  x)  {}\mRightarrow{}  (\mneg{}((t  \mleq{}  run-event-step(a))  \mwedge{}  run-event-step(a)  <  t  +  n)))@i
\mvdash{}  \mforall{}[M:Type  {}\mrightarrow{}  Type]
        \mforall{}x:Id.  \mforall{}v3:component(P.M[P])  List.  \mforall{}v11:Id.  \mforall{}k:\mBbbN{}.  \mforall{}ms:pMsg(P.M[P]).
        \mforall{}G:LabeledDAG(pInTransit(P.M[P])).
            (Continuous+(P.M[P])
            {}\mRightarrow{}  (\mneg{}\muparrow{}x  =  v11)
            {}\mRightarrow{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v3)  \msubseteq{}  let  Cs,G  =  deliver-msg(k;ms;v11;v3;G) 
                                                                                                      in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs))


By

---

Latex:
(All  Thin  THEN  Auto)

---

Home Index