---

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

.....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)
BY
{ (Using [`S2', ⌈S⌉] (BLemma `sub-system_transitivity`)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
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.  \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
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))]
\mvdash{}  sub-system(P.M[P];S1;S3)


By

---

Latex:
(Using  [`S2',  \mkleeneopen{}S\mkleeneclose{}]  (BLemma  `sub-system\_transitivity`)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index