### 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))|