Nuprl Lemma : local-simulation-event-loc

[f:Name ─→ Type]. ∀[Info:Type]. ∀[es:EO+(Message(f))]. ∀[hdr:Name]. ∀[locs:bag(Id)].
  ∀[e:E]
    loc(local-simulation-event(es;e;hdr;locs)) (fst(msg-body(info(e)))) ∈ Id 
    supposing ↑has-header-and-in-locs(info(e);hdr;locs) 
  supposing hdr encodes Id × Info


Proof




Definitions occuring in Statement :  local-simulation-event: local-simulation-event(es;e;hdr;locs) local-simulation-eo: local-simulation-eo(es;e;hdr;locs) has-header-and-in-locs: has-header-and-in-locs(msg;hdr;locs) encodes-msg-type: hdr encodes T msg-body: msg-body(msg) Message: Message(f) es-info: info(e) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id name: Name assert: b uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) function: x:A ─→ B[x] product: x:A × B[x] universe: Type equal: t ∈ T bag: bag(T)
Lemmas :  global-eo-loc map_append_sq filter_append_sq filter_wf5 map_wf es-info_wf es-before_wf l_member_wf has-header-and-in-locs_wf list_wf map_cons_lemma map_nil_lemma filter_cons_lemma filter_nil_lemma bool_wf eqtt_to_assert eqff_to_assert assert_elim bfalse_wf and_wf equal_wf bnot_wf btrue_neq_bfalse bool_cases_sqequal subtype_base_sq bool_subtype_base assert_wf Message_wf subtype_rel_product Id_wf top_wf subtype_rel_transitivity es-E_wf event-ordering+_subtype encodes-msg-type_wf bag_wf name_wf event-ordering+_wf cons_wf msg-type_wf msg-body_wf nil_wf subtype_rel_list length_wf_nat lt_int_wf length_wf assert_of_lt_int less_than_irreflexivity assert-bnot less_than_wf select-append length-map int_subtype_base minus-one-mul add-mul-special zero-mul assert-has-header-and-in-locs pi1_wf_top msg-body_wf2 list_subtype_base atom_subtype_base

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[Info:Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[hdr:Name].  \mforall{}[locs:bag(Id)].
    \mforall{}[e:E]
        loc(local-simulation-event(es;e;hdr;locs))  =  (fst(msg-body(info(e)))) 
        supposing  \muparrow{}has-header-and-in-locs(info(e);hdr;locs) 
    supposing  hdr  encodes  Id  \mtimes{}  Info



Date html generated: 2015_07_21-PM-04_50_33
Last ObjectModification: 2015_01_28-AM-08_47_15

Home Index