Nuprl Lemma : order-messages_wf
∀[allhdrs:Name List]. ∀[f:hdr:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)].
order-messages(mcmp;locs;allhdrs) ∈ {b:bag(Interface(to locs, with allhdrs))|
single-valued-bag([mi∈b|¬bmsg-header(mi.msg) ∈b hdrs)];Interface)} ─→ (Interface\000C(to locs, with allhdrs) List)
supposing (∀h∈allhdrs.valueall-type(f h)) ∧ (∀h∈hdrs.∀x,y:f h. (((mcmp h x y) = 0 ∈ ℤ) ⇒ (x = y ∈ (f h))))
Proof
Definitions occuring in Statement :
order-messages: order-messages(mcmp;locs;hdrs),
constrained-msg-interface: Interface(to locs, with hdrs),
msg-interface-message: mi.msg,
msg-interface: Interface,
msg-header: msg-header(m),
Id: Id,
name-deq: NameDeq,
name: Name,
deq-member: x ∈b L),
comparison: comparison(T),
l_all: (∀x∈L.P[x]),
list: T List,
valueall-type: valueall-type(T),
bnot: ¬bb,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T,
single-valued-bag: single-valued-bag(b;T),
bag-filter: [x∈b|p[x]],
bag: bag(T)
Lemmas :
bag-to-list_wf,
constrained-msg-interface-valueall-type,
interface-cmp_wf,
subtype_rel_comparison,
bag-member_wf,
interface-cmp-zero,
equal-wf-T-base,
comparison_wf,
set_wf,
bag_wf,
constrained-msg-interface_wf,
single-valued-bag_wf,
msg-interface_wf,
bag-filter_wf,
bnot_wf,
deq-member_wf,
name-deq_wf,
msg-header_wf,
msg-interface-message_wf,
subtype_rel_bag,
assert_wf,
l_all_wf2,
name_wf,
l_member_wf,
valueall-type_wf,
all_wf,
list_wf,
Id_wf,
decidable__l_member,
decidable__equal_name,
l_all_iff,
msg-body_wf2,
msg-type_wf,
subtype_rel-equal,
iff_weakening_equal,
msg-interface-destination_wf,
msg-interface-extensionality,
Message-extensionality,
bag-member-subtype,
bag-member-filter,
iff_transitivity,
not_wf,
iff_weakening_uiff,
assert_of_bnot,
assert-deq-member,
squash_wf,
true_wf
Latex:
\mforall{}[allhdrs:Name List]. \mforall{}[f:hdr:Name {}\mrightarrow{} Type]. \mforall{}[locs:Id List]. \mforall{}[hdrs:Name List].
\mforall{}[mcmp:hdr:Name {}\mrightarrow{} comparison(f hdr)].
order-messages(mcmp;locs;allhdrs) \mmember{} \{b:bag(Interface(to locs, with allhdrs))|
single-valued-bag([mi\mmember{}b|\mneg{}\msubb{}msg-header(mi.msg) \mmember{}\msubb{} hdrs)];
Interface)\} {}\mrightarrow{} (Interface(to locs, with allhdrs) List)
supposing (\mforall{}h\mmember{}allhdrs.valueall-type(f h)) \mwedge{} (\mforall{}h\mmember{}hdrs.\mforall{}x,y:f h. (((mcmp h x y) = 0) {}\mRightarrow{} (x = y)))
Date html generated:
2015_07_22-PM-00_01_26
Last ObjectModification:
2015_02_04-PM-05_08_10
Home
Index