---

Step * 2 of Lemma system-strongly-realizes-and1


1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. [A] : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. S1 : InitialSystem(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. [B1] : EO+(pMsg(P.M[P])) ─→ ℙ
9. [B2] : EO+(pMsg(P.M[P])) ─→ ℙ
10. assuming(env,r.A[env;r])
     S1 |= eo.B1[eo]@i
11. ∀S2@0:InitialSystem(P.M[P]). (sub-system(P.M[P];S2;S2@0) ⇒ assuming(env,r.A[env;r]) S2@0 |- eo.B2[eo])@i
12. S : InitialSystem(P.M[P])@i
13. sub-system(P.M[P];S1;S)@i
14. sub-system(P.M[P];S2;S)@i
15. S3 : InitialSystem(P.M[P])@i
16. sub-system(P.M[P];S;S3)@i
17. assuming(env,r.A[env;r])
     S3 |- eo.B2[eo]
⊢ assuming(env,r.A[env;r])
   S3 |- eo.B1[eo] ∧ B2[eo]
BY
{ (RepeatFor 2 (ParallelLast) THEN All (RepUR ``let``) THEN ParallelLast THEN Auto) }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. [A] : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. S1 : InitialSystem(P.M[P])@i
7. S2 : InitialSystem(P.M[P])@i
8. [B1] : EO+(pMsg(P.M[P])) ─→ ℙ
9. [B2] : EO+(pMsg(P.M[P])) ─→ ℙ
10. assuming(env,r.A[env;r])
     S1 |= eo.B1[eo]@i
11. ∀S2@0:InitialSystem(P.M[P]). (sub-system(P.M[P];S2;S2@0) ⇒ assuming(env,r.A[env;r]) S2@0 |- eo.B2[eo])@i
12. S : InitialSystem(P.M[P])@i
13. sub-system(P.M[P];S1;S)@i
14. sub-system(P.M[P];S2;S)@i
15. S3 : InitialSystem(P.M[P])@i
16. sub-system(P.M[P];S;S3)@i
17. env : pEnvType(P.M[P])@i
18. A[env;pRun(S3;env;n2m;l2m)]@i
19. B2[EO(pRun(S3;env;n2m;l2m))]
⊢ B1[EO(pRun(S3;env;n2m;l2m))]

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  [A]  :  pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}
4.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
6.  S1  :  InitialSystem(P.M[P])@i
7.  S2  :  InitialSystem(P.M[P])@i
8.  [B1]  :  EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}
9.  [B2]  :  EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}
10.  assuming(env,r.A[env;r])
          S1  |=  eo.B1[eo]@i
11.  \mforall{}S2@0:InitialSystem(P.M[P])
            (sub-system(P.M[P];S2;S2@0)  {}\mRightarrow{}  assuming(env,r.A[env;r])  S2@0  |-  eo.B2[eo])@i
12.  S  :  InitialSystem(P.M[P])@i
13.  sub-system(P.M[P];S1;S)@i
14.  sub-system(P.M[P];S2;S)@i
15.  S3  :  InitialSystem(P.M[P])@i
16.  sub-system(P.M[P];S;S3)@i
17.  assuming(env,r.A[env;r])
          S3  |-  eo.B2[eo]
\mvdash{}  assuming(env,r.A[env;r])
      S3  |-  eo.B1[eo]  \mwedge{}  B2[eo]


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  All  (RepUR  ``let``)  THEN  ParallelLast  THEN  Auto)

---

Home Index