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 = P a in single-valued-bag(b;B) | inr(z) => True
Definitions occuring in Statement :
iterate-hdataflow: P*(inputs),
list: T List,
all: ∀x:A. B[x],
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-valued
Latex:
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