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 y) 0 ∈ ℤ (x y ∈ (f h))))


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: List valueall-type: valueall-type(T) bnot: ¬bb uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ─→ B[x] natural_number: $n int: universe: Type equal: 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

\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