Nuprl Lemma : member-base-class

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[hdr:Name].  header(e) hdr ∈ Name supposing ↑e ∈b Base(hdr)


Proof




Definitions occuring in Statement :  base-headers-msg-val: Base(hdr) es-header: header(e) Message: Message(f) member-eclass: e ∈b X event-ordering+: EO+(Info) es-E: E name: Name assert: b uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T
Lemmas :  member-implies-classrel base-noloc-classrel encodes-msg-type-trivial assert_wf member-eclass_wf Message_wf base-headers-msg-val_wf name_wf es-E_wf event-ordering+_subtype event-ordering+_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[hdr:Name].
    header(e)  =  hdr  supposing  \muparrow{}e  \mmember{}\msubb{}  Base(hdr)



Date html generated: 2015_07_23-AM-11_27_30
Last ObjectModification: 2015_01_28-PM-11_13_19

Home Index