---

Step * 3 1 of Lemma lg-label-deliver-msg

.....subterm..... T:t
2:n
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@i
9. G : LabeledDAG(pInTransit(P.M[P]))@i
10. i : ℕlg-size(G)@i
⊢ i ∈ ℕ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>)))
BY
{ (((InstLemma `lg-size-deliver-msg-general` [⌈M⌉;⌈t⌉;⌈x⌉;⌈m⌉;⌈v⌉;⌈X⌉;⌈G⌉]⋅ THENM MoveToConcl (-1)) THENA Auto)
   THEN GenConcl ⌈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>)
                  = p
                  ∈ (component(P.M[P]) List × LabeledDAG(pInTransit(P.M[P])))⌉⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  t  :  \mBbbN{}
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@i
9.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
10.  i  :  \mBbbN{}lg-size(G)@i
\mvdash{}  i  \mmember{}  \mBbbN{}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>)))


By

---

Latex:
(((InstLemma  `lg-size-deliver-msg-general`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{}]\mcdot{}  THENM  MoveToConcl  (-1))
    THENA  Auto
    )
  THEN  GenConcl  \mkleeneopen{}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>)
                                =  p\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index