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


1. Type ─→ Type
2. Continuous+(P.M[P])
3. : ℕ
4. Id
5. pMsg(P.M[P])
6. Cs component(P.M[P]) List
7. component(P.M[P]) List
8. LabeledDAG(pInTransit(P.M[P]))
⊢ lg-size(G) ≤ lg-size(snd(accumulate (with value and list item C):
                            deliver-msg-to-comp(t;m;x;S;C)
                           over list:
                             Cs
                           with starting value:
                            <X, G>)))
BY
RepeatFor (MoveToConcl (-1)) }

1
1. Type ─→ Type
2. Continuous+(P.M[P])
3. : ℕ
4. Id
5. pMsg(P.M[P])
6. Cs component(P.M[P]) List
⊢ ∀X:component(P.M[P]) List. ∀G:LabeledDAG(pInTransit(P.M[P])).
    (lg-size(G) ≤ lg-size(snd(accumulate (with value and list item C):
                               deliver-msg-to-comp(t;m;x;S;C)
                              over list:
                                Cs
                              with starting value:
                               <X, G>))))


Latex:



Latex:

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(G)  \mleq{}  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


Latex:
RepeatFor  2  (MoveToConcl  (-1))




Home Index