Nuprl Lemma : es-info-type_wf

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


Proof




Definitions occuring in Statement :  es-info-type: es-info-type(es;e;f) Message: Message(f) event-ordering+: EO+(Info) es-E: E name: Name uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  msg-type_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-info-type(es;e;f)  \mmember{}  Type)



Date html generated: 2015_07_21-PM-04_48_33
Last ObjectModification: 2015_01_28-AM-08_46_15

Home Index