---

Step * 1 2 1 1 1 1 2 2 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. 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)
BY
{ ((Reduce 0 THEN RWW  "mapfilter-append mapfilter-singleton" 0 THEN Reduce 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;rev(Ds)) @ map(λc.(snd(c));if C1 = x then [<C1, C2>] else [] fi ))
@ mapfilter(λC.(fst(Process-apply(snd(C);ms)));λ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{}  rev(mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;fst(<rev([<C1,  C2>  /  Ds]),  G>))
@  mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Es))
=  rev(mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;rev(Ds))
    @  mapfilter(\mlambda{}C.(fst(Process-apply(snd(C);ms)));\mlambda{}c.fst(c)  =  x;Es))


By

---

Latex:
((Reduce  0  THEN  RWW    "mapfilter-append  mapfilter-singleton"  0  THEN  Reduce  0)  THENA  Auto)

---

Home Index