Nuprl Lemma : data-stream_wf

[A,B:Type]. ∀[L:A List]. ∀[P:dataflow(A;B)].  (data-stream(P;L) ∈ List)


Proof




Definitions occuring in Statement :  data-stream: data-stream(P;L) dataflow: dataflow(A;B) list: List uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf dataflow_wf equal-wf-T-base colength_wf_list list-cases nil_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 length_of_cons_lemma map_wf int_seg_wf length_wf dataflow-ap_wf iterate-dataflow_wf firstn_wf cons_wf select_wf length_cons non_neg_length length_wf_nat upto_wf list_wf

Latex:
\mforall{}[A,B:Type].  \mforall{}[L:A  List].  \mforall{}[P:dataflow(A;B)].    (data-stream(P;L)  \mmember{}  B  List)



Date html generated: 2015_07_23-AM-11_05_56
Last ObjectModification: 2015_01_29-AM-00_11_48

Home Index