---

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


1. M : Type ⟶ Type@i'
2. Continuous+(P.M[P])@i'
3. n : {1...}@i
4. x : Id@i
5. λc.fst(c) = x ∈ component(P.M[P]) ⟶ 𝔹@i
6. ms : pMsg(P.M[P])@i
7. Ds : component(P.M[P]) List@i
8. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ map(λc.(snd(c));filter(λc.fst(c) = x;Ds))
= rev(map(λc.(snd(c));filter(λc.fst(c) = x;rev(Ds))))
∈ (Process(P.M[P]) List)
BY
{ (Fold `mapfilter` 0 THEN RWW "mapfilter-reverse reverse-reverse" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type@i'
2.  Continuous+(P.M[P])@i'
3.  n  :  \{1...\}@i
4.  x  :  Id@i
5.  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}@i
6.  ms  :  pMsg(P.M[P])@i
7.  Ds  :  component(P.M[P])  List@i
8.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
\mvdash{}  map(\mlambda{}c.(snd(c));filter(\mlambda{}c.fst(c)  =  x;Ds))  =  rev(map(\mlambda{}c.(snd(c));filter(\mlambda{}c.fst(c)  =  x;rev(Ds))))


By

---

Latex:
(Fold  `mapfilter`  0  THEN  RWW  "mapfilter-reverse  reverse-reverse"  0  THEN  Auto)

---

Home Index