Nuprl Definition : hdf-single-val-step
hdf-single-val-step(P;X;A;B) == case X of inl(p) => ∀a:A. let X',b = p a in single-valued-bag(b;B) ∧ P | inr(z) => True
Definitions occuring in Statement :
all: ∀x:A. B[x],
and: P ∧ Q,
true: True,
apply: f a,
spread: spread def,
decide: case b 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:
2015_07_17-AM-08_05_50
Last ObjectModification:
2012_11_23-PM-02_09_41
Home
Index