---

Step * 1 2 2 1 1 1 1 of Lemma adjacent-run-states


1. [M] : Type ─→ Type
2. x : Id@i
3. v3 : component(P.M[P]) List@i
4. v11 : Id@i
5. k : ℕ@i
6. ms : pMsg(P.M[P])@i
7. G : LabeledDAG(pInTransit(P.M[P]))@i
8. Continuous+(P.M[P])@i'
9. ¬↑x = v11@i
10. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
11. L : component(P.M[P]) List@i
12. [] = L ∈ (component(P.M[P]) List)@i
13. Z : Process(P.M[P]) List@i
14. [] = Z ∈ (Process(P.M[P]) List)@i
15. Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⊢ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = accumulate (with value S and list item C):
                                                            deliver-msg-to-comp(k;ms;v11;S;C)
                                                           over list:
                                                             v3
                                                           with starting value:
                                                            <L, G>) 
                                                in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
BY
{ (RepeatFor 2 ((MoveToConcl (-1) THEN Thin (-1))) THEN MoveToConcl (-1) THEN MoveToConcl (-4)) }

1
1. [M] : Type ─→ Type
2. x : Id@i
3. v3 : component(P.M[P]) List@i
4. v11 : Id@i
5. k : ℕ@i
6. ms : pMsg(P.M[P])@i
7. Continuous+(P.M[P])@i'
8. ¬↑x = v11@i
9. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
⊢ ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
    (Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
    ⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = accumulate (with value S and list item C):
                                                                 deliver-msg-to-comp(k;ms;v11;S;C)
                                                                over list:
                                                                  v3
                                                                with starting value:
                                                                 <L, G>) 
                                                     in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  x  :  Id@i
3.  v3  :  component(P.M[P])  List@i
4.  v11  :  Id@i
5.  k  :  \mBbbN{}@i
6.  ms  :  pMsg(P.M[P])@i
7.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
8.  Continuous+(P.M[P])@i'
9.  \mneg{}\muparrow{}x  =  v11@i
10.  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}
11.  L  :  component(P.M[P])  List@i
12.  []  =  L@i
13.  Z  :  Process(P.M[P])  List@i
14.  []  =  Z@i
15.  Z  \msubseteq{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;L)
\mvdash{}  Z  @  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v3)
    \msubseteq{}  let  Cs,G  =  accumulate  (with  value  S  and  list  item  C):
                                deliver-msg-to-comp(k;ms;v11;S;C)
                              over  list:
                                  v3
                              with  starting  value:
                                <L,  G>) 
        in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)


By

---

Latex:
(RepeatFor  2  ((MoveToConcl  (-1)  THEN  Thin  (-1)))  THEN  MoveToConcl  (-1)  THEN  MoveToConcl  (-4))

---

Home Index