Nuprl Lemma : es-info-make-Msg

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name]. ∀[v:f hdr].
  (make-Msg(hdr;v) info(e) ∈ Message(f)) supposing 
     (msg-authentic(info(e)) ff and 
     (msg-body(info(e)) v ∈ (f hdr)) and 
     (header(e) hdr ∈ Name))


Definitions occuring in Statement :  make-Msg: make-Msg(hdr;val) es-header: header(e) msg-body: msg-body(msg) msg-authentic: msg-authentic(m) Message: Message(f) es-info: info(e) event-ordering+: EO+(Info) es-E: E name: Name bfalse: ff bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  equal-wf-T-base bool_wf msg-authentic_wf equal_wf es-header_wf subtype_rel_dep_function name_wf es-E_wf event-ordering+_subtype event-ordering+_wf Message_wf es-info_wf subtype_base_sq bool_subtype_base subtype_rel_self subtype_rel_wf make-Msg_wf list_subtype_base atom_subtype_base msg-body_wf2

\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].  \mforall{}[v:f  hdr].
    (make-Msg(hdr;v)  =  info(e))  supposing 
          (msg-authentic(info(e))  =  ff  and 
          (msg-body(info(e))  =  v)  and 
          (header(e)  =  hdr))

Date html generated: 2015_07_21-PM-04_53_49
Last ObjectModification: 2015_01_28-AM-08_44_53

Home Index