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

  ∀[Xpr1,Xpr2,Ypr1,Ypr2:Id ─→ hdataflow(Info;B)].
    (Xpr1 || Ypr1 Xpr2 || Ypr2 ∈ (Id ─→ hdataflow(Info;B))) supposing 
       ((Xpr1 Xpr2 ∈ (Id ─→ hdataflow(Info;B))) and 
       (Ypr1 Ypr2 ∈ (Id ─→ hdataflow(Info;B)))) 
  supposing valueall-type(B)


Definitions occuring in Statement :  parallel-class-program: || Y 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 :  and_wf equal_wf Id_wf hdataflow_wf hdf-parallel_wf valueall-type_wf

    \mforall{}[Xpr1,Xpr2,Ypr1,Ypr2:Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (Xpr1  ||  Ypr1  =  Xpr2  ||  Ypr2)  supposing  ((Xpr1  =  Xpr2)  and  (Ypr1  =  Ypr2)) 
    supposing  valueall-type(B)

Date html generated: 2015_07_22-PM-00_03_56
Last ObjectModification: 2015_01_28-AM-09_53_07

Home Index