Nuprl Lemma : es-info-body-equal

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e,e':E]. ∀[T:Type].
  (msgval(e) msgval(e') ∈ T) supposing ((e e' ∈ E) and ((f header(e)) ⊆T))


Proof




Definitions occuring in Statement :  es-info-body: msgval(e) es-header: header(e) Message: Message(f) event-ordering+: EO+(Info) es-E: E name: Name uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  es-info-body_wf equal_wf subtype_rel_wf es-header_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e,e':E].  \mforall{}[T:Type].
    (msgval(e)  =  msgval(e'))  supposing  ((e  =  e')  and  ((f  header(e))  \msubseteq{}r  T))



Date html generated: 2015_07_21-PM-04_48_46
Last ObjectModification: 2015_01_28-AM-08_46_53

Home Index