---

Step * of Lemma system-strongly-realizes_functionality

∀[M:Type ─→ Type]
  ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]).
    ∀[A:pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ]. ∀[B:EO+(pMsg(P.M[P])) ─→ ℙ].
      ∀X,Y:InitialSystem(P.M[P]).
        (system-equiv(P.M[P];X;Y) ⇒ assuming(env,r.A[env;r]) X |= eo.B[eo] ⇒ assuming(env,r.A[env;r]) Y |= eo.B[eo]) 
  supposing Continuous+(P.M[P])
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN RenameVar `Z' (-3)
   THEN RepUR ``let`` 0
   THEN Assert ⌈∃W:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;Z) ∧ sub-system(P.M[P];X;W))⌉⋅) }

1
.....assertion..... 
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. [A] : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
6. [B] : EO+(pMsg(P.M[P])) ─→ ℙ
7. X : InitialSystem(P.M[P])@i
8. Y : InitialSystem(P.M[P])@i
9. system-equiv(P.M[P];X;Y)@i
10. assuming(env,r.A[env;r])
     X |= eo.B[eo]@i
11. Z : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];Y;Z)@i
13. env : pEnvType(P.M[P])@i
⊢ ∃W:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;Z) ∧ sub-system(P.M[P];X;W))

2
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. [A] : pEnvType(P.M[P]) ─→ pRunType(P.M[P]) ─→ ℙ
6. [B] : EO+(pMsg(P.M[P])) ─→ ℙ
7. X : InitialSystem(P.M[P])@i
8. Y : InitialSystem(P.M[P])@i
9. system-equiv(P.M[P];X;Y)@i
10. assuming(env,r.A[env;r])
     X |= eo.B[eo]@i
11. Z : InitialSystem(P.M[P])@i
12. sub-system(P.M[P];Y;Z)@i
13. env : pEnvType(P.M[P])@i
14. ∃W:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;Z) ∧ sub-system(P.M[P];X;W))
⊢ A[env;pRun(Z;env;n2m;l2m)] ⇒ B[EO(pRun(Z;env;n2m;l2m))]

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).
        \mforall{}[A:pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}].
            \mforall{}X,Y:InitialSystem(P.M[P]).
                (system-equiv(P.M[P];X;Y)
                {}\mRightarrow{}  assuming(env,r.A[env;r])
                        X  |=  eo.B[eo]
                {}\mRightarrow{}  assuming(env,r.A[env;r])
                        Y  |=  eo.B[eo]) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  RenameVar  `Z'  (-3)
  THEN  RepUR  ``let``  0
  THEN  Assert  \mkleeneopen{}\mexists{}W:InitialSystem(P.M[P]).  (system-equiv(P.M[P];W;Z)  \mwedge{}  sub-system(P.M[P];X;W))\mkleeneclose{}\mcdot{})

---

Home Index