---

Step * 1 1 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. 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>)
BY
{ ((Subst' t + 0 ~ t 0 THEN Auto) THEN BLemma `l_contains_weakening` 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.  t  :  \mBbbN{}\msupplus{}@i
10.  \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  +  0)))@i
\mvdash{}  run-event-state-when(pRun(S;env;n2m;l2m);<t,  x>)  \msubseteq{}  run-event-state-when(pRun(S;env;n2m;l2m);<t  +  0\000C,  x>)


By

---

Latex:
((Subst'  t  +  0  \msim{}  t  0  THEN  Auto)  THEN  BLemma  `l\_contains\_weakening`  THEN  Auto)

---

Home Index