Step
*
2
1
1
1
1
2
of Lemma
pRun-intransit-invariant
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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
(((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. t1 : ℕ@i
11. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : ℕ@i
16. v3 : ℕ@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
19. ↑null(lg-in-edges(G;v1))
20. v1 < lg-size(G)
21. v5 : ℤ × Id@i
22. v7 : Id@i
23. v8 : pCom(P.M[P])@i
24. lg-label(G;v1) = <v5, v7, v8> ∈ pInTransit(P.M[P])@i
25. H : LabeledDAG(pInTransit(P.M[P]))@i
26. lg-remove(G;v1) = H ∈ LabeledDAG(pInTransit(P.M[P]))@i
27. ∀x∈H.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⊢ let Cs,G = snd(if com-kind(v8) =a "msg" then <inl <v5, v7, comm-msg(v8)>, deliver-msg(t1 + 1;comm-msg(v8);v7;C;H)>
if com-kind(v8) =a "create" then <inr ⋅ , create-component(t1 + 1;comm-create(v8);v7;C;H)>
if com-kind(v8) =a "choose" then <inl <v5, v7, n2m v3>, deliver-msg(t1 + 1;n2m v3;v7;C;H)>
if com-kind(v8) =a "new" then <inl <v5, v7, l2m v4>, deliver-msg(t1 + 1;l2m v4;v7;C;H)>
else <inr ⋅ , C, H>
fi )
in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
BY
{ Assert ⌈∀[M:Type ─→ Type]
∀G0:LabeledDAG(pInTransit(P.M[P])). ∀t1:ℕ. ∀C:component(P.M[P]) List. ∀v7:Id.
(Continuous+(P.M[P])
⇒ (∀H:LabeledDAG(pInTransit(P.M[P]))
(∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⇒ (∀v:pMsg(P.M[P]). ∀cs:component(P.M[P]) List.
let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(t1;v;v7;S;C)
over list:
C
with starting value:
<cs, H>)
in ∀x∈G.((fst(fst(x))) ≤ t1)
∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))⌉⋅ }
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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
(((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. t1 : ℕ@i
11. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : ℕ@i
16. v3 : ℕ@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
19. ↑null(lg-in-edges(G;v1))
20. v1 < lg-size(G)
21. v5 : ℤ × Id@i
22. v7 : Id@i
23. v8 : pCom(P.M[P])@i
24. lg-label(G;v1) = <v5, v7, v8> ∈ pInTransit(P.M[P])@i
25. H : LabeledDAG(pInTransit(P.M[P]))@i
26. lg-remove(G;v1) = H ∈ LabeledDAG(pInTransit(P.M[P]))@i
27. ∀x∈H.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⊢ ∀[M:Type ─→ Type]
∀G0:LabeledDAG(pInTransit(P.M[P])). ∀t1:ℕ. ∀C:component(P.M[P]) List. ∀v7:Id.
(Continuous+(P.M[P])
⇒ (∀H:LabeledDAG(pInTransit(P.M[P]))
(∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⇒ (∀v:pMsg(P.M[P]). ∀cs:component(P.M[P]) List.
let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(t1;v;v7;S;C)
over list:
C
with starting value:
<cs, H>)
in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))
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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : ℕ@i
9. ∀x:pInTransit(P.M[P]). ∀t:ℤ.
(((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id))) ∈ ℙ)
10. t1 : ℕ@i
11. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : ℕ@i
16. v3 : ℕ@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>;e1;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
19. ↑null(lg-in-edges(G;v1))
20. v1 < lg-size(G)
21. v5 : ℤ × Id@i
22. v7 : Id@i
23. v8 : pCom(P.M[P])@i
24. lg-label(G;v1) = <v5, v7, v8> ∈ pInTransit(P.M[P])@i
25. H : LabeledDAG(pInTransit(P.M[P]))@i
26. lg-remove(G;v1) = H ∈ LabeledDAG(pInTransit(P.M[P]))@i
27. ∀x∈H.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
28. ∀[M:Type ─→ Type]
∀G0:LabeledDAG(pInTransit(P.M[P])). ∀t1:ℕ. ∀C:component(P.M[P]) List. ∀v7:Id.
(Continuous+(P.M[P])
⇒ (∀H:LabeledDAG(pInTransit(P.M[P]))
(∀x∈H.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
⇒ (∀v:pMsg(P.M[P]). ∀cs:component(P.M[P]) List.
let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(t1;v;v7;S;C)
over list:
C
with starting value:
<cs, H>)
in ∀x∈G.((fst(fst(x))) ≤ t1) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))))))
⊢ let Cs,G = snd(if com-kind(v8) =a "msg" then <inl <v5, v7, comm-msg(v8)>, deliver-msg(t1 + 1;comm-msg(v8);v7;C;H)>
if com-kind(v8) =a "create" then <inr ⋅ , create-component(t1 + 1;comm-create(v8);v7;C;H)>
if com-kind(v8) =a "choose" then <inl <v5, v7, n2m v3>, deliver-msg(t1 + 1;n2m v3;v7;C;H)>
if com-kind(v8) =a "new" then <inl <v5, v7, l2m v4>, deliver-msg(t1 + 1;l2m v4;v7;C;H)>
else <inr ⋅ , C, H>
fi )
in ∀x∈G.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
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. Cs0 : component(P.M[P]) List@i
6. G0 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. t : \mBbbN{}@i
9. \mforall{}x:pInTransit(P.M[P]). \mforall{}t:\mBbbZ{}.
(((fst(fst(x))) \mleq{} t) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))))) \mmember{} \mBbbP{})
10. t1 : \mBbbN{}@i
11. C : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. \mforall{}x\mmember{}G.((fst(fst(x))) \mleq{} t1) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))@i
14. e1 : pEnvType(P.M[P])@i
15. v1 : \mBbbN{}@i
16. v3 : \mBbbN{}@i
17. v4 : Id@i
18. (e1 (t1 + 1) pRun(<Cs0, G0>e1;n2m;l2m)) = <v1, v3, v4>@i
19. \muparrow{}null(lg-in-edges(G;v1))
20. v1 < lg-size(G)
21. v5 : \mBbbZ{} \mtimes{} Id@i
22. v7 : Id@i
23. v8 : pCom(P.M[P])@i
24. lg-label(G;v1) = <v5, v7, v8>@i
25. H : LabeledDAG(pInTransit(P.M[P]))@i
26. lg-remove(G;v1) = H@i
27. \mforall{}x\mmember{}H.((fst(fst(x))) \mleq{} (t1 + 1)) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))
\mvdash{} let Cs,G = snd(if com-kind(v8) =a "msg"
then <inl <v5, v7, comm-msg(v8)>, deliver-msg(t1 + 1;comm-msg(v8);v7;C;H)>
if com-kind(v8) =a "create" then <inr \mcdot{} , create-component(t1 + 1;comm-create(v8);v7;C;H)>
if com-kind(v8) =a "choose" then <inl <v5, v7, n2m v3>, deliver-msg(t1 + 1;n2m v3;v7;C;H)>
if com-kind(v8) =a "new" then <inl <v5, v7, l2m v4>, deliver-msg(t1 + 1;l2m v4;v7;C;H)>
else <inr \mcdot{} , C, H>
fi )
in \mforall{}x\mmember{}G.((fst(fst(x))) \mleq{} (t1 + 1)) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))
By
Latex:
Assert \mkleeneopen{}\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}G0:LabeledDAG(pInTransit(P.M[P])). \mforall{}t1:\mBbbN{}. \mforall{}C:component(P.M[P]) List. \mforall{}v7:Id.
(Continuous+(P.M[P])
{}\mRightarrow{} (\mforall{}H:LabeledDAG(pInTransit(P.M[P]))
(\mforall{}x\mmember{}H.((fst(fst(x))) \mleq{} t1) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))
{}\mRightarrow{} (\mforall{}v:pMsg(P.M[P]). \mforall{}cs:component(P.M[P]) List.
let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(t1;v;v7;S;C)
over list:
C
with starting value:
<cs, H>)
in \mforall{}x\mmember{}G.((fst(fst(x))) \mleq{} t1)
\mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))))))\mkleeneclose{}\mcdot{}
Home
Index