---

Step * 2 2 1 1 of Lemma system-strongly-realizes_functionality


1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. A : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
6. B : EO+(pMsg(P.M[P])) ─→ ℙ
7. X : InitialSystem(P.M[P])@i
8. Y : InitialSystem(P.M[P])@i
9. system-equiv(P.M[P];X;Y)@i
10. assuming(env,r.A[env;r])
     X |= eo.B[eo]@i
11. Z : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];Y;Z)@i
13. env : pEnvType(P.M[P])@i
14. W : System(P.M[P])
15. std-initial(W)
16. system-equiv(P.M[P];W;Z)
17. sub-system(P.M[P];X;W)
18. pRun(W;env;n2m;l2m) = pRun(Z;env;n2m;l2m) ∈ pRunType(P.M[P])
19. z : pRunType(P.M[P])
20. z = pRun(W;env;n2m;l2m) ∈ pRunType(P.M[P])
21. A[env;z]
22. e : runEvents(z)@i
23. run-initialization(z;snd(W))
⊢ fst(fst(run-info(z;e))) < run-event-step(e)
BY
{ (HypSubst' -4 -1 THEN Auto) }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. A : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
6. B : EO+(pMsg(P.M[P])) ─→ ℙ
7. X : InitialSystem(P.M[P])@i
8. Y : InitialSystem(P.M[P])@i
9. system-equiv(P.M[P];X;Y)@i
10. assuming(env,r.A[env;r])
     X |= eo.B[eo]@i
11. Z : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];Y;Z)@i
13. env : pEnvType(P.M[P])@i
14. W : System(P.M[P])
15. std-initial(W)
16. system-equiv(P.M[P];W;Z)
17. sub-system(P.M[P];X;W)
18. pRun(W;env;n2m;l2m) = pRun(Z;env;n2m;l2m) ∈ pRunType(P.M[P])
19. z : pRunType(P.M[P])
20. z = pRun(W;env;n2m;l2m) ∈ pRunType(P.M[P])
21. A[env;z]
22. e : runEvents(z)@i
23. run-initialization(pRun(W;env;n2m;l2m);snd(W))
⊢ fst(fst(run-info(z;e))) < run-event-step(e)

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  A  :  pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}
6.  B  :  EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}
7.  X  :  InitialSystem(P.M[P])@i
8.  Y  :  InitialSystem(P.M[P])@i
9.  system-equiv(P.M[P];X;Y)@i
10.  assuming(env,r.A[env;r])
          X  |=  eo.B[eo]@i
11.  Z  :  InitialSystem(P.M[P])@i
12.  sub-system(P.M[P];Y;Z)@i
13.  env  :  pEnvType(P.M[P])@i
14.  W  :  System(P.M[P])
15.  std-initial(W)
16.  system-equiv(P.M[P];W;Z)
17.  sub-system(P.M[P];X;W)
18.  pRun(W;env;n2m;l2m)  =  pRun(Z;env;n2m;l2m)
19.  z  :  pRunType(P.M[P])
20.  z  =  pRun(W;env;n2m;l2m)
21.  A[env;z]
22.  e  :  runEvents(z)@i
23.  run-initialization(z;snd(W))
\mvdash{}  fst(fst(run-info(z;e)))  <  run-event-step(e)


By

---

Latex:
(HypSubst'  -4  -1  THEN  Auto)

---

Home Index