---

Step * of Lemma stdEO-eq-E

∀[M:Type ⟶ Type]
  ∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ⟶ pMsg(P.M[P]). ∀l2m:Id ⟶ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]). ∀e1,e2:E.
    (e1 = e2 ∈ E ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) = run-event-step(e2) ∈ ℤ)) 
  supposing Continuous+(P.M[P])
BY
{ (RepeatFor 8 (Intro)
   THEN RepUR ``es-E stdEO runEO run-eo mk-extended-eo mk-eo mk-eo-record`` -2
   THEN RepUR ``es-E stdEO runEO run-eo mk-extended-eo mk-eo mk-eo-record`` -1
   THEN (InstLemma `run-event-loc_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-loc_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-step_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN (InstLemma `run-event-step_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN (InstLemma `runEvents_wf` [⌜M⌝;⌜pRun(S0;env;n2m;l2m)⌝]⋅ THENA Auto)
   THEN RepUR ``es-E stdEO runEO run-eo mk-extended-eo mk-eo mk-eo-record`` 0
   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. ∀[e:runEvents(pRun(S0;env;n2m;l2m))]. (run-event-loc(e) ∈ Id)
10. ∀[e:runEvents(pRun(S0;env;n2m;l2m))]. (run-event-loc(e) ∈ Id)
11. ∀[e:runEvents(pRun(S0;env;n2m;l2m))]. (run-event-step(e) ∈ ℕ)
12. ∀[e:runEvents(pRun(S0;env;n2m;l2m))]. (run-event-step(e) ∈ ℕ)
13. runEvents(pRun(S0;env;n2m;l2m)) ∈ Type
14. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
15. run-event-step(e1) = run-event-step(e2) ∈ ℤ@i
⊢ e1 = e2 ∈ {e:runEvents(pRun(S0;env;n2m;l2m))| True} 

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S0:InitialSystem(P.M[P]).  \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
    \mforall{}e1,e2:E.
        (e1  =  e2
        \mLeftarrow{}{}\mRightarrow{}  (run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  (run-event-step(e1)  =  run-event-step(e2))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(RepeatFor  8  (Intro)
  THEN  RepUR  ``es-E  stdEO  runEO  run-eo  mk-extended-eo  mk-eo  mk-eo-record``  -2
  THEN  RepUR  ``es-E  stdEO  runEO  run-eo  mk-extended-eo  mk-eo  mk-eo-record``  -1
  THEN  (InstLemma  `run-event-loc\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-loc\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-step\_wf`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}pRun(S0;env;n2m;l2m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `run-event-step\_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{}  THENA  Auto)
  THEN  RepUR  ``es-E  stdEO  runEO  run-eo  mk-extended-eo  mk-eo  mk-eo-record``  0
  THEN  Auto)

---

Home Index