---

Step * 1 of Lemma lg-size-deliver-msg-general

.....wf..... 
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
6. Cs : component(P.M[P]) List
7. X : component(P.M[P]) List
8. G : LabeledDAG(pInTransit(P.M[P]))
⊢ lg-size(snd(accumulate (with value S and list item C):
               deliver-msg-to-comp(t;m;x;S;C)
              over list:
                Cs
              with starting value:
               <X, G>))) ∈ ℤ
BY
{ (GenConcl ⌈accumulate (with value S and list item C):
              deliver-msg-to-comp(t;m;x;S;C)
             over list:
               Cs
             with starting value:
              <X, G>)
             = p
             ∈ (component(P.M[P]) List × LabeledDAG(pInTransit(P.M[P])))⌉⋅
   THEN Auto
   ) }

---

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.  Cs  :  component(P.M[P])  List
7.  X  :  component(P.M[P])  List
8.  G  :  LabeledDAG(pInTransit(P.M[P]))
\mvdash{}  lg-size(snd(accumulate  (with  value  S  and  list  item  C):
                              deliver-msg-to-comp(t;m;x;S;C)
                            over  list:
                                Cs
                            with  starting  value:
                              <X,  G>)))  \mmember{}  \mBbbZ{}


By

---

Latex:
(GenConcl  \mkleeneopen{}accumulate  (with  value  S  and  list  item  C):
                        deliver-msg-to-comp(t;m;x;S;C)
                      over  list:
                          Cs
                      with  starting  value:
                        <X,  G>)
                      =  p\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index