---

Step * 1 2 2 1 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. 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))
BY
{ (ListInd 3 THEN Reduce 0) }

1
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λ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;L))

2
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
9. u : component(P.M[P])@i
10. v : component(P.M[P]) List@i
11. ∀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;v) ⊆ let Cs,G = accumulate (with value S and list item C):
                                                                  deliver-msg-to-comp(k;ms;v11;S;C)
                                                                 over list:
                                                                   v
                                                                 with starting value:
                                                                  <L, G>) 
                                                      in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))@i
⊢ ∀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;[u / v]) ⊆ let Cs,G = accumulate (with value S and list item C):
                                                                      deliver-msg-to-comp(k;ms;v11;S;C)
                                                                     over list:
                                                                       v
                                                                     with starting value:
                                                                      deliver-msg-to-comp(k;ms;v11;<L, G>;u)) 
                                                          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.  Continuous+(P.M[P])@i'
8.  \mneg{}\muparrow{}x  =  v11@i
9.  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mforall{}G:LabeledDAG(pInTransit(P.M[P])).  \mforall{}L:component(P.M[P])  List.  \mforall{}Z:Process(P.M[P])  List.
        (Z  \msubseteq{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;L)
        {}\mRightarrow{}  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:
(ListInd  3  THEN  Reduce  0)

---

Home Index