Nuprl Lemma : es-authentic_wf

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E].  (es-authentic(es;e) ∈ 𝔹)


Proof




Definitions occuring in Statement :  es-authentic: es-authentic(es;e) Message: Message(f) event-ordering+: EO+(Info) es-E: E name: Name bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  msg-authentic_wf es-info_wf es-E_wf event-ordering+_subtype Message_wf event-ordering+_wf name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].    (es-authentic(es;e)  \mmember{}  \mBbbB{})



Date html generated: 2015_07_21-PM-04_48_30
Last ObjectModification: 2015_01_28-AM-08_46_21

Home Index