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