Def ma-single-effect1(x;A;y;B;k;T;f)
Def == ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))

is mentioned by

Thm* i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA). Thm* y = x Thm*  Thm* @i: ma-single-effect1(x;A;y;B;k;T;f)  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-effect1(x;A;y;B;k;T;f)  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k  Knd  (valtype(e) r T)) 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((x when e),(y when e),val(e))  A))

[effect-rule1]

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