---

Step * of Lemma system-strongly-realizes-and1

∀[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]
        ⇒ (∀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]))) 
  supposing Continuous+(P.M[P])
BY
{ (Auto THEN RepeatFor 2 (ParallelOp -4) THEN ParallelLast) }

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

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. 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. assuming(env,r.A[env;r])
     S3 |- eo.B2[eo]
⊢ assuming(env,r.A[env;r])
   S3 |- eo.B1[eo] ∧ B2[eo]

---

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{}  (\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]))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelOp  -4)  THEN  ParallelLast)

---

Home Index