---

Step * of Lemma stdEO-event-history

∀[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) ⇐⇒ (e1 ∈ run-event-history(pRun(S0;env;n2m;l2m);e2))) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `stdEO-locl` [] THEN RepeatFor 8 ((ParallelLast' THENA Auto)) THEN RWO "-1" 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)
⊢ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2)
⇐⇒ (e1 ∈ run-event-history(pRun(S0;env;n2m;l2m);e2))

2
.....wf..... 
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. -any : (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2) ∈ Type
⊢ (e1 <loc e2) ∈ Type

3
.....wf..... 
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. (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2)
⇐⇒ (e1 ∈ run-event-history(pRun(S0;env;n2m;l2m);e2))
⊢ (run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2)
  ⇐⇒ (e1 ∈ run-event-history(pRun(S0;env;n2m;l2m);e2)) ∈ Type

---

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{}  (e1  \mmember{}  run-event-history(pRun(S0;env;n2m;l2m);e2))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `stdEO-locl`  []  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))  THEN  RWO  "-1"  0\mcdot{})

---

Home Index