Nuprl Lemma : cond-msg-body-sv-bag-only

[f:Name ─→ Type]. ∀[hdr:Name]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[T:Type].
  (sv-bag-only(cond-msg-body(hdr;info(e))) ∈ T) supposing ((header(e) hdr ∈ Name) and hdr encodes T)


Definitions occuring in Statement :  cond-msg-body: cond-msg-body(hdr;msg) encodes-msg-type: hdr encodes T es-header: header(e) Message: Message(f) es-info: info(e) event-ordering+: EO+(Info) es-E: E name: Name uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type equal: t ∈ T sv-bag-only: sv-bag-only(b)
Lemmas :  sv-bag-only_wf cond-msg-body_wf es-info_wf Message_wf cond-msg-body-single-valued name_eq_wf msg-header_wf bool_wf eqtt_to_assert assert-name_eq bag_size_single_lemma eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot bag_size_empty_lemma name_wf es-header_wf encodes-msg-type_wf es-E_wf event-ordering+_subtype event-ordering+_wf

\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr:Name].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[T:Type].
    (sv-bag-only(cond-msg-body(hdr;info(e)))  \mmember{}  T)  supposing  ((header(e)  =  hdr)  and  hdr  encodes  T)

Date html generated: 2015_07_21-PM-04_49_22
Last ObjectModification: 2015_01_28-AM-08_45_38

Home Index