---

Step * 2 1 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])
⊢ λ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) ─→ ℙ
BY
{ (RepeatFor 4 (MemCD)
   THEN Try (QuickAuto)
   THEN (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])
\mvdash{}  \mlambda{}Cs.\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>))))  \mmember{}  (component(P.M[P])  List)  {}\mrightarrow{}  \mBbbP{}


By

---

Latex:
(RepeatFor  4  (MemCD)
  THEN  Try  (QuickAuto)
  THEN  (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