Nuprl Lemma : classfun-res-base-classrel

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


Definitions occuring in Statement :  base-headers-msg-val: Base(hdr) encodes-msg-type: hdr encodes T Message: Message(f) classfun-res: X@e classrel: v ∈ X(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 :  classfun-res-member-base assert-member-eclass base-headers-msg-val_wf classrel_wf base-noloc-classrel Message_wf encodes-msg-type_wf name_wf es-E_wf event-ordering+_subtype event-ordering+_wf

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

Date html generated: 2015_07_23-AM-11_28_58
Last ObjectModification: 2015_01_28-PM-11_12_37

Home Index