Nuprl Lemma : parallel-compose2-program-eq

[Info,B,C:Type]. ∀[X1,X2:Id ─→ hdataflow(Info;B ─→ bag(C))]. ∀[X:Id ─→ hdataflow(Info;B)].
  (X1 || X2 X1 || X2 X ∈ (Id ─→ hdataflow(Info;C))) supposing 
     (valueall-type(C) and 
     valueall-type(B) and 


Definitions occuring in Statement :  parallel-class-program: || Y eclass2-program: Xpr Ypr Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] squash: T function: x:A ─→ B[x] universe: Type equal: t ∈ T bag: bag(T) hdataflow: hdataflow(A;B)
Lemmas :  bag-value-type local-class-equality eclass2_wf parallel-class_wf bag_wf hdataflow-class_wf parallel-class-program_wf eclass2-program_wf pi2_wf hdataflow_wf hdf-ap_wf iterate-hdataflow_wf es-loc_wf event-ordering+_subtype map_wf es-E_wf es-info_wf es-before_wf event-ordering+_wf all_wf equal_wf class-ap_wf sq_exists_subtype_rel Id_wf iff_weakening_equal squash_wf true_wf eclass_wf parallel-eclass2-left function-valueall-type list_wf valueall-type_wf bool_wf hdf-compose2_wf hdf-parallel_wf hdf-halted_wf eqtt_to_assert bor_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_imp_equal_bool btrue_wf assert_wf or_wf iff_transitivity iff_weakening_uiff assert_of_band assert_of_bor iff_wf hdf-parallel-halted band_wf hdf-halted-compose2-iterate

\mforall{}[Info,B,C:Type].  \mforall{}[X1,X2:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X:Id  {}\mrightarrow{}  hdataflow(Info;B)].
    (X1  o  X  ||  X2  o  X  =  X1  ||  X2  o  X)  supposing  (valueall-type(C)  and  valueall-type(B)  and  (\mdownarrow{}B))

Date html generated: 2015_07_22-PM-00_03_53
Last ObjectModification: 2015_02_04-PM-05_10_30

Home Index