---

Step * 1 1 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 : ℕ × Id@i
8. ↑is-run-event(pRun(S0;env;n2m;l2m);fst(e1);snd(e1))@i
9. True@i
10. e2 : ℕ × Id@i
11. ↑is-run-event(pRun(S0;env;n2m;l2m);fst(e2);snd(e2))@i
12. True@i
13. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (snd(e) ∈ Id)
14. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (snd(e) ∈ Id)
15. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (fst(e) ∈ ℕ)
16. ∀[e:{tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))} ]. (fst(e) ∈ ℕ)
17. {tx:ℕ × Id| ↑is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))}  ∈ Type
18. (snd(e1)) = (snd(e2)) ∈ Id@i
19. (fst(e1)) = (fst(e2)) ∈ ℤ@i
⊢ e1 = e2 ∈ (ℕ × Id)
BY
{ (DVar `e1' THEN DVar `e2' THEN All Reduce THEN Auto) }

---

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  :  \mBbbN{}  \mtimes{}  Id@i
8.  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(e1);snd(e1))@i
9.  True@i
10.  e2  :  \mBbbN{}  \mtimes{}  Id@i
11.  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(e2);snd(e2))@i
12.  True@i
13.  \mforall{}[e:\{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\}  ].  (snd(e)  \mmember{}  Id)
14.  \mforall{}[e:\{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\}  ].  (snd(e)  \mmember{}  Id)
15.  \mforall{}[e:\{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\}  ].  (fst(e)  \mmember{}  \mBbbN{})
16.  \mforall{}[e:\{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\}  ].  (fst(e)  \mmember{}  \mBbbN{})
17.  \{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\}    \mmember{}  Type
18.  (snd(e1))  =  (snd(e2))@i
19.  (fst(e1))  =  (fst(e2))@i
\mvdash{}  e1  =  e2


By

---

Latex:
(DVar  `e1'  THEN  DVar  `e2'  THEN  All  Reduce  THEN  Auto)

---

Home Index