---

Step * of Lemma stdEO-causal

∀[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].
    run-event-step(e1) < run-event-step(e2) supposing (e1 < e2) 
  supposing Continuous+(P.M[P])
BY
{ Intros }

1
1. M : Type ⟶ Type
2. Continuous+(P.M[P])
3. S0 : InitialSystem(P.M[P])
4. n2m : ℕ ⟶ pMsg(P.M[P])
5. l2m : Id ⟶ pMsg(P.M[P])
6. env : pEnvType(P.M[P])
7. e1 : E
8. e2 : E
9. (e1 < e2)
⊢ 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].
        run-event-step(e1)  <  run-event-step(e2)  supposing  (e1  <  e2) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
Intros

---

Home Index