Nuprl Lemma : loop-class-state-program-wf-hdf
∀[Info,B:Type].
  ∀[init:Id ⟶ bag(B)]. ∀[pr:Id ⟶ hdataflow(Info;B ⟶ B)].
    (loop-class-state-program(pr;init) ∈ Id ⟶ hdataflow(Info;B)) 
  supposing valueall-type(B)
Proof
Definitions occuring in Statement : 
loop-class-state-program: loop-class-state-program(pr;init)
, 
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
, 
loop-class-state-program: loop-class-state-program(pr;init)
Latex:
\mforall{}[Info,B:Type].
    \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  B)].
        (loop-class-state-program(pr;init)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B)) 
    supposing  valueall-type(B)
Date html generated:
2016_05_17-AM-09_07_31
Last ObjectModification:
2015_12_29-PM-03_36_03
Theory : local!classes
Home
Index