---

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


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
⊢ ∀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>))))
BY
{ ListInd' (-1) }

1
.....wf..... 
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. 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>)))) ∈ (component(P.M[P]) List) ─→ ℙ

2
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
⊢ ∀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:
                                []
                              with starting value:
                               <X, G>))))

3
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. ∀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:
                                 v
                               with starting value:
                                <X, G>))))@i
⊢ ∀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:
                                [u / v]
                              with starting value:
                               <X, G>))))

4
.....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])).
    (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:
                                v
                              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
\mvdash{}  \mforall{}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>))))


By

---

Latex:
ListInd'  (-1)

---

Home Index