---

Step * 2 1 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. 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))]
BY
{ ((With ⌈S3⌉ (D 10)⋅ THEN Auto) THEN D -1) }

1
.....antecedent..... 
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. ∀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
11. S : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];S1;S)@i
13. sub-system(P.M[P];S2;S)@i
14. S3 : InitialSystem(P.M[P])@i
15. sub-system(P.M[P];S;S3)@i
16. env : pEnvType(P.M[P])@i
17. A[env;pRun(S3;env;n2m;l2m)]@i
18. B2[EO(pRun(S3;env;n2m;l2m))]
⊢ sub-system(P.M[P];S1;S3)

2
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. ∀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
11. S : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];S1;S)@i
13. sub-system(P.M[P];S2;S)@i
14. S3 : InitialSystem(P.M[P])@i
15. sub-system(P.M[P];S;S3)@i
16. env : pEnvType(P.M[P])@i
17. A[env;pRun(S3;env;n2m;l2m)]@i
18. B2[EO(pRun(S3;env;n2m;l2m))]
19. assuming(env,r.A[env;r])
     S3 |- eo.B1[eo]@i
⊢ 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.  env  :  pEnvType(P.M[P])@i
18.  A[env;pRun(S3;env;n2m;l2m)]@i
19.  B2[EO(pRun(S3;env;n2m;l2m))]
\mvdash{}  B1[EO(pRun(S3;env;n2m;l2m))]


By

---

Latex:
((With  \mkleeneopen{}S3\mkleeneclose{}  (D  10)\mcdot{}  THEN  Auto)  THEN  D  -1)

---

Home Index