Nuprl Lemma : eo-msg-interface-constraint_wf

[f:Name ─→ Type]. ∀[X:EClass(Interface)]. ∀[hdrs:Name List]. ∀[es:EO+(Message(f))].
  (eo-msg-interface-constraint(es;X;hdrs;f) ∈ ℙ)


Proof




Definitions occuring in Statement :  eo-msg-interface-constraint: eo-msg-interface-constraint(es;X;hdrs;f) msg-interface: Interface Message: Message(f) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) name: Name list: List uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  all_wf es-E_wf event-ordering+_subtype l_member_wf es-header_wf squash_wf exists_wf es-causl_wf classrel_wf make-msg-interface_wf es-loc_wf es-info_wf event-ordering+_wf Message_wf list_wf name_wf eclass_wf3 msg-interface_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(Interface)].  \mforall{}[hdrs:Name  List].  \mforall{}[es:EO+(Message(f))].
    (eo-msg-interface-constraint(es;X;hdrs;f)  \mmember{}  \mBbbP{})



Date html generated: 2015_07_22-AM-11_59_28
Last ObjectModification: 2015_01_28-AM-08_41_46

Home Index