Step
*
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 : {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}
BY
{ (RepeatFor 2 (DSetVars) THEN RepeatFor 2 ((MemTypeCD 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 : ℕ × 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)
2
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
20. tx : ℕ × Id
⊢ is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx)) ∈ 𝔹
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:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} | True\} @i
8. e2 : \{e:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} | True\} @i
9. \mforall{}[e:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} ]. (snd(e) \mmember{} Id)
10. \mforall{}[e:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} ]. (snd(e) \mmember{} Id)
11. \mforall{}[e:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} ]. (fst(e) \mmember{} \mBbbN{})
12. \mforall{}[e:\{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} ]. (fst(e) \mmember{} \mBbbN{})
13. \{tx:\mBbbN{} \mtimes{} Id| \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);fst(tx);snd(tx))\} \mmember{} Type
14. (snd(e1)) = (snd(e2))@i
15. (fst(e1)) = (fst(e2))@i
\mvdash{} e1 = e2
By
Latex:
(RepeatFor 2 (DSetVars) THEN RepeatFor 2 ((MemTypeCD THENA Auto)))
Home
Index