### Nuprl Lemma : es-info-make-Msg-iff2

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

Proof

Definitions occuring in Statement :  make-Msg: `make-Msg(hdr;val)` es-info-body: `msgval(e)` es-header: `header(e)` es-authentic: `es-authentic(es;e)` 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: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  es-info-make-Msg-iff

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);es-authentic(es;e)  =  ff  \mwedge{}  (header(e)  =  hdr)  \mwedge{}  (msgval(e)  =  v))

Date html generated: 2015_07_21-PM-04_53_56
Last ObjectModification: 2015_01_28-AM-08_42_05

Home Index