Nuprl Lemma : eclass0-bag-program_wf

[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[F:Id ─→ bag(B) ─→ bag(C)]. ∀[Xpr:LocalClass(X)].
  (eclass0-bag-program(F;Xpr) ∈ LocalClass(eclass0-bag(F;X))) supposing 
     ((∀i:Id. ((F {}) {} ∈ bag(C))) and 


Definitions occuring in Statement :  eclass0-bag-program: eclass0-bag-program(f;pr) eclass0-bag: eclass0-bag(f;X) local-class: LocalClass(X) eclass: EClass(A[eo; e]) Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T apply: a function: x:A ─→ B[x] universe: Type equal: t ∈ T empty-bag: {} bag: bag(T)
Lemmas :  hdf-compose0-bag_wf es-E_wf event-ordering+_subtype all_wf equal_wf bag_wf class-ap_wf eclass0-bag_wf hdf-ap_wf iterate-hdataflow_wf es-loc_wf map_wf es-info_wf es-before_wf hdataflow_wf Id_wf equal-wf-T-base empty-bag_wf valueall-type_wf local-class_wf eclass_wf event-ordering+_wf iff_weakening_equal list_wf list_induction hdataflow-ext unit_wf2 iter_hdf_nil_lemma valueall-type-has-valueall bag-valueall-type evalall-reduce iter_hdf_cons_lemma subtype_rel_list top_wf iterate-hdf-halt

\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[F:Id  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)].  \mforall{}[Xpr:LocalClass(X)].
    (eclass0-bag-program(F;Xpr)  \mmember{}  LocalClass(eclass0-bag(F;X)))  supposing 
          ((\mforall{}i:Id.  ((F  i  \{\})  =  \{\}))  and 

Date html generated: 2015_07_22-PM-00_01_56
Last ObjectModification: 2015_02_04-PM-05_11_00

Home Index