---

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


1. ∀[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. [M] : Type ─→ Type
3. Continuous+(P.M[P])
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. S : System(P.M[P])@i
7. env : pEnvType(P.M[P])@i
8. x : Id@i
9. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
10. n : ℤ@i
11. \\%3 : 0 < n@i
12. ∀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
13. t : ℕ+@i
14. ∀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
15. ¬↑is-run-event(pRun(S;env;n2m;l2m);(t + n) - 1;x)
⊢ let info,Cs,G = pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1) in 
  mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ⊆ let info,Cs,G = if ((t + n) - 1 =z 0)
  then <inr ⋅ , S>
  else let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in 
       do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + n) - 1 - 1)));n@0;m;nm)
  fi  in 
  mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
BY
{ (Thin 9⋅
   THEN (Unfold `is-run-event` -1 THEN RecUnfold `pRun` (-1) THEN Reduce (-1))
   THEN MoveToConcl (-1)
   THEN AutoSplit
   THEN Try (Complete (Auto'))
   THEN Subst' (t + n) - 1 - 1 ~ (t + (n - 1)) - 1 0
   THEN Try (Complete (Auto))
   THEN (Assert λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹 BY
               Auto)
   THEN PromoteHyp (-1) 9)⋅ }

1
1. ∀[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. [M] : Type ─→ Type
3. Continuous+(P.M[P])
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. S : System(P.M[P])@i
7. env : pEnvType(P.M[P])@i
8. x : Id@i
9. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
10. n : ℤ@i
11. \\%3 : 0 < n@i
12. ∀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
13. t : ℕ+@i
14. (t + n) - 1 ≠ 0
15. ∀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
⊢ (¬↑let info,S = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in 
     do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1)));n@0;m;nm) 
     in isl(info) ∧b let ev,z,m = outl(info) in x = z)
⇒ let info,Cs,G = pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1) in 
   mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ⊆ let info,Cs,G = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in 
   do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1)));n@0;m;nm) in 
   mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)

---

Latex:

---

Latex:

1.  \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))
2.  [M]  :  Type  {}\mrightarrow{}  Type
3.  Continuous+(P.M[P])
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
6.  S  :  System(P.M[P])@i
7.  env  :  pEnvType(P.M[P])@i
8.  x  :  Id@i
9.  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])
10.  n  :  \mBbbZ{}@i
11.  \mbackslash{}\mbackslash{}\%3  :  0  <  n@i
12.  \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
13.  t  :  \mBbbN{}\msupplus{}@i
14.  \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
15.  \mneg{}\muparrow{}is-run-event(pRun(S;env;n2m;l2m);(t  +  n)  -  1;x)
\mvdash{}  let  info,Cs,G  =  pRun(S;env;n2m;l2m)  ((t  +  (n  -  1))  -  1)  in 
    mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)  \msubseteq{}  let  info,Cs,G  =  if  ((t  +  n)  -  1  =\msubz{}  0)
    then  <inr  \mcdot{}  ,  S>
    else  let  n@0,m,nm  =  env  ((t  +  n)  -  1)  pRun(S;env;n2m;l2m)  in 
              do-chosen-command(n2m;l2m;(t  +  n)  -  1;snd((pRun(S;env;n2m;l2m)  ((t  +  n)  -  1  -  1)));n@0;m;nm)
    fi    in 
    mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)


By

---

Latex:
(Thin  9\mcdot{}
  THEN  (Unfold  `is-run-event`  -1  THEN  RecUnfold  `pRun`  (-1)  THEN  Reduce  (-1))
  THEN  MoveToConcl  (-1)
  THEN  AutoSplit
  THEN  Try  (Complete  (Auto'))
  THEN  Subst'  (t  +  n)  -  1  -  1  \msim{}  (t  +  (n  -  1))  -  1  0
  THEN  Try  (Complete  (Auto))
  THEN  (Assert  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}  BY
                          Auto)
  THEN  PromoteHyp  (-1)  9)\mcdot{}

---

Home Index