Proof of Nuprl Lemma : system-strongly-realizes

Step * 1 1 2 2 2 1 2 1 2 2 1 1 of Lemma system-strongly-realizes_functionality

.....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. j : ℕ||X1||@i
⊢ d upto(||Z1||)[f j] ∈ Dec(∃i:ℕ||Y1||. (upto(||Z1||)[f 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. 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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

40. ||upto(||Z1||)|| ≥ 0
41. ||Z1|| ≥ 0
42. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
43. j2 : ℕ||Z1||@i
44. p1 : ∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ)

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

46. ||upto(||Z1||)|| ≥ 0
47. ||Z1|| ≥ 0
48. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
49. j3 : ℕ||Z1||@i
50. p2 : ∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ)

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

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. 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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

3
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

4
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

5
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

6
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

7
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

8
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. j : ℕ||X1||@i
34. ||upto(||Z1||)|| ≥ 0
35. ||Z1|| ≥ 0
36. ||map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))|| ≥ 0
37. j1 : ℕ||Z1||@i
38. p : ∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ)

39. (d j1) = (inl p) ∈ (∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j1 = (f i) ∈ ℤ))))

45. (d j2) = (inl p1) ∈ (∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j2 = (f i) ∈ ℤ))))

51. (d j3) = (inl p2) ∈ (∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ) + (¬(∃i:ℕ||Y1||. (j3 = (f i) ∈ ℤ))))

⊢ fst(p2) < ||X1||

Latex:

Latex:
.....wf..... 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. 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@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. 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. 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|| 33. j : \mBbbN{}||X1||@i \mvdash{} d upto(||Z1||)[f j] \mmember{} Dec(\mexists{}i:\mBbbN{}||Y1||. (upto(||Z1||)[f j] = (f i))) By Latex: Auto Home Index