---

Step * 2 2 of Lemma system-strongly-realizes_functionality

.....wf..... 
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 : InitialSystem(P.M[P])
15. system-equiv(P.M[P];W;Z)
16. sub-system(P.M[P];X;W)
17. pRun(W;env;n2m;l2m) = pRun(Z;env;n2m;l2m) ∈ pRunType(P.M[P])
18. z : pRunType(P.M[P])
19. z = pRun(W;env;n2m;l2m) ∈ pRunType(P.M[P])
⊢ A[env;z] ⇒ B[EO(z)] ∈ ℙ
BY
{ (DVar `W' 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
⊢ fst(fst(run-info(z;e))) < run-event-step(e)

---

Latex:

---

Latex:
.....wf..... 
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  :  InitialSystem(P.M[P])
15.  system-equiv(P.M[P];W;Z)
16.  sub-system(P.M[P];X;W)
17.  pRun(W;env;n2m;l2m)  =  pRun(Z;env;n2m;l2m)
18.  z  :  pRunType(P.M[P])
19.  z  =  pRun(W;env;n2m;l2m)
\mvdash{}  A[env;z]  {}\mRightarrow{}  B[EO(z)]  \mmember{}  \mBbbP{}


By

---

Latex:
(DVar  `W'  THEN  Auto)

---

Home Index