Nuprl Lemma : Process-stream_wf

[M:Type ─→ Type]
  ∀[msgs:pMsg(P.M[P]) List]. ∀[P:Process(P.M[P])].  (Process-stream(P;msgs) ∈ pExt(P.M[P]) List) 
  supposing Continuous+(P.M[P])


Proof




Definitions occuring in Statement :  Process-stream: Process-stream(P;msgs) pExt: pExt(P.M[P]) pMsg: pMsg(P.M[P]) Process: Process(P.M[P]) list: List strong-type-continuous: Continuous+(T.F[T]) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf Process_wf equal-wf-T-base colength_wf_list list-cases data_stream_nil_lemma nil_wf pExt_wf product_subtype_list spread_cons_lemma sq_stable__le le_antisymmetry_iff add_functionality_wrt_le add-associates add-zero zero-add le-add-cancel nat_wf decidable__le false_wf not-le-2 condition-implies-le minus-add minus-one-mul add-commutes le_wf subtract_wf not-ge-2 less-iff-le minus-minus add-swap subtype_base_sq set_subtype_base int_subtype_base data-stream-cons subtype_rel_list top_wf list_wf pMsg_wf strong-type-continuous_wf cons_wf Process-apply_wf

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[msgs:pMsg(P.M[P])  List].  \mforall{}[P:Process(P.M[P])].    (Process-stream(P;msgs)  \mmember{}  pExt(P.M[P])  List) 
    supposing  Continuous+(P.M[P])



Date html generated: 2015_07_23-AM-11_07_24
Last ObjectModification: 2015_01_29-AM-00_10_28

Home Index