Nuprl Lemma : parallel-bind-program-eq-gen

[Info,B1,B2,C:Type]. ∀[X1:Id ─→ hdataflow(Info;B1)]. ∀[X2:Id ─→ hdataflow(Info;B2)].
[Y1:B1 ─→ Id ─→ hdataflow(Info;C)]. ∀[Y2:B2 ─→ Id ─→ hdataflow(Info;C)].
  (X1 >>Y1 || X2 >>Y2
     X1 X2 >>= λ of inl(b1) => Y1 b1 inr(b2) => Y2 b2
     ∈ (Id ─→ hdataflow(Info;C))) supposing 
     (valueall-type(C) and 
     valueall-type(B1) and 


Definitions occuring in Statement :  eclass-disju-program: xpr ypr parallel-class-program: || Y bind-class-program: xpr >>ypr Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ─→ B[x] decide: case of inl(x) => s[x] inr(y) => t[y] universe: Type equal: t ∈ T hdataflow: hdataflow(A;B)
Lemmas :  local-class-equality bind-class_wf eclass-disju_wf hdataflow-class_wf parallel-class-program_wf bind-class-program_wf pi2_wf hdataflow_wf bag_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 parallel-class_wf squash_wf true_wf eclass_wf eclass-disju-bind-left iff_weakening_equal eclass-disju-program_wf list_wf valueall-type_wf bool_wf hdf-halted_wf hdf-parallel_wf hdf-bind_wf hdf-parallel-bind-halt-eq-gen hdf-union_wf lifting-apply-decide hdf-union-eq-disju

\mforall{}[Info,B1,B2,C:Type].  \mforall{}[X1:Id  {}\mrightarrow{}  hdataflow(Info;B1)].  \mforall{}[X2:Id  {}\mrightarrow{}  hdataflow(Info;B2)].
\mforall{}[Y1:B1  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)].  \mforall{}[Y2:B2  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)].
    (X1  >>=  Y1  ||  X2  >>=  Y2  =  X1  +  X2  >>=  \mlambda{}  b  of  inl(b1)  =>  Y1  b1  |  inr(b2)  =>  Y2  b2)  supposing 
          (valueall-type(C)  and 
          valueall-type(B1)  and 

Date html generated: 2015_07_22-PM-00_05_55
Last ObjectModification: 2015_02_04-PM-05_10_43

Home Index