---

Step * 1 1 1 2 1 of Lemma stdEO-locl


1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. S0 : InitialSystem(P.M[P])@i
4. n2m : ℕ ⟶ pMsg(P.M[P])@i
5. l2m : Id ⟶ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. e1 : {e:runEvents(pRun(S0;env;n2m;l2m))| True} @i
8. e2 : {e:runEvents(pRun(S0;env;n2m;l2m))| True} @i
9. run-event-step(e1) < run-event-step(e2) supposing ↓e1 run-lt(pRun(S0;env;n2m;l2m)) e2
10. run-event-loc(e1) ∈ Id
11. run-event-loc(e2) ∈ Id
12. run-event-step(e1) ∈ ℕ
13. run-event-step(e2) ∈ ℕ
14. run-lt(pRun(S0;env;n2m;l2m)) ∈ runEvents(pRun(S0;env;n2m;l2m)) ⟶ runEvents(pRun(S0;env;n2m;l2m)) ⟶ ℙ
15. runEvents(pRun(S0;env;n2m;l2m)) ∈ Type
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. run-event-step(e1) < run-event-step(e2)@i
⊢ run-info(pRun(S0;env;n2m;l2m);e2) ∈ ℤ × Id × Top
BY
{ UsingVars [`M'] Auto }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  S0  :  InitialSystem(P.M[P])@i
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
6.  env  :  pEnvType(P.M[P])@i
7.  e1  :  \{e:runEvents(pRun(S0;env;n2m;l2m))|  True\}  @i
8.  e2  :  \{e:runEvents(pRun(S0;env;n2m;l2m))|  True\}  @i
9.  run-event-step(e1)  <  run-event-step(e2)  supposing  \mdownarrow{}e1  run-lt(pRun(S0;env;n2m;l2m))  e2
10.  run-event-loc(e1)  \mmember{}  Id
11.  run-event-loc(e2)  \mmember{}  Id
12.  run-event-step(e1)  \mmember{}  \mBbbN{}
13.  run-event-step(e2)  \mmember{}  \mBbbN{}
14.  run-lt(pRun(S0;env;n2m;l2m))  \mmember{}  runEvents(pRun(S0;env;n2m;l2m))
        {}\mrightarrow{}  runEvents(pRun(S0;env;n2m;l2m))
        {}\mrightarrow{}  \mBbbP{}
15.  runEvents(pRun(S0;env;n2m;l2m))  \mmember{}  Type
16.  run-event-loc(e1)  =  run-event-loc(e2)@i
17.  run-event-step(e1)  <  run-event-step(e2)@i
\mvdash{}  run-info(pRun(S0;env;n2m;l2m);e2)  \mmember{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Top


By

---

Latex:
UsingVars  [`M']  Auto

---

Home Index