Nuprl Definition : hdf-single-valued

hdf-single-valued(X;A;B) ==
  ∀L:A List. case X*(L) of inl(P) => ∀a:A. let X',b in single-valued-bag(b;B) inr(z) => True

Definitions occuring in Statement :  iterate-hdataflow: P*(inputs) list: List all: x:A. B[x] true: True apply: a spread: spread def decide: case of inl(x) => s[x] inr(y) => t[y] single-valued-bag: single-valued-bag(b;T)
FDL editor aliases :  hdf-single-valued

hdf-single-valued(X;A;B)  ==
    \mforall{}L:A  List.  case  X*(L)  of  inl(P)  =>  \mforall{}a:A.  let  X',b  =  P  a  in  single-valued-bag(b;B)  |  inr(z)  =>  True

Date html generated: 2016_05_16-AM-10_40_23
Last ObjectModification: 2012_11_23-PM-02_09_42

Theory : halting!dataflow

Home Index