---

Step * 3 of Lemma lg-label-deliver-msg

.....wf..... 
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
6. u : component(P.M[P])@i
7. v : component(P.M[P]) List@i
⊢ ∀X:component(P.M[P]) List
    ∀[G:LabeledDAG(pInTransit(P.M[P]))]. ∀[i:ℕlg-size(G)].
      (lg-label(snd(accumulate (with value S and list item C):
                     deliver-msg-to-comp(t;m;x;S;C)
                    over list:
                      v
                    with starting value:
                     <X, G>));i)
      = lg-label(G;i)
      ∈ pInTransit(P.M[P])) ∈ ℙ
BY
{ (RepeatFor 5 (MemCD) THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
6. u : component(P.M[P])@i
7. v : component(P.M[P]) List@i
8. X : component(P.M[P]) List@i
9. G : LabeledDAG(pInTransit(P.M[P]))@i
10. i : ℕlg-size(G)@i
⊢ i ∈ ℕlg-size(snd(accumulate (with value S and list item C):
                    deliver-msg-to-comp(t;m;x;S;C)
                   over list:
                     v
                   with starting value:
                    <X, G>)))

---

Latex:

---

Latex:
.....wf..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  t  :  \mBbbN{}
4.  x  :  Id
5.  m  :  pMsg(P.M[P])
6.  u  :  component(P.M[P])@i
7.  v  :  component(P.M[P])  List@i
\mvdash{}  \mforall{}X:component(P.M[P])  List
        \mforall{}[G:LabeledDAG(pInTransit(P.M[P]))].  \mforall{}[i:\mBbbN{}lg-size(G)].
            (lg-label(snd(accumulate  (with  value  S  and  list  item  C):
                                          deliver-msg-to-comp(t;m;x;S;C)
                                        over  list:
                                            v
                                        with  starting  value:
                                          <X,  G>));i)
            =  lg-label(G;i))  \mmember{}  \mBbbP{}


By

---

Latex:
(RepeatFor  5  (MemCD)  THEN  Try  (Complete  (Auto)))

---

Home Index