---

Step * of Lemma adjacent-run-states

∀[M:Type ⟶ Type]
  ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀S:System(P.M[P]). ∀env:pEnvType(P.M[P]). ∀x:Id. ∀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)) 
  supposing Continuous+(P.M[P])
BY
{ (RepeatFor 7 ((D 0 THENA Auto))
   THEN (Assert pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN Assert ⌜∀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,\000C x>))⌝⋅) }

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])
⊢ ∀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>))

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:ℕ. ∀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))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S:System(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).  \mforall{}x:Id.
    \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)) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(RepeatFor  7  ((D  0  THENA  Auto))
  THEN  (Assert  pRun(S;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  Assert  \mkleeneopen{}\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;en\000Cv;n2m;l2m);<t  +  n,  x>))\mkleeneclose{}\mcdot{})

---

Home Index