---

Step * 1 2 1 1 1 1 2 1 1 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. C2 : Process(P.M[P])@i
9. Es : component(P.M[P]) List@i
10. ∀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
11. Ds : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. C1 = x ∈ Id
14. v1 : Process(P.M[P])@i
15. v2 : pExt(P.M[P])@i
16. Process-apply(C2;ms) = <v1, v2> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
⊢ rev(mapfilter(λc.(snd(c));λc.fst(c) = x;fst(<rev([<C1, v1> / Ds]), lg-append(G;add-cause(<n, x>;v2))>)) @ mapfilter(λC\000C.(fst(Process-apply(snd(C);ms)));λc.fst(c) = x;Es))
= rev(mapfilter(λc.(snd(c));λc.fst(c) = x;rev(Ds))
  @ [v1 / 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. C2 : Process(P.M[P])@i
9. Es : component(P.M[P]) List@i
10. ∀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
11. Ds : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
13. C1 = x ∈ Id
14. v1 : Process(P.M[P])@i
15. v2 : pExt(P.M[P])@i
16. Process-apply(C2;ms) = <v1, v2> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
⊢ rev((mapfilter(λc.(snd(c));λc.fst(c) = x;rev(Ds)) @ map(λc.(snd(c));if C1 = x then [<C1, v1>] 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))
  @ [v1 / 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.  C2  :  Process(P.M[P])@i
9.  Es  :  component(P.M[P])  List@i
10.  \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
11.  Ds  :  component(P.M[P])  List@i
12.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
13.  C1  =  x
14.  v1  :  Process(P.M[P])@i
15.  v2  :  pExt(P.M[P])@i
16.  Process-apply(C2;ms)  =  <v1,  v2>@i
\mvdash{}  rev(mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;fst(<rev([<C1,  v1>  /  Ds]),  lg-append(G;add-cause(<n,  x>v2\000C))>))
@  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))
    @  [v1  /  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