Nuprl Lemma : parallel-bind-program-eq

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


Definitions occuring in Statement :  parallel-class-program: || Y bind-class-program: xpr >>ypr Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T hdataflow: hdataflow(A;B)
Lemmas :  local-class-equality bind-class_wf parallel-class_wf hdataflow-class_wf sq_exists_subtype_rel Id_wf hdataflow_wf all_wf es-E_wf event-ordering+_subtype equal_wf bag_wf class-ap_wf hdf-ap_wf iterate-hdataflow_wf es-loc_wf map_wf es-info_wf es-before_wf squash_wf true_wf eclass_wf event-ordering+_wf parallel-class-bind-left iff_weakening_equal bind-class-program_wf parallel-class-program_wf hdf-parallel-bind-halt-eq list_wf valueall-type_wf pi2_wf

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

Date html generated: 2015_07_22-PM-00_05_53
Last ObjectModification: 2015_02_04-PM-05_10_38

Home Index