Nuprl 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])
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,
list: T List,
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],
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Lemmas :
nil_wf,
list_induction,
list_accum_nil_lemma,
lg-label_wf,
pInTransit_wf,
int_seg_wf,
lg-size_wf,
ldag_wf,
list_accum_cons_lemma,
eq_id_wf,
bool_wf,
eqtt_to_assert,
assert-eq-id,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
cons_wf,
Process_wf,
list_wf,
component_wf,
pMsg_wf,
Id_wf,
nat_wf,
strong-type-continuous_wf,
list_accum_wf,
System_wf,
deliver-msg-to-comp_wf,
all_wf,
uall_wf,
lg-size-deliver-msg-general,
less_than_transitivity1,
lelt_wf,
le_wf,
Process-apply_wf,
pExt_wf,
lg-append_wf_dag,
add-cause_wf,
lg-append_wf,
iff_weakening_equal,
less_than_wf,
squash_wf,
true_wf,
lg-size-append,
lg-label-append,
lt_int_wf,
assert_of_lt_int
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])
Date html generated:
2015_07_23-AM-11_09_05
Last ObjectModification:
2015_02_04-PM-04_48_19
Home
Index