Nuprl Lemma : es-info-mk-msg

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


Definitions occuring in Statement :  mk-msg: mk-msg(auth;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 bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  equal_wf msg-authentic_wf es-header_wf subtype_rel_dep_function name_wf bool_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 list_subtype_base atom_subtype_base msg-body_wf2

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

Date html generated: 2015_07_21-PM-04_53_52
Last ObjectModification: 2015_01_28-AM-08_42_22

Home Index