---

Step * of Lemma system-strongly-realizes-and

∀[M:Type ─→ Type]
  ∀[A:pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ]
    ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S1,S2:InitialSystem(P.M[P]).
      ∀[B1,B2:EO+(pMsg(P.M[P])) ─→ ℙ].
        (assuming(env,r.A[env;r])
          S1 |= eo.B1[eo]
        ⇒ assuming(env,r.A[env;r])
            S2 |= eo.B2[eo]
        ⇒ assuming(env,r.A[env;r])
            S1 @ S2 |= eo.B1[eo] ∧ B2[eo]) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `system-strongly-realizes-and1` []
   THEN RepeatFor 11 ((ParallelLast' THENA Auto))
   THEN BHyp -1 
   THEN Auto
   THEN Try ((BLemma `sub-system-append` THEN Auto)⋅)) }

1
.....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])

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[A:pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}]
        \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S1,S2:InitialSystem(P.M[P]).
            \mforall{}[B1,B2:EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}].
                (assuming(env,r.A[env;r])
                    S1  |=  eo.B1[eo]
                {}\mRightarrow{}  assuming(env,r.A[env;r])
                        S2  |=  eo.B2[eo]
                {}\mRightarrow{}  assuming(env,r.A[env;r])
                        S1  @  S2  |=  eo.B1[eo]  \mwedge{}  B2[eo]) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `system-strongly-realizes-and1`  []
  THEN  RepeatFor  11  ((ParallelLast'  THENA  Auto))
  THEN  BHyp  -1 
  THEN  Auto
  THEN  Try  ((BLemma  `sub-system-append`  THEN  Auto)\mcdot{}))

---

Home Index