---

Step * 1 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
⊢ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (↓e1 run-lt(pRun(S0;env;n2m;l2m)) e2)
⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2)
BY
{ ((InstLemma `run-event-loc_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝;⌜e1⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-loc_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝;⌜e2⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-step_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝;⌜e1⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-step_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝;⌜e2⌝]⋅ THENA Auto)
   THEN (InstLemma `run-lt_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN InstLemma `runEvents_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅
   THEN Auto) }

1
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
⊢ ↓e1 run-lt(pRun(S0;env;n2m;l2m)) e2

---

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
\mvdash{}  (run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  (\mdownarrow{}e1  run-lt(pRun(S0;env;n2m;l2m))  e2)
\mLeftarrow{}{}\mRightarrow{}  (run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  run-event-step(e1)  <  run-event-step(e2)


By

---

Latex:
((InstLemma  `run-event-loc\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-loc\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-step\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-step\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-lt\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `runEvents\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index