---

Step * 1 2 1 1 1 1 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. 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
⊢ 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:
                                            let Q,ext = Process-apply(C2;ms) 
                                            in <[<C1, Q> / Ds], lg-append(G;add-cause(<n, x>;ext))>))))
= rev(map(λc.(snd(c));filter(λc.fst(c) = x;rev(Ds)))
  @ [fst(Process-apply(C2;ms)) / map(λC.(fst(Process-apply(snd(C);ms)));filter(λc.fst(c) = x;Es))])
∈ (Process(P.M[P]) List)
BY
{ (GenConclAtAddr [3;1;2;1;1] THEN D -2 THEN Reduce 0 THEN Fold `mapfilter` 0 THEN (RWO "-7" 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;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)

---

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
\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:
                                                                                        let  Q,ext  =  Process-apply(C2;ms) 
                                                                                        in  <[<C1,  Q>  /  Ds],  lg-append(G;add-cause(<n,  x>ext))>)\000C)))
=  rev(map(\mlambda{}c.(snd(c));filter(\mlambda{}c.fst(c)  =  x;rev(Ds)))
    @  [fst(Process-apply(C2;ms))  /  map(\mlambda{}C.(fst(Process-apply(snd(C);ms)));filter(\mlambda{}c.fst(c)  =  x;Es))])


By

---

Latex:
(GenConclAtAddr  [3;1;2;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Fold  `mapfilter`  0
  THEN  (RWO  "-7"  0  THENA  Auto))

---

Home Index