---

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

∀[M:Type ─→ Type]
  ∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[Cs,X:component(P.M[P]) List]. ∀[G:LabeledDAG(pInTransit(P.M[P]))].
    (lg-size(G) ≤ 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>)))) 
  supposing Continuous+(P.M[P])
BY
{ (Intros THEN (Unhide THENA Auto)) }

1
.....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>))) ∈ ℤ

2
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(G) ≤ 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>)))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[t:\mBbbN{}].  \mforall{}[x:Id].  \mforall{}[m:pMsg(P.M[P])].  \mforall{}[Cs,X:component(P.M[P])  List].
    \mforall{}[G:LabeledDAG(pInTransit(P.M[P]))].
        (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>)))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto))

---

Home Index