---

Step * 1 2 2 1 1 1 1 of Lemma run-event-state-next


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. (fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))) = (fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))) ∈ (component(P.M[P]) List)
23. r : fulpRunType(P.M[P])@i
24. pRun(S0;env;n2m;l2m) = r ∈ fulpRunType(P.M[P])@i
25. ∃m:ℕn
     ((run-prior-state(S0;r;<n, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P]) \000CList))
     ∧ (∀t:{m + 1..n-}. (¬↑is-run-event(r;t;x))))@i
⊢ sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;x5)));run-prior-state(S0;r;<n, x>)); mapfilter(λC.(fst(Process-a\000Cpply(snd(C);x5)));
                                                    λc.fst(c) = x;
                                                    fst(snd((r (n - 1))))))
BY
{ (RepeatFor 2 (D (-1)) THEN HypSubst' (-2) 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. 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. (fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))) = (fst(snd((pRun(S0;env;n2m;l2m) (n - 1))))) ∈ (component(P.M[P]) List)
23. r : fulpRunType(P.M[P])@i
24. pRun(S0;env;n2m;l2m) = r ∈ fulpRunType(P.M[P])@i
25. m : ℕn@i
26. run-prior-state(S0;r;<n, x>) = let info,Cs,G = r m in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ∈ (Process(P.M[P]) Lis\000Ct)@i
27. ∀t:{m + 1..n-}. (¬↑is-run-event(r;t;x))@i
⊢ sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;x5)));let info,Cs,G = r m in 
                                mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)); mapfilter(λC.(fst(Process-apply(snd(C);x5)));
                                                                                    λc.fst(c) = x;
                                                                                    fst(snd((r (n - 1))))))

---

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.  (fst(snd((pRun(S0;env;n2m;l2m)  (n  -  1)))))  =  (fst(snd((pRun(S0;env;n2m;l2m)  (n  -  1)))))
23.  r  :  fulpRunType(P.M[P])@i
24.  pRun(S0;env;n2m;l2m)  =  r@i
25.  \mexists{}m:\mBbbN{}n
          ((run-prior-state(S0;r;<n,  x>)  =  let  info,Cs,G  =  r  m  in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)\000C)
          \mwedge{}  (\mforall{}t:\{m  +  1..n\msupminus{}\}.  (\mneg{}\muparrow{}is-run-event(r;t;x))))@i
\mvdash{}  sub-mset(Process(P.M[P]);  map(\mlambda{}P.(fst(Process-apply(P;x5)));run-prior-state(S0;r;<n,  x>));  mapfilt\000Cer(\mlambda{}C.(fst(Process-apply(snd(C);x5)));
                                                                                                        \mlambda{}c.fst(c)  =  x;
                                                                                                        fst(snd((r  (n  -  1))))))


By

---

Latex:
(RepeatFor  2  (D  (-1))  THEN  HypSubst'  (-2)  0  THEN  Auto)\mcdot{}

---

Home Index