---

Step * of Lemma lg-label-deliver-msg

∀[M:Type ⟶ Type]
  ∀[t:ℕ]. ∀[x:Id]. ∀[m:pMsg(P.M[P])]. ∀[Cs:component(P.M[P]) List]. ∀[G:LabeledDAG(pInTransit(P.M[P]))].
  ∀[i:ℕlg-size(G)].
    (lg-label(snd(deliver-msg(t;m;x;Cs;G));i) = lg-label(G;i) ∈ pInTransit(P.M[P])) 
  supposing Continuous+(P.M[P])
BY
{ (RepUR ``deliver-msg`` 0
   THEN RepeatFor 6 ((D 0 THENA Auto))
   THEN (GenConcl ⌜[] = X ∈ (component(P.M[P]) List)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN ListInd' (-1)
   THEN Try ((Reduce 0
              THEN Auto
              THEN DVar `u'
              THEN RepUR ``deliver-msg-to-comp`` 0
              THEN AutoSplit
              THEN Fold `deliver-msg-to-comp` 0
              THEN Try ((BackThruSomeHyp THEN Unfold `component` 0 THEN Auto))))) }

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]))]. ∀[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:
                          Cs
                        with starting value:
                         <X, G>));i)
          = lg-label(G;i)
          ∈ pInTransit(P.M[P])) ∈ (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])
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
⊢ 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:
                let Q,ext = Process-apply(u2;m) 
                in <[<u1, Q> / X], lg-append(G;add-cause(<t, x>;ext))>));i)
= lg-label(G;i)
∈ pInTransit(P.M[P])

3
.....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]))]. ∀[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])) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[t:\mBbbN{}].  \mforall{}[x:Id].  \mforall{}[m:pMsg(P.M[P])].  \mforall{}[Cs:component(P.M[P])  List].
    \mforall{}[G:LabeledDAG(pInTransit(P.M[P]))].  \mforall{}[i:\mBbbN{}lg-size(G)].
        (lg-label(snd(deliver-msg(t;m;x;Cs;G));i)  =  lg-label(G;i)) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(RepUR  ``deliver-msg``  0
  THEN  RepeatFor  6  ((D  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}[]  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ListInd'  (-1)
  THEN  Try  ((Reduce  0
                        THEN  Auto
                        THEN  DVar  `u'
                        THEN  RepUR  ``deliver-msg-to-comp``  0
                        THEN  AutoSplit
                        THEN  Fold  `deliver-msg-to-comp`  0
                        THEN  Try  ((BackThruSomeHyp  THEN  Unfold  `component`  0  THEN  Auto)))))

---

Home Index