---

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


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]))]. ∀[i:ℕlg-size(G)].
       (lg-label(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)
       = lg-label(G;i)
       ∈ pInTransit(P.M[P]))@i
10. X : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))
12. i : ℕlg-size(G)
13. u1 = x ∈ Id
14. v2 : Process(P.M[P])@i
15. v3 : pExt(P.M[P])@i
16. Process-apply(u2;m) = <v2, v3> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
⊢ lg-label(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, v2> / X], lg-append(G;add-cause(<t, x>;v3))>));i)
= lg-label(G;i)
∈ pInTransit(P.M[P])
BY
{ (RWO "9" 0 THEN Auto THEN Try ((Unfold `component` 0 THEN Auto))) }

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]))]. ∀[i:ℕlg-size(G)].
       (lg-label(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)
       = lg-label(G;i)
       ∈ pInTransit(P.M[P]))@i
10. X : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))
12. i : ℤ
13. 0 ≤ i
14. i < lg-size(G)
15. u1 = x ∈ Id
16. v2 : Process(P.M[P])@i
17. v3 : pExt(P.M[P])@i
18. Process-apply(u2;m) = <v2, v3> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
⊢ i < lg-size(lg-append(G;add-cause(<t, x>;v3)))

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. 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]))]. ∀[i:ℕlg-size(G)].
       (lg-label(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)
       = lg-label(G;i)
       ∈ pInTransit(P.M[P]))@i
10. X : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))
12. i : ℕlg-size(G)
13. u1 = x ∈ Id
14. v2 : Process(P.M[P])@i
15. v3 : pExt(P.M[P])@i
16. Process-apply(u2;m) = <v2, v3> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
⊢ lg-label(lg-append(G;add-cause(<t, x>;v3));i) = lg-label(G;i) ∈ pInTransit(P.M[P])

---

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.  u1  :  Id@i
7.  u2  :  Process(P.M[P])@i
8.  v  :  component(P.M[P])  List@i
9.  \mforall{}X:component(P.M[P])  List
          \mforall{}[G:LabeledDAG(pInTransit(P.M[P]))].  \mforall{}[i:\mBbbN{}lg-size(G)].
              (lg-label(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)
              =  lg-label(G;i))@i
10.  X  :  component(P.M[P])  List@i
11.  G  :  LabeledDAG(pInTransit(P.M[P]))
12.  i  :  \mBbbN{}lg-size(G)
13.  u1  =  x
14.  v2  :  Process(P.M[P])@i
15.  v3  :  pExt(P.M[P])@i
16.  Process-apply(u2;m)  =  <v2,  v3>@i
\mvdash{}  lg-label(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,  v2>  /  X],  lg-append(G;add-cause(<t,  x>v3))>));i)
=  lg-label(G;i)


By

---

Latex:
(RWO  "9"  0  THEN  Auto  THEN  Try  ((Unfold  `component`  0  THEN  Auto)))

---

Home Index