---

Step * 1 1 of Lemma run-event-state_wf


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
BY
{ (Using [`T', component(P.M[P])] MemCD⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  fulpRunType(P.M[P])
3.  e1  :  \mBbbN{}
4.  e2  :  Id
5.  v1  :  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  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>@i
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  e2;v3)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(Using  [`T',  component(P.M[P])]  MemCD\mcdot{}  THEN  Auto)

---

Home Index