Nuprl Lemma : parallel-class-program-compose2-eq

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


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 :  parallel-compose2-program-eq

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

Home Index