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 in Q[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]
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