---

Step * 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:ℕ. ∀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))))
     ⇒ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + n, x>))
⊢ ∀n,m:ℕ+.
    (run-event-state-when(pRun(S;env;n2m;l2m);<n, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<m, x>)) supposing 
       ((∀a:runEvents(pRun(S;env;n2m;l2m))
           ¬((n ≤ run-event-step(a)) ∧ run-event-step(a) < m) supposing run-event-loc(a) = x ∈ Id) and 
       (n ≤ m))
BY
{ (Auto THEN Subst' m ~ n + (m - n) 0 THEN Try (BackThruSomeHyp) THEN DVar `n' THEN DVar `m' THEN Auto')⋅ }

---

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.  \mforall{}n:\mBbbN{}.  \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))))
          {}\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,  x>))
\mvdash{}  \mforall{}n,m:\mBbbN{}\msupplus{}.
        (run-event-state-when(pRun(S;env;n2m;l2m);<n,  x>)  \msubseteq{}  run-event-state-when(pRun(S;env;n2m;l2m);<m,\000C  x>))  supposing 
              ((\mforall{}a:runEvents(pRun(S;env;n2m;l2m))
                      \mneg{}((n  \mleq{}  run-event-step(a))  \mwedge{}  run-event-step(a)  <  m)  supposing  run-event-loc(a)  =  x)  and 
              (n  \mleq{}  m))


By

---

Latex:
(Auto
  THEN  Subst'  m  \msim{}  n  +  (m  -  n)  0
  THEN  Try  (BackThruSomeHyp)
  THEN  DVar  `n'
  THEN  DVar  `m'
  THEN  Auto')\mcdot{}

---

Home Index