---

Step * 2 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 : 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))]
BY
{ (Auto
   THEN (((With ⌈W⌉ (D 10)⋅ THENM D -1 THENM With ⌈env⌉ (D (-1))⋅) THEN Auto)
         THEN RepUR ``let`` -1
         THEN ThinTrivial
         THEN Auto)⋅
   ) }

---

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  :  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)
\mvdash{}  A[env;pRun(W;env;n2m;l2m)]  {}\mRightarrow{}  B[EO(pRun(W;env;n2m;l2m))]


By

---

Latex:
(Auto
  THEN  (((With  \mkleeneopen{}W\mkleeneclose{}  (D  10)\mcdot{}  THENM  D  -1  THENM  With  \mkleeneopen{}env\mkleeneclose{}  (D  (-1))\mcdot{})  THEN  Auto)
              THEN  RepUR  ``let``  -1
              THEN  ThinTrivial
              THEN  Auto)\mcdot{}
  )

---

Home Index