Nuprl Lemma : es-info-make-Msg-iff

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


Proof




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: 𝔹 uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  equal_wf Message_wf make-Msg_wf es-info_wf es-info-make-Msg equal-wf-T-base bool_wf msg-authentic_wf es-header_wf subtype_rel_dep_function name_wf msg-body_wf2 subtype_base_sq list_subtype_base atom_subtype_base subtype_rel_self es-E_wf event-ordering+_subtype event-ordering+_wf bfalse_wf basicMessage_wf msg-msg_wf and_wf pi1_wf_top subtype_rel_product top_wf subtype_top

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



Date html generated: 2015_07_21-PM-04_53_54
Last ObjectModification: 2015_01_28-AM-08_43_09

Home Index