---

Step * 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. 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
⊢ sub-system(P.M[P];S2;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.  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
\mvdash{}  sub-system(P.M[P];S2;S3)


By

---

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

---

Home Index