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 not otherwise mentioned in this or prior sections.

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html