Step
*
2
1
3
1
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. 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))>)))
BY
{ (GenConclAtAddr [2;1;1;2;1] THEN D -2 THEN Reduce 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
13. v2 : Process(P.M[P])@i
14. v3 : pExt(P.M[P])@i
15. Process-apply(u2;m) = <v2, v3> ∈ (Process(P.M[P]) × pExt(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, v2> / X], lg-append(G;add-cause(<t, x>;v3))>)))
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])).
(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
10. X : component(P.M[P]) List@i
11. G : LabeledDAG(pInTransit(P.M[P]))@i
12. u1 = x
\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:
let Q,ext = Process-apply(u2;m)
in <[<u1, Q> / X], lg-append(G;add-cause(<t, x>ext))>)))
By
Latex:
(GenConclAtAddr [2;1;1;2;1] THEN D -2 THEN Reduce 0)
Home
Index