---

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


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. C1 : Id@i
8. ¬(C1 = x ∈ Id)
9. C2 : Process(P.M[P])@i
10. Es : component(P.M[P]) List@i
11. ∀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:
                       Es
                     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\000C(c) = x;Es))
      ∈ (Process(P.M[P]) List))@i
12. Ds : component(P.M[P]) List@i
13. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ map(λc.(snd(c));filter(λc.fst(c) = x;fst(accumulate (with value S and list item C):
                                            deliver-msg-to-comp(n;ms;x;S;C)
                                           over list:
                                             Es
                                           with starting value:
                                            <[<C1, C2> / Ds], G>))))
= rev(map(λc.(snd(c));filter(λc.fst(c) = x;rev(Ds))) @ map(λC.(fst(Process-apply(snd(C);ms)));filter(λc.fst(c) = x;Es)))
∈ (Process(P.M[P]) List)
BY
{ (Fold `mapfilter` 0 THEN (RWO "-3" 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. C1 : Id@i
8. ¬(C1 = x ∈ Id)
9. C2 : Process(P.M[P])@i
10. Es : component(P.M[P]) List@i
11. ∀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:
                       Es
                     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\000C(c) = x;Es))
      ∈ (Process(P.M[P]) List))@i
12. Ds : component(P.M[P]) List@i
13. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ rev(mapfilter(λc.(snd(c));λc.fst(c) = x;fst(<rev([<C1, C2> / Ds]), G>)) @ mapfilter(λC.(fst(Process-apply(snd(C);ms)))\000C;λc.fst(c) = x;Es))
= rev(mapfilter(λc.(snd(c));λc.fst(c) = x;rev(Ds)) @ mapfilter(λC.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;Es))
∈ (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.  C1  :  Id@i
8.  \mneg{}(C1  =  x)
9.  C2  :  Process(P.M[P])@i
10.  Es  :  component(P.M[P])  List@i
11.  \mforall{}Ds:component(P.M[P])  List.  \mforall{}G:LabeledDAG(pInTransit(P.M[P])).
            (mapfilter(\mlambda{}c.(snd(c));
                                  \mlambda{}c.fst(c)  =  x;
                                  fst(accumulate  (with  value  S  and  list  item  C):
                                            deliver-msg-to-comp(n;ms;x;S;C)
                                          over  list:
                                              Es
                                          with  starting  value:
                                            <Ds,  G>)))
            =  rev(mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;fst(<rev(Ds),  G>))
                @  mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Es)))@i
12.  Ds  :  component(P.M[P])  List@i
13.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
\mvdash{}  map(\mlambda{}c.(snd(c));filter(\mlambda{}c.fst(c)  =  x;fst(accumulate  (with  value  S  and  list  item  C):
                                                                                        deliver-msg-to-comp(n;ms;x;S;C)
                                                                                      over  list:
                                                                                          Es
                                                                                      with  starting  value:
                                                                                        <[<C1,  C2>  /  Ds],  G>))))
=  rev(map(\mlambda{}c.(snd(c));filter(\mlambda{}c.fst(c)  =  x;rev(Ds)))
    @  map(\mlambda{}C.(fst(Process-apply(snd(C);ms)));filter(\mlambda{}c.fst(c)  =  x;Es)))


By

---

Latex:
(Fold  `mapfilter`  0  THEN  (RWO  "-3"  0  THENA  Auto))

---

Home Index