---

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


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
⊢ run-event-state-when(pRun(S;env;n2m;l2m);<t + (n - 1), x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + n, x>)
BY
{ Assert ⌈∀[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))⌉⋅ }

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

2
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
14. ∀[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))
⊢ run-event-state-when(pRun(S;env;n2m;l2m);<t + (n - 1), x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + n, x>)

---

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.  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{}  run-event-state-when(pRun(S;env;n2m;l2m);<t  +  (n  -  1),  x>)  \msubseteq{}  run-event-state-when(pRun(S;env;n2m;l\000C2m);<t  +  n,  x>)


By

---

Latex:
Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}

---

Home Index