Step
*
1
1
2
2
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. 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
25. <map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> ∈ System(P.M[P])
26. [%22] : std-initial(<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
⊢ system-equiv(P.M[P];<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>;<Z1, Z2>) ∧ sub-syst\000Cem(P.M[P];<X1, X2>;<map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>)
BY
{ (All (RepUR ``system-equiv sub-system``) THEN 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. 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||))||@i
⊢ 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
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
⊢ X1 ⊆ map(λj.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))
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. 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 : \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. d : \mforall{}j:\mBbbN{}||Z1||. Dec(\mexists{}i:\mBbbN{}||Y1||. (j = (f i)))
24. map(\mlambda{}j.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)) \mmember{} component(P.M[P]) List
25. <map(\mlambda{}j.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2> \mmember{} System(P.M[P])
26. [\%22] : std-initial(<map(\mlambda{}j.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||))
, Z2
>)
\mvdash{} system-equiv(P.M[P];<map(\mlambda{}j.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)), Z2>
<Z1, Z2>)
\mwedge{} sub-system(P.M[P];<X1, X2><map(\mlambda{}j.case d j of inl(p) => X1[fst(p)] | inr(z) => Z1[j];upto(||Z1||)\000C), Z2>)
By
Latex:
(All (RepUR ``system-equiv sub-system``) THEN Auto)\mcdot{}
Home
Index