Nuprl Definition : hdf-invariant
hdf-invariant(A;b.Q[b];X) == ∀L:A List. case X*(L) of inl(P) => ∀m:A. let X',b = P m in Q[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]
FDL editor aliases :
hdf-invariant
hdf-invariant(A;b.Q[b];X) ==
\mforall{}L:A List. case X*(L) of inl(P) => \mforall{}m:A. let X',b = P m in Q[b] | inr(z) => True
Date html generated:
2015_07_17-AM-08_05_10
Last ObjectModification:
2014_07_16-PM-07_21_36
Home
Index