Nuprl Lemma : hdf-parallel-compose-eq

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


Definitions occuring in Statement :  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) hdf-parallel: || Y hdf-compose2: Y hdataflow: hdataflow(A;B)
Lemmas :  parallel-compose2-program-eq Id_wf hdataflow_wf valueall-type_wf squash_wf bag_wf

\mforall{}[A,B,C:Type].  \mforall{}[X1,X2:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X:hdataflow(A;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_05_57
Last ObjectModification: 2015_01_28-AM-09_52_16

Home Index