Nuprl Lemma : base-class-program_wf

[f:Name ⟶ Type]. ∀[hdr:Name]. ∀[T:Type].  base-class-program(hdr) ∈ LocalClass(Base(hdr)) supposing hdr encodes T


Proof




Definitions occuring in Statement :  base-class-program: base-class-program(hdr) base-headers-msg-val: Base(hdr) encodes-msg-type: hdr encodes T Message: Message(f) local-class: LocalClass(X) name: Name uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a base-class-program: base-class-program(hdr) local-class: LocalClass(X) sq_exists: x:{A| B[x]} so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] subtype_rel: A ⊆B implies:  Q top: Top pi1: fst(t) hdf-ap: X(a) hdf-base: hdf-base(m.F[m]) mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) ifthenelse: if then else fi  bfalse: ff hdf-run: hdf-run(P) prop: base-headers-msg-val: Base(hdr) class-ap: X(e) pi2: snd(t) encodes-msg-type: hdr encodes T

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr:Name].  \mforall{}[T:Type].
    base-class-program(hdr)  \mmember{}  LocalClass(Base(hdr))  supposing  hdr  encodes  T



Date html generated: 2016_05_17-AM-09_07_56
Last ObjectModification: 2015_12_29-PM-03_36_30

Theory : local!classes


Home Index