Def M.ef(k,x,s,v,w)
Def == E != 1of(2of(2of(2of(2of(M)))))(<k,x>) ==> w = E(s,v)  M.ds(x)

is mentioned

In prior sections: mb event system 5

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html