Nuprl Lemma : eclass2-program-wf-hdf
∀[Info,B,C:Type].
  ∀[Xpr:Id ⟶ hdataflow(Info;B ⟶ bag(C))]. ∀[Ypr:Id ⟶ hdataflow(Info;B)].  (Xpr o Ypr ∈ Id ⟶ hdataflow(Info;C)) 
  supposing valueall-type(C)
Proof
Definitions occuring in Statement : 
eclass2-program: Xpr o Ypr
, 
hdataflow: hdataflow(A;B)
, 
Id: Id
, 
valueall-type: valueall-type(T)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
bag: bag(T)
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
eclass2-program: Xpr o Ypr
Latex:
\mforall{}[Info,B,C:Type].
    \mforall{}[Xpr:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  bag(C))].  \mforall{}[Ypr:Id  {}\mrightarrow{}  hdataflow(Info;B)].
        (Xpr  o  Ypr  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;C)) 
    supposing  valueall-type(C)
Date html generated:
2016_05_17-AM-09_04_51
Last ObjectModification:
2015_12_29-PM-03_36_44
Theory : local!classes
Home
Index