---

Step * 1 2 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
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;Ds)
= rev(mapfilter(λc.(snd(c));λc.fst(c) = x;rev(Ds)) @ [])
∈ (Process(P.M[P]) List)
BY
{ (RepUR ``mapfilter`` 0 THEN (RWO "append-nil" 0 THENA Auto)) }

1
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)

---

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{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Ds)  =  rev(mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;rev(Ds))  @  [])


By

---

Latex:
(RepUR  ``mapfilter``  0  THEN  (RWO  "append-nil"  0  THENA  Auto))

---

Home Index