Nuprl Lemma : pv11_p1_valid-p1b-message_wf

[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E.
    ((header(e) ``pv11_p1 p1b`` ∈ Name)  (pv11_p1_valid-p1b-message(Cmd;es;e;f) ∈ ℙ))


Proof




Definitions occuring in Statement :  pv11_p1_valid-p1b-message: pv11_p1_valid-p1b-message(Cmd;es;e;f) pv11_p1_headers_type: pv11_p1_headers_type{i:l}(Cmd) es-header: header(e) Message: Message(f) event-ordering+: EO+(Info) es-E: E name: Name cons: [a b] nil: [] valueall-type: valueall-type(T) uall: [x:A]. B[x] prop: all: x:A. B[x] implies:  Q member: t ∈ T set: {x:A| B[x]}  token: "$token" universe: Type equal: t ∈ T
Lemmas :  sq_stable__and equal_wf cons_wf_listp nil_wf listp_wf vatype_wf cons_wf pv11_p1_Ballot_Num_wf list_wf equal-wf-T-base Id_wf sq_stable__equal squash_wf int_seg_wf length_wf name_wf pv11_p1_headers_wf l_all_iff l_member_wf pv11_p1_headers_fun_wf cons_member equal-wf-base iff_weakening_equal subtype_rel-equal pv11_p1_valid-proposals_wf map_wf es-header_wf es-E_wf event-ordering+_subtype event-ordering+_wf Message_wf subtype_rel_dep_function pv11_p1_headers_type_wf set_wf valueall-type_wf

Latex:
\mforall{}[Cmd:\{T:Type|  valueall-type(T)\}  ]
    \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.
        ((header(e)  =  ``pv11\_p1  p1b``)  {}\mRightarrow{}  (pv11\_p1\_valid-p1b-message(Cmd;es;e;f)  \mmember{}  \mBbbP{}))



Date html generated: 2015_07_23-PM-05_03_43
Last ObjectModification: 2015_02_04-AM-07_50_46

Home Index