---

Step * of Lemma stdEO-le

∀[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 ≤loc e2  ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) ≤ run-event-step(e2))) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `stdEO-locl` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN (InstLemma `stdEO-eq-E` [⌈M⌉;⌈S0⌉;⌈n2m⌉;⌈l2m⌉;⌈env⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
   THEN Unfold `es-le` 0) }

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@i
8. e2 : E@i
9. (e1 <loc e2) ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2)
10. e1 = e2 ∈ E ⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) = run-event-step(e2) ∈ ℤ)
⊢ (e1 <loc e2) ∨ (e1 = e2 ∈ E)
⇐⇒ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ (run-event-step(e1) ≤ run-event-step(e2))

---

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  \mleq{}loc  e2 
        \mLeftarrow{}{}\mRightarrow{}  (run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e2))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `stdEO-locl`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  (InstLemma  `stdEO-eq-E`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}S0\mkleeneclose{};\mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `es-le`  0)

---

Home Index