---

Step * 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])
⊢ ∀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>))
BY
{ (InductionOnNat THEN Auto) }

1
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. t : ℕ+@i
10. ∀a:runEvents(pRun(S;env;n2m;l2m))
      ((run-event-loc(a) = x ∈ Id) ⇒ (¬((t ≤ run-event-step(a)) ∧ run-event-step(a) < t + 0)))@i
⊢ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + 0, 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 : ℤ@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, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + n, x>)

---

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])
\mvdash{}  \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);<\000Ct  +  n,  x>))


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index