---

Step * 1 of Lemma stdEO-eq-E


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} 
BY
{ All (RepUR ``runEvents run-event-loc run-event-step``) }

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:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} | True} @i
8. e2 : {e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} | True} @i
9. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (snd(e) ∈ Id)
10. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (snd(e) ∈ Id)
11. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (fst(e) ∈ ℕ)
12. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (fst(e) ∈ ℕ)
13. {tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))}  ∈ Type
14. (snd(e1)) = (snd(e2)) ∈ Id@i
15. (fst(e1)) = (fst(e2)) ∈ ℤ@i
⊢ e1 = e2 ∈ {e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} | True} 

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  S0  :  InitialSystem(P.M[P])@i
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  l2m  :  Id  {}\mrightarrow{}  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.  \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].  (run-event-loc(e)  \mmember{}  Id)
10.  \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].  (run-event-loc(e)  \mmember{}  Id)
11.  \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].  (run-event-step(e)  \mmember{}  \mBbbN{})
12.  \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].  (run-event-step(e)  \mmember{}  \mBbbN{})
13.  runEvents(pRun(S0;env;n2m;l2m))  \mmember{}  Type
14.  run-event-loc(e1)  =  run-event-loc(e2)@i
15.  run-event-step(e1)  =  run-event-step(e2)@i
\mvdash{}  e1  =  e2


By

---

Latex:
All  (RepUR  ``runEvents  run-event-loc  run-event-step``)

---

Home Index