---

Step * 1 of Lemma system-strongly-realizes_functionality

.....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))
BY
{ (RepeatFor 2 (DVar `Z')
   THEN RepeatFor 2 (DVar `X')
   THEN RepeatFor 2 (DVar `Y')
   THEN RepUR ``sub-system`` -2
   THEN D -2
   THEN D -3
   THEN ExRepD
   THEN (Assert ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ)) BY
               Auto)) }

1
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. X1 : component(P.M[P]) List@i
8. X2 : LabeledDAG(pInTransit(P.M[P]))@i
9. \\%7 : std-initial(<X1, X2>)@i
10. Y1 : component(P.M[P]) List@i
11. Y2 : LabeledDAG(pInTransit(P.M[P]))@i
12. \\%9 : std-initial(<Y1, Y2>)@i
13. system-equiv(P.M[P];<X1, X2>;<Y1, Y2>)@i
14. assuming(env,r.A[env;r])
     <X1, X2> |= eo.B[eo]@i
15. Z1 : component(P.M[P]) List@i
16. Z2 : LabeledDAG(pInTransit(P.M[P]))@i
17. \\%5 : std-initial(<Z1, Z2>)@i
18. f : ℕ||Y1|| ─→ ℕ||Z1||@i
19. increasing(f;||Y1||)@i
20. ∀j:ℕ||Y1||. (Y1[j] = Z1[f j] ∈ component(P.M[P]))@i
21. Y2 ⊆ Z2@i
22. env : pEnvType(P.M[P])@i
23. ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
⊢ ∃W:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;<Z1, Z2>) ∧ sub-system(P.M[P];<X1, X2>;W))

---

Latex:

---

Latex:
.....assertion..... 
1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  pMsg(P.M[P])@i
5.  [A]  :  pEnvType(P.M[P])  {}\mrightarrow{}  pRunType(P.M[P])  {}\mrightarrow{}  \mBbbP{}
6.  [B]  :  EO+(pMsg(P.M[P]))  {}\mrightarrow{}  \mBbbP{}
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
\mvdash{}  \mexists{}W:InitialSystem(P.M[P]).  (system-equiv(P.M[P];W;Z)  \mwedge{}  sub-system(P.M[P];X;W))


By

---

Latex:
(RepeatFor  2  (DVar  `Z')
  THEN  RepeatFor  2  (DVar  `X')
  THEN  RepeatFor  2  (DVar  `Y')
  THEN  RepUR  ``sub-system``  -2
  THEN  D  -2
  THEN  D  -3
  THEN  ExRepD
  THEN  (Assert  \mforall{}j:\mBbbN{}||Z1||.  Dec(\mexists{}i:\mBbbN{}||Y1||.  (j  =  (f  i)))  BY
                          Auto))

---

Home Index