Nuprl Lemma : deliver-msg_functionality
∀[M:Type ─→ Type]
∀t:ℕ. ∀x:Id. ∀m:pMsg(P.M[P]). ∀G1,G2:LabeledDAG(pInTransit(P.M[P])). ∀Cs1,Cs2:component(P.M[P]) List.
((∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
∧ (deliver-msg(t;m;x;Cs1;G1)
= deliver-msg(t;m;x;Cs2;G2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))) supposing
((||Cs1|| = ||Cs2|| ∈ ℤ) and
(G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))))
supposing Continuous+(P.M[P])
Proof
Definitions occuring in Statement :
deliver-msg: deliver-msg(t;m;x;Cs;L),
system-equiv: system-equiv(T.M[T];S1;S2),
pInTransit: pInTransit(P.M[P]),
component: component(P.M[P]),
process-equiv: process-equiv,
pMsg: pMsg(P.M[P]),
ldag: LabeledDAG(T),
Id: Id,
select: L[n],
length: ||as||,
list: T List,
strong-type-continuous: Continuous+(T.F[T]),
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ─→ B[x],
spread: spread def,
product: x:A × B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
list_induction,
list_wf,
component_wf,
Id_wf,
Process_wf,
sq_stable__le,
select_wf,
less_than_transitivity1,
length_wf,
le_weakening,
process-equiv_wf,
system-equiv_wf,
top_wf,
ldag_wf,
pInTransit_wf,
list_accum_wf,
deliver-msg-to-comp_wf,
all_wf,
equal_wf,
int_seg_wf,
System_wf,
list-cases,
length_of_nil_lemma,
stuck-spread,
base_wf,
list_accum_nil_lemma,
product_subtype_list,
length_of_cons_lemma,
list_accum_cons_lemma,
non_neg_length,
length_wf_nat,
equal-wf-base-T,
cons_wf,
equal-wf-T-base,
length_cons,
select_cons_tl,
decidable__lt,
false_wf,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-commutes,
add_functionality_wrt_le,
add-associates,
add-zero,
le-add-cancel,
decidable__le,
not-le-2,
less-iff-le,
add-swap,
le-add-cancel2,
iff_weakening_equal,
trivial-int-eq1,
subtype_base_sq,
atom2_subtype_base,
eq_id_wf,
bool_wf,
eqtt_to_assert,
assert-eq-id,
eqff_to_assert,
bool_cases_sqequal,
bool_subtype_base,
assert-bnot,
pMsg_wf,
nil_wf,
data_stream_nil_lemma,
data-stream-cons,
Process-apply_wf,
pExt_wf,
hd_wf,
listp_properties,
assert_of_lt_int,
cons_neq_nil,
nat_wf,
assert_wf,
lt_int_wf,
set_wf,
reduce_hd_cons_lemma,
tl_wf,
reduce_tl_cons_lemma,
and_wf,
add-cause_wf,
lg-append_wf_dag,
decidable__equal_int,
int_subtype_base,
not-equal-2,
minus-zero,
le_antisymmetry_iff,
subtract_wf,
minus-minus,
lelt_wf,
subtype_rel_list,
cons_one_one,
Process-stream_wf,
squash_wf,
true_wf,
pi1_wf_top,
subtype_rel_product,
subtype_top,
pi2_wf,
ge_wf,
cons_wf_listp
Latex:
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}t:\mBbbN{}. \mforall{}x:Id. \mforall{}m:pMsg(P.M[P]). \mforall{}G1,G2:LabeledDAG(pInTransit(P.M[P])).
\mforall{}Cs1,Cs2:component(P.M[P]) List.
((\mforall{}k:\mBbbN{}||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z) \mwedge{} P\mequiv{}Q)
{}\mRightarrow{} (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
\mwedge{} (deliver-msg(t;m;x;Cs1;G1) = deliver-msg(t;m;x;Cs2;G2)))) supposing
((||Cs1|| = ||Cs2||) and
(G1 = G2))
supposing Continuous+(P.M[P])
Date html generated:
2015_07_23-AM-11_08_51
Last ObjectModification:
2015_02_04-PM-04_51_34
Home
Index