---

Step * 2 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:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;Z) ∧ sub-system(P.M[P];X;W))
⊢ A[env;pRun(Z;env;n2m;l2m)] ⇒ B[EO(pRun(Z;env;n2m;l2m))]
BY
{ (RepeatFor 2 (D -1)
   THEN (Assert pRun(W;env;n2m;l2m) = pRun(Z;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (BLemma `pRun_functionality` THEN Auto))
   THEN StrongRevHypSubst (-1) 0
   THEN Try (Complete (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 : 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])
⊢ A[env;pRun(W;env;n2m;l2m)] ⇒ B[EO(pRun(W;env;n2m;l2m))]

2
.....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)] ∈ ℙ

---

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.  \mexists{}W:InitialSystem(P.M[P]).  (system-equiv(P.M[P];W;Z)  \mwedge{}  sub-system(P.M[P];X;W))
\mvdash{}  A[env;pRun(Z;env;n2m;l2m)]  {}\mRightarrow{}  B[EO(pRun(Z;env;n2m;l2m))]


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (Assert  pRun(W;env;n2m;l2m)  =  pRun(Z;env;n2m;l2m)  BY
                          (BLemma  `pRun\_functionality`  THEN  Auto))
  THEN  StrongRevHypSubst  (-1)  0
  THEN  Try  (Complete  (Auto)))

---

Home Index