Nuprl Lemma : eclass2-program-eq-hdf

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


Definitions occuring in Statement :  eclass2-program: Xpr Ypr 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 bag: bag(T) hdataflow: hdataflow(A;B)
Lemmas :  and_wf equal_wf Id_wf hdataflow_wf bag_wf hdf-compose2_wf valueall-type_wf

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

Date html generated: 2015_07_22-PM-00_01_49
Last ObjectModification: 2015_01_28-AM-09_53_50

Home Index