Step
*
1
2
2
1
1
of Lemma
run-event-state-next2
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. S0 : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. n : {1...}
8. x : Id@i
9. v1 : ℕ@i
10. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
11. v3 : ℕ@i
12. v4 : Id@i
13. (env n pRun(S0;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
14. x2 : ℤ × Id@i
15. x5 : pMsg(P.M[P])@i
16. v7 : component(P.M[P]) List@i
17. v8 : LabeledDAG(pInTransit(P.M[P]))@i
18. do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m) (n - 1)));v1;v3;v4)
= <inl <x2, x, x5>, v7, v8>
∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
19. G : LabeledDAG(pInTransit(P.M[P]))
20. v7 = (fst(deliver-msg(n;x5;x;fst(snd((pRun(S0;env;n2m;l2m) (n - 1))));G))) ∈ (component(P.M[P]) List)
21. mapfilter(λc.(snd(c));λc.fst(c) = x;v7)
= rev(mapfilter(λC.(fst(Process-apply(snd(C);x5)));λc.fst(c) = x;fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))))
∈ (Process(P.M[P]) List)
22. v : ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P])@i
23. (pRun(S0;env;n2m;l2m) (n - 1)) = v ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
⊢ map(λP.(fst(Process-apply(P;x5)));let info,Cs,G = v in
mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))
= mapfilter(λC.(fst(Process-apply(snd(C);x5)));λc.fst(c) = x;fst(snd(v)))
∈ (Process(P.M[P]) List)
BY
{ (RepeatFor 2 (D (-2)) THEN RepUR ``mapfilter`` 0 THEN (RWO "map-map" 0 THENA 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. S0 : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. n : {1...}
8. x : Id@i
9. v1 : ℕ@i
10. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
11. v3 : ℕ@i
12. v4 : Id@i
13. (env n pRun(S0;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
14. x2 : ℤ × Id@i
15. x5 : pMsg(P.M[P])@i
16. v7 : component(P.M[P]) List@i
17. v8 : LabeledDAG(pInTransit(P.M[P]))@i
18. do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m) (n - 1)));v1;v3;v4)
= <inl <x2, x, x5>, v7, v8>
∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
19. G : LabeledDAG(pInTransit(P.M[P]))
20. v7 = (fst(deliver-msg(n;x5;x;fst(snd((pRun(S0;env;n2m;l2m) (n - 1))));G))) ∈ (component(P.M[P]) List)
21. mapfilter(λc.(snd(c));λc.fst(c) = x;v7)
= rev(mapfilter(λC.(fst(Process-apply(snd(C);x5)));λc.fst(c) = x;fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))))
∈ (Process(P.M[P]) List)
22. v9 : ℤ × Id × Id × pMsg(P.M[P])?@i
23. v11 : component(P.M[P]) List@i
24. v12 : LabeledDAG(pInTransit(P.M[P]))@i
25. (pRun(S0;env;n2m;l2m) (n - 1)) = <v9, v11, v12> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
⊢ map((λP.(fst(Process-apply(P;x5)))) o (λc.(snd(c)));filter(λc.fst(c) = x;v11))
= map(λC.(fst(Process-apply(snd(C);x5)));filter(λc.fst(c) = x;v11))
∈ (Process(P.M[P]) List)
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. S0 : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. n : \{1...\}
8. x : Id@i
9. v1 : \mBbbN{}@i
10. \mlambda{}c.fst(c) = x \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{}
11. v3 : \mBbbN{}@i
12. v4 : Id@i
13. (env n pRun(S0;env;n2m;l2m)) = <v1, v3, v4>@i
14. x2 : \mBbbZ{} \mtimes{} Id@i
15. x5 : pMsg(P.M[P])@i
16. v7 : component(P.M[P]) List@i
17. v8 : LabeledDAG(pInTransit(P.M[P]))@i
18. do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m) (n - 1)));v1;v3;v4)
= <inl <x2, x, x5>, v7, v8>@i
19. G : LabeledDAG(pInTransit(P.M[P]))
20. v7 = (fst(deliver-msg(n;x5;x;fst(snd((pRun(S0;env;n2m;l2m) (n - 1))));G)))
21. mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;v7)
= rev(mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);x5)));
\mlambda{}c.fst(c) = x;
fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))))
22. v : \mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])? \mtimes{} System(P.M[P])@i
23. (pRun(S0;env;n2m;l2m) (n - 1)) = v@i
\mvdash{} map(\mlambda{}P.(fst(Process-apply(P;x5)));let info,Cs,G = v in
mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs))
= mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);x5)));\mlambda{}c.fst(c) = x;fst(snd(v)))
By
Latex:
(RepeatFor 2 (D (-2)) THEN RepUR ``mapfilter`` 0 THEN (RWO "map-map" 0 THENA Auto))\mcdot{}
Home
Index