Def d-single-effect(i; ds; da; k; x; f)(j)
Def == if eqof(IdDeq)(j,i) ma-single-effect(ds; da; k; x; f) else  fi

is mentioned by

Thm* i,x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* d-single-effect(i; ds; da; k; x; f)  Thm* realizes es.(x:Id. vartype(i;x) r ds(x)?Top) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e)))) Thm* realizes es.& (e:E.  Thm* realizes es.& (loc(e) = i  Id Thm* realizes es.& ( Thm* realizes es.& (kind(e) = k  Knd Thm* realizes es.& ( Thm* realizes es.& ((x after e) = f((z.(z when e)),val(e))  ds(x)?Top)

[effect-rule]

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