Nuprl Lemma : state-class1-program-wf-hdf

[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[pr:Id ─→ hdataflow(Info;A)].
  (state-class1-program(init;f;pr) ∈ Id ─→ hdataflow(Info;B)) supposing (valueall-type(B) and (↓B))


Definitions occuring in Statement :  state-class1-program: state-class1-program(init;tr;pr) Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] squash: T member: t ∈ T function: x:A ─→ B[x] universe: Type hdataflow: hdataflow(A;B)
Lemmas :  loop-class-state-program-wf-hdf single-bag_wf eclass1-program-wf-hdf function-valueall-type valueall-type-value-type valueall-type_wf squash_wf Id_wf hdataflow_wf

\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;A)].
    (state-class1-program(init;f;pr)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B))  supposing  (valueall-type(B)  and  (\mdownarrow{}B))

Date html generated: 2015_07_22-PM-00_05_10
Last ObjectModification: 2015_01_28-AM-09_53_20

Home Index