Nuprl Lemma : eo-forward-base-classfun-res

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[e':E]. ∀[hdr:Name]. ∀[T:Type].
  (Base(hdr)@e' Base(hdr)@e' ∈ T) supposing ((header(e') hdr ∈ Name) and hdr encodes T)


Definitions occuring in Statement :  base-headers-msg-val: Base(hdr) encodes-msg-type: hdr encodes T es-header: header(e) Message: Message(f) classfun-res: X@e eo-forward: eo.e event-ordering+: EO+(Info) es-E: E name: Name uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  eo-forward-base-classfun equal_wf name_wf es-header_wf subtype_rel_dep_function eo-forward-E-subtype event-ordering+_subtype Message_wf encodes-msg-type_wf es-E_wf eo-forward_wf event-ordering+_wf

\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[e':E].  \mforall{}[hdr:Name].  \mforall{}[T:Type].
    (Base(hdr)@e'  =  Base(hdr)@e')  supposing  ((header(e')  =  hdr)  and  hdr  encodes  T)

Date html generated: 2015_07_21-PM-04_50_51
Last ObjectModification: 2015_01_28-AM-08_44_16

Home Index