Nuprl Definition : hdf-single-val-step

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

Definitions occuring in Statement :  all: x:A. B[x] and: P ∧ Q 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-val-step

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

Date html generated: 2016_05_16-AM-10_40_18
Last ObjectModification: 2012_11_23-PM-02_09_41

Theory : halting!dataflow

Home Index