---

Step * 1 of Lemma system-strongly-realizes-and

.....wf..... 
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. assuming(env,r.A[env;r])
     S2 |= eo.B2[eo]@i
12. ∀S:InitialSystem(P.M[P])
      (sub-system(P.M[P];S1;S) ⇒ sub-system(P.M[P];S2;S) ⇒ assuming(env,r.A[env;r]) S |= eo.B1[eo] ∧ B2[eo])
⊢ S1 @ S2 ∈ InitialSystem(P.M[P])
BY
{ (All Thin THEN RepeatFor 2 (DVar `S1') THEN RepeatFor 2 (DVar `S2')) }

1
1. M : Type ─→ Type
2. S3 : component(P.M[P]) List@i
3. S4 : LabeledDAG(pInTransit(P.M[P]))@i
4. std-initial(<S3, S4>)@i
5. S5 : component(P.M[P]) List@i
6. S6 : LabeledDAG(pInTransit(P.M[P]))@i
7. std-initial(<S5, S6>)@i
⊢ <S3, S4> @ <S5, S6> ∈ InitialSystem(P.M[P])

---

Latex:

---

Latex:
.....wf..... 
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.  assuming(env,r.A[env;r])
          S2  |=  eo.B2[eo]@i
12.  \mforall{}S:InitialSystem(P.M[P])
            (sub-system(P.M[P];S1;S)
            {}\mRightarrow{}  sub-system(P.M[P];S2;S)
            {}\mRightarrow{}  assuming(env,r.A[env;r])
                    S  |=  eo.B1[eo]  \mwedge{}  B2[eo])
\mvdash{}  S1  @  S2  \mmember{}  InitialSystem(P.M[P])


By

---

Latex:
(All  Thin  THEN  RepeatFor  2  (DVar  `S1')  THEN  RepeatFor  2  (DVar  `S2'))

---

Home Index