{ 
[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))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
deliver-msg: deliver-msg(t;m;x;Cs;L),
pInTransit: pInTransit(P.M[P]),
component: component(P.M[P]),
pMsg: pMsg(P.M[P]),
ldag: LabeledDAG(T),
lg-label: lg-label(g;x),
lg-size: lg-size(g),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
int_seg: {i..j
},
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
pi2: snd(t),
function: x:A B[x],
list: type List,
natural_number: $n,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s],
component: component(P.M[P]),
pi2: snd(t),
deliver-msg: deliver-msg(t;m;x;Cs;L),
list_accum: list_accum(x,a.f[x; a];y;l),
deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),
member: t 
T,
so_lambda: 
x.t[x],
all: x:A. B[x],
implies: P 
Q,
ycomb: Y,
ifthenelse: if b then t else f fi ,
btrue: tt,
prop: 
,
bfalse: ff,
int_seg: {i..j},
rev_implies: P 
Q,
iff: P Q,
lelt: i 
j < k,
and: P 
Q,
le: A B,
not: 
A,
false: False,
ldag: LabeledDAG(T),
nat: ,
bool: 
,
unit: Unit,
it: 
Lemmas :
component_wf,
lg-label_wf_dag,
pInTransit_wf,
int_seg_wf,
lg-size_wf_dag,
ldag_wf,
eq_id_wf,
bool_wf,
iff_weakening_uiff,
uiff_transitivity,
assert_wf,
eqtt_to_assert,
assert-eq-id,
not_wf,
bnot_wf,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
pMsg_wf,
Id_wf,
nat_wf,
strong-type-continuous_wf,
Process-apply_wf,
Process_wf,
pExt_wf,
lg-append_wf_dag,
add-cause_wf,
le_wf,
lg-size-append,
labeled-graph_wf,
is-dag_wf,
lg-size_wf,
lg-append_wf,
lg-label-append,
lt_int_wf,
assert_of_lt_int,
le_int_wf,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int
\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])
Date html generated:
2011_08_16-PM-06_53_38
Last ObjectModification:
2011_06_18-AM-11_08_16
Home
Index