---

Step * 1 of Lemma run-event-state_wf


1. M : Type ─→ Type
2. r : fulpRunType(P.M[P])
3. e1 : ℕ
4. e2 : Id
⊢ let info,Cs,G = r e1 in 
  mapfilter(λc.(snd(c));λc.fst(c) = e2;Cs) ∈ Process(P.M[P]) List
BY
{ (GenConclAtAddr [2;1] THEN RepeatFor 2 (D -2) THEN Reduce 0) }

1
1. M : Type ─→ Type
2. r : fulpRunType(P.M[P])
3. e1 : ℕ
4. e2 : Id
5. v1 : ℤ × Id × Id × pMsg(P.M[P])?@i
6. v3 : component(P.M[P]) List@i
7. v4 : LabeledDAG(pInTransit(P.M[P]))@i
8. (r e1) = <v1, v3, v4> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
⊢ mapfilter(λc.(snd(c));λc.fst(c) = e2;v3) ∈ Process(P.M[P]) List

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  fulpRunType(P.M[P])
3.  e1  :  \mBbbN{}
4.  e2  :  Id
\mvdash{}  let  info,Cs,G  =  r  e1  in 
    mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  e2;Cs)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  RepeatFor  2  (D  -2)  THEN  Reduce  0)

---

Home Index