---

Step * 1 2 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. G : LabeledDAG(pInTransit(P.M[P]))@i
8. Cs : component(P.M[P]) List@i
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;fst(deliver-msg(n;ms;x;Cs;G)))
= rev(mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;Cs))
∈ (Process(P.M[P]) List)
BY
{ (Subst' mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;Cs) ~ mapfilter(λc.(snd(c));
                                                                                     λc.fst(c) = x;
                                                                                     fst(<rev([]), G>))
   @ mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;Cs) 0
   THENA (RepUR ``mapfilter`` 0 THEN Trivial)
   )
THEN (Unfold `deliver-msg` 0
      THEN (GenConcl ⌈[] = Ds ∈ (component(P.M[P]) List)⌉⋅ THENA Auto)
      THEN Thin (-1)
      THEN MoveToConcl (-3)
      THEN MoveToConcl (-1)
      THEN ListInd (-1)
      THEN Reduce 0
      THEN 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
⊢ 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)

2
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. u : component(P.M[P])@i
8. v : component(P.M[P]) List@i
9. ∀Ds:component(P.M[P]) List. ∀G:LabeledDAG(pInTransit(P.M[P])).
     (mapfilter(λc.(snd(c));
                λc.fst(c) = x;
                fst(accumulate (with value S and list item C):
                     deliver-msg-to-comp(n;ms;x;S;C)
                    over list:
                      v
                    with starting value:
                     <Ds, G>)))
     = rev(mapfilter(λc.(snd(c));λc.fst(c) = x;fst(<rev(Ds), G>)) @ mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(\000Cc) = x;v))
     ∈ (Process(P.M[P]) List))@i
10. Ds : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ mapfilter(λc.(snd(c));
            λc.fst(c) = x;
            fst(accumulate (with value S and list item C):
                 deliver-msg-to-comp(n;ms;x;S;C)
                over list:
                  v
                with starting value:
                 deliver-msg-to-comp(n;ms;x;<Ds, G>;u))))
= rev(mapfilter(λc.(snd(c));λc.fst(c) = x;rev(Ds))
  @ mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;[u / v]))
∈ (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.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
8.  Cs  :  component(P.M[P])  List@i
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;fst(deliver-msg(n;ms;x;Cs;G)))
=  rev(mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Cs))


By

---

Latex:
(Subst'  mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Cs)  \msim{}  mapfilter(\mlambda{}c.(snd(c));
                                                                                                                                                                      \mlambda{}c.fst(c)  =  x;
                                                                                                                                                                      fst(<rev([]),  G>)\000C)
  @  mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Cs)  0
  THENA  (RepUR  ``mapfilter``  0  THEN  Trivial)
  )
THEN  (Unfold  `deliver-msg`  0
            THEN  (GenConcl  \mkleeneopen{}[]  =  Ds\mkleeneclose{}\mcdot{}  THENA  Auto)
            THEN  Thin  (-1)
            THEN  MoveToConcl  (-3)
            THEN  MoveToConcl  (-1)
            THEN  ListInd  (-1)
            THEN  Reduce  0
            THEN  Auto)\mcdot{}

---

Home Index