Step
*
2
1
1
1
1
1
of Lemma
pRun-intransit-invariant
.....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
⊢ ∀x∈H.((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
BY
{ ((At ⌈Type⌉ (RevHypSubst (-1) 0)⋅ THEN Auto) THENA skip{(D (-1) THEN RepUR ``let`` 0 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. 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
⊢ ∀x∈lg-remove(G;v1).((fst(fst(x))) ≤ (t1 + 1)) ∨ (∃m:ℕlg-size(G0). ((fst(x)) = (fst(lg-label(G0;m))) ∈ (ℤ × Id)))
Latex:
Latex:
.....assertion.....
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
\mvdash{} \mforall{}x\mmember{}H.((fst(fst(x))) \mleq{} (t1 + 1)) \mvee{} (\mexists{}m:\mBbbN{}lg-size(G0). ((fst(x)) = (fst(lg-label(G0;m)))))
By
Latex:
((At \mkleeneopen{}Type\mkleeneclose{} (RevHypSubst (-1) 0)\mcdot{} THEN Auto) THENA skip\{(D (-1) THEN RepUR ``let`` 0 THEN Auto)\})
Home
Index