---

Step * 1 1 of Lemma system-strongly-realizes_functionality


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))
BY
{ (RenameVar `d' (-1)⋅
   THEN Assert ⌈map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List⌉⋅
   ) }

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. 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. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
⊢ map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List

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. 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. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
24. map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List
⊢ ∃W:InitialSystem(P.M[P]). (system-equiv(P.M[P];W;<Z1, Z2>) ∧ sub-system(P.M[P];<X1, X2>;W))

---

Latex:

---

Latex:

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.  X1  :  component(P.M[P])  List@i
8.  X2  :  LabeledDAG(pInTransit(P.M[P]))@i
9.  \mbackslash{}\mbackslash{}\%7  :  std-initial(<X1,  X2>)@i
10.  Y1  :  component(P.M[P])  List@i
11.  Y2  :  LabeledDAG(pInTransit(P.M[P]))@i
12.  \mbackslash{}\mbackslash{}\%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.  \mbackslash{}\mbackslash{}\%5  :  std-initial(<Z1,  Z2>)@i
18.  f  :  \mBbbN{}||Y1||  {}\mrightarrow{}  \mBbbN{}||Z1||@i
19.  increasing(f;||Y1||)@i
20.  \mforall{}j:\mBbbN{}||Y1||.  (Y1[j]  =  Z1[f  j])@i
21.  Y2  \msubseteq{}  Z2@i
22.  env  :  pEnvType(P.M[P])@i
23.  \mforall{}j:\mBbbN{}||Z1||.  Dec(\mexists{}i:\mBbbN{}||Y1||.  (j  =  (f  i)))
\mvdash{}  \mexists{}W:InitialSystem(P.M[P]).  (system-equiv(P.M[P];W;<Z1,  Z2>)  \mwedge{}  sub-system(P.M[P];<X1,  X2>W))


By

---

Latex:
(RenameVar  `d'  (-1)\mcdot{}
  THEN  Assert  \mkleeneopen{}map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))
                            \mmember{}  component(P.M[P])  List\mkleeneclose{}\mcdot{}
  )

---

Home Index