---

Step * of Lemma stdEO-locl

∀[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
{ (RepeatFor 8 (Intro) THEN (InstLemma `stdEO-causal` [⌜M⌝;⌜S0⌝;⌜n2m⌝;⌜l2m⌝;⌜env⌝;⌜e1⌝]⋅ THENA 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@i
8. e2 : E@i
9. ∀[e2:E]. run-event-step(e1) < run-event-step(e2) supposing (e1 < e2)
⊢ (e1 <loc e2) ⇐⇒ (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  <loc  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  (InstLemma  `stdEO-causal`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}S0\mkleeneclose{};\mkleeneopen{}n2m\mkleeneclose{};\mkleeneopen{}l2m\mkleeneclose{};\mkleeneopen{}env\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index