Nuprl Lemma : iterate-hdf-buffer-simple

[A,B:Type]. ∀[X:hdataflow(A;B ─→ bag(B))]. ∀[bs:bag(B)].
  ∀[L:A List]. ∀[a:A].  ((snd(hdf-buffer(X;bs)*(L)(a))) (snd(simple-hdf-buffer(X;bs)*(L)(a))) ∈ bag(B)) 
  supposing valueall-type(B)


Proof




Definitions occuring in Statement :  hdf-buffer: hdf-buffer(X;bs) simple-hdf-buffer: simple-hdf-buffer(X;bs) iterate-hdataflow: P*(inputs) hdf-ap: X(a) hdataflow: hdataflow(A;B) list: List valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] pi2: snd(t) function: x:A ─→ B[x] universe: Type equal: t ∈ T bag: bag(T)
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf bag_wf equal-wf-T-base colength_wf_list list-cases iter_hdf_nil_lemma 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 iter_hdf_cons_lemma nil_wf list-subtype-bag
\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  bag(B))].  \mforall{}[bs:bag(B)].
    \mforall{}[L:A  List].  \mforall{}[a:A].    ((snd(hdf-buffer(X;bs)*(L)(a)))  =  (snd(simple-hdf-buffer(X;bs)*(L)(a)))) 
    supposing  valueall-type(B)



Date html generated: 2015_07_17-AM-08_07_55
Last ObjectModification: 2015_01_27-PM-00_07_34

Home Index