Nuprl Lemma : strong-message-constraint-no-rep-large_wf

[f:Name ─→ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) ∈ ℙ')


Proof




Definitions occuring in Statement :  strong-message-constraint-no-rep-large: strong-message-constraint-no-rep-large{i:l}(es;X;hdrs;f) Message: Message(f) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id name: Name list: List uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ─→ B[x] product: x:A × B[x] universe: Type
Lemmas :  all_wf es-E_wf event-ordering+_subtype squash_wf exists_wf bag_wf bag-no-repeats_wf bag-member_wf not_wf es-locl_wf es-causl_wf sub-bag_wf Id_wf Message_wf delivered-with-headers_wf list-subtype-bag l_member_wf msg-header_wf class-output_wf es-le_wf list_wf name_wf eclass_wf3 subtype_rel_dep_function event-ordering+_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[X:EClass(Id  \mtimes{}  Message(f))].  \mforall{}[hdrs:Name  List].
    (strong-message-constraint-no-rep-large\{i:l\}(es;X;hdrs;f)  \mmember{}  \mBbbP{}')



Date html generated: 2015_07_21-PM-04_51_34
Last ObjectModification: 2015_01_28-AM-08_43_29

Home Index