---

Step * 1 2 1 1 1 1 2 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. 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)
BY
{ (RenameVar `Es' (-4)
   THEN RenameVar `C' (-5)
   THEN DVar `C'
   THEN RepUR ``deliver-msg-to-comp mapfilter`` 0
   THEN Fold `deliver-msg-to-comp` 0
   THEN AutoSplit) }

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
⊢ 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)

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. 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)

---

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.  u  :  component(P.M[P])@i
8.  v  :  component(P.M[P])  List@i
9.  \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:
                                            v
                                        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;v)))@i
10.  Ds  :  component(P.M[P])  List@i
11.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
\mvdash{}  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:
                                    v
                                with  starting  value:
                                  deliver-msg-to-comp(n;ms;x;<Ds,  G>u))))
=  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;[u  /  v]))


By

---

Latex:
(RenameVar  `Es'  (-4)
  THEN  RenameVar  `C'  (-5)
  THEN  DVar  `C'
  THEN  RepUR  ``deliver-msg-to-comp  mapfilter``  0
  THEN  Fold  `deliver-msg-to-comp`  0
  THEN  AutoSplit)

---

Home Index