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

  ∀[xpr1,xpr2:Id ─→ hdataflow(Info;A)]. ∀[ypr1,ypr2:A ─→ Id ─→ hdataflow(Info;B)].
    (xpr1 >>ypr1 xpr2 >>ypr2 ∈ (Id ─→ hdataflow(Info;B))) supposing 
       ((xpr1 xpr2 ∈ (Id ─→ hdataflow(Info;A))) and 
       (ypr1 ypr2 ∈ (A ─→ Id ─→ hdataflow(Info;B)))) 
  supposing valueall-type(B)


Definitions occuring in Statement :  bind-class-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 hdataflow: hdataflow(A;B)
Lemmas :  hdf-bind_wf and_wf equal_wf Id_wf hdataflow_wf valueall-type_wf

    \mforall{}[xpr1,xpr2:Id  {}\mrightarrow{}  hdataflow(Info;A)].  \mforall{}[ypr1,ypr2:A  {}\mrightarrow{}  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_02_47
Last ObjectModification: 2015_01_28-AM-09_53_39

Home Index