---

Step * 2 1 3 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. 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
9. X : component(P.M[P]) List@i
10. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ 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:
                            deliver-msg-to-comp(t;m;x;<X, G>;u))))
BY
{ (D 6 THEN RepUR ``deliver-msg-to-comp`` 0 THEN AutoSplit THEN Fold `deliver-msg-to-comp` 0) }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
6. u1 : Id@i
7. u2 : Process(P.M[P])@i
8. v : component(P.M[P]) List@i
9. ∀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
10. X : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))@i
12. u1 = x ∈ Id
⊢ 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:
                            let Q,ext = Process-apply(u2;m) 
                            in <[<u1, Q> / X], lg-append(G;add-cause(<t, x>;ext))>)))

2
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. t : ℕ
4. x : Id
5. m : pMsg(P.M[P])
6. u1 : Id@i
7. ¬(u1 = x ∈ Id)
8. u2 : Process(P.M[P])@i
9. v : component(P.M[P]) List@i
10. ∀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
11. X : component(P.M[P]) List@i
12. G : LabeledDAG(pInTransit(P.M[P]))@i
⊢ 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:
                            <[<u1, u2> / 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.  u  :  component(P.M[P])@i
7.  v  :  component(P.M[P])  List@i
8.  \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:
                                                                  v
                                                              with  starting  value:
                                                                <X,  G>))))@i
9.  X  :  component(P.M[P])  List@i
10.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
\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:
                                                          v
                                                      with  starting  value:
                                                        deliver-msg-to-comp(t;m;x;<X,  G>u))))


By

---

Latex:
(D  6  THEN  RepUR  ``deliver-msg-to-comp``  0  THEN  AutoSplit  THEN  Fold  `deliver-msg-to-comp`  0)

---

Home Index