Nuprl Lemma : verify-class-program-wf-hdf

[f:Name ─→ Type]. ∀[hdr:Name]. ∀[T:Type].
  verify-class-program(hdr) ∈ Id ─→ hdataflow(Message(f);T) supposing hdr encodes T


Proof




Definitions occuring in Statement :  verify-class-program: verify-class-program(hdr) encodes-msg-type: hdr encodes T Message: Message(f) Id: Id name: Name uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type hdataflow: hdataflow(A;B)
Lemmas :  hdf-base_wf Message_wf cond-verify-msg-body_wf Id_wf encodes-msg-type_wf name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr:Name].  \mforall{}[T:Type].
    verify-class-program(hdr)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Message(f);T)  supposing  hdr  encodes  T



Date html generated: 2015_07_22-PM-00_03_36
Last ObjectModification: 2015_01_28-AM-09_52_48

Home Index