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))


Proof




Definitions occuring in Statement :  hdf-parallel: || Y hdf-compose2: Y hdataflow: hdataflow(A;B) 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)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a squash: T parallel-class-program: || Y eclass2-program: Xpr Ypr mkid: "$x" Id: Id prop:

Latex:
\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: 2016_05_17-AM-09_12_22
Last ObjectModification: 2016_01_17-PM-09_11_51

Theory : local!classes


Home Index