---

Step * 1 1 2 2 2 1 2 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. X2 = Y2 ∈ LabeledDAG(pInTransit(P.M[P]))@i
14. ||X1|| = ||Y1|| ∈ ℤ@i
15. ∀k:ℕ||X1||. let x,P = X1[k] in let z,Q = Y1[k] in (x = z ∈ Id) ∧ P≡Q@i
16. assuming(env,r.A[env;r])
     <X1, X2> |= eo.B[eo]@i
17. Z1 : component(P.M[P]) List@i
18. Z2 : LabeledDAG(pInTransit(P.M[P]))@i
19. [%5] : std-initial(<Z1, Z2>)@i
20. f : ℕ||Y1|| ⟶ ℕ||Z1||@i
21. increasing(f;||Y1||)@i
22. ∀j:ℕ||Y1||. (Y1[j] = Z1[f j] ∈ component(P.M[P]))@i
23. Y2 ⊆ Z2@i
24. env : pEnvType(P.M[P])@i
25. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
26. map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List
27. <map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> ∈ System(P.M[P])
28. [%22] : std-initial(<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
29. Z2 = Z2 ∈ LabeledDAG(pInTransit(P.M[P]))
30. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| = ||Z1|| ∈ ℤ
31. ∀k:ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||
      let x,P = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[k] 
      in let z,Q = Z1[k] 
         in (x = z ∈ Id) ∧ P≡Q
32. f ∈ ℕ||X1|| ⟶ ℕ||Z1||
⊢ X1 ⊆ map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))
BY
{ With ⌜f⌝ (D 0)⋅ }

1
.....wf..... 
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. std-initial(<X1, X2>)@i
10. Y1 : component(P.M[P]) List@i
11. Y2 : LabeledDAG(pInTransit(P.M[P]))@i
12. std-initial(<Y1, Y2>)@i
13. X2 = Y2 ∈ LabeledDAG(pInTransit(P.M[P]))@i
14. ||X1|| = ||Y1|| ∈ ℤ@i
15. ∀k:ℕ||X1||. let x,P = X1[k] in let z,Q = Y1[k] in (x = z ∈ Id) ∧ P≡Q@i
16. assuming(env,r.A[env;r])
     <X1, X2> |= eo.B[eo]@i
17. Z1 : component(P.M[P]) List@i
18. Z2 : LabeledDAG(pInTransit(P.M[P]))@i
19. std-initial(<Z1, Z2>)@i
20. f : ℕ||Y1|| ⟶ ℕ||Z1||@i
21. increasing(f;||Y1||)@i
22. ∀j:ℕ||Y1||. (Y1[j] = Z1[f j] ∈ component(P.M[P]))@i
23. Y2 ⊆ Z2@i
24. env : pEnvType(P.M[P])@i
25. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
26. map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List
27. <map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> ∈ System(P.M[P])
28. std-initial(<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
29. Z2 = Z2 ∈ LabeledDAG(pInTransit(P.M[P]))
30. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| = ||Z1|| ∈ ℤ
31. ∀k:ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||
      let x,P = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[k] 
      in let z,Q = Z1[k] 
         in (x = z ∈ Id) ∧ P≡Q
32. f ∈ ℕ||X1|| ⟶ ℕ||Z1||
⊢ f ∈ ℕ||X1|| ⟶ ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||

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. X2 = Y2 ∈ LabeledDAG(pInTransit(P.M[P]))@i
14. ||X1|| = ||Y1|| ∈ ℤ@i
15. ∀k:ℕ||X1||. let x,P = X1[k] in let z,Q = Y1[k] in (x = z ∈ Id) ∧ P≡Q@i
16. assuming(env,r.A[env;r])
     <X1, X2> |= eo.B[eo]@i
17. Z1 : component(P.M[P]) List@i
18. Z2 : LabeledDAG(pInTransit(P.M[P]))@i
19. [%5] : std-initial(<Z1, Z2>)@i
20. f : ℕ||Y1|| ⟶ ℕ||Z1||@i
21. increasing(f;||Y1||)@i
22. ∀j:ℕ||Y1||. (Y1[j] = Z1[f j] ∈ component(P.M[P]))@i
23. Y2 ⊆ Z2@i
24. env : pEnvType(P.M[P])@i
25. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
26. map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List
27. <map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> ∈ System(P.M[P])
28. [%22] : std-initial(<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
29. Z2 = Z2 ∈ LabeledDAG(pInTransit(P.M[P]))
30. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| = ||Z1|| ∈ ℤ
31. ∀k:ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||
      let x,P = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[k] 
      in let z,Q = Z1[k] 
         in (x = z ∈ Id) ∧ P≡Q
32. f ∈ ℕ||X1|| ⟶ ℕ||Z1||
⊢ increasing(f;||X1||)
∧ (∀j:ℕ||X1||
     (X1[j] = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[f j] ∈ component(P.M[P])))

3
.....wf..... 
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. std-initial(<X1, X2>)@i
10. Y1 : component(P.M[P]) List@i
11. Y2 : LabeledDAG(pInTransit(P.M[P]))@i
12. std-initial(<Y1, Y2>)@i
13. X2 = Y2 ∈ LabeledDAG(pInTransit(P.M[P]))@i
14. ||X1|| = ||Y1|| ∈ ℤ@i
15. ∀k:ℕ||X1||. let x,P = X1[k] in let z,Q = Y1[k] in (x = z ∈ Id) ∧ P≡Q@i
16. assuming(env,r.A[env;r])
     <X1, X2> |= eo.B[eo]@i
17. Z1 : component(P.M[P]) List@i
18. Z2 : LabeledDAG(pInTransit(P.M[P]))@i
19. std-initial(<Z1, Z2>)@i
20. f : ℕ||Y1|| ⟶ ℕ||Z1||@i
21. increasing(f;||Y1||)@i
22. ∀j:ℕ||Y1||. (Y1[j] = Z1[f j] ∈ component(P.M[P]))@i
23. Y2 ⊆ Z2@i
24. env : pEnvType(P.M[P])@i
25. d : ∀j:ℕ||Z1||. Dec(∃i:ℕ||Y1||. (j = (f i) ∈ ℤ))
26. map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) ∈ component(P.M[P]) List
27. <map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> ∈ System(P.M[P])
28. std-initial(<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
29. Z2 = Z2 ∈ LabeledDAG(pInTransit(P.M[P]))
30. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| = ||Z1|| ∈ ℤ
31. ∀k:ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||
      let x,P = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[k] 
      in let z,Q = Z1[k] 
         in (x = z ∈ Id) ∧ P≡Q
32. f ∈ ℕ||X1|| ⟶ ℕ||Z1||
33. f1 : ℕ||X1|| ⟶ ℕ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))||
⊢ increasing(f1;||X1||)
  ∧ (∀j:ℕ||X1||
       (X1[j] = map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))[f1 j] ∈ component(P.M[P]))) ∈ ℙ

---

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.  [\%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.  X2  =  Y2@i
14.  ||X1||  =  ||Y1||@i
15.  \mforall{}k:\mBbbN{}||X1||.  let  x,P  =  X1[k]  in  let  z,Q  =  Y1[k]  in  (x  =  z)  \mwedge{}  P\mequiv{}Q@i
16.  assuming(env,r.A[env;r])
          <X1,  X2>  |=  eo.B[eo]@i
17.  Z1  :  component(P.M[P])  List@i
18.  Z2  :  LabeledDAG(pInTransit(P.M[P]))@i
19.  [\%5]  :  std-initial(<Z1,  Z2>)@i
20.  f  :  \mBbbN{}||Y1||  {}\mrightarrow{}  \mBbbN{}||Z1||@i
21.  increasing(f;||Y1||)@i
22.  \mforall{}j:\mBbbN{}||Y1||.  (Y1[j]  =  Z1[f  j])@i
23.  Y2  \msubseteq{}  Z2@i
24.  env  :  pEnvType(P.M[P])@i
25.  d  :  \mforall{}j:\mBbbN{}||Z1||.  Dec(\mexists{}i:\mBbbN{}||Y1||.  (j  =  (f  i)))
26.  map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))  \mmember{}  component(P.M[P])  List
27.  <map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||)),  Z2>  \mmember{}  System(P.M[P])
28.  [\%22]  :  std-initial(<map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))
                                                ,  Z2
                                                >)
29.  Z2  =  Z2
30.  ||map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))||  =  ||Z1||
31.  \mforall{}k:\mBbbN{}||map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))||
            let  x,P  =  map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))[k] 
            in  let  z,Q  =  Z1[k] 
                  in  (x  =  z)  \mwedge{}  P\mequiv{}Q
32.  f  \mmember{}  \mBbbN{}||X1||  {}\mrightarrow{}  \mBbbN{}||Z1||
\mvdash{}  X1  \msubseteq{}  map(\mlambda{}j.case  d  j  of  inl(p)  =>  X1[fst(p)]  |  inr(z)  =>  Z1[j];upto(||Z1||))


By

---

Latex:
With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index