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

is mentioned by

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

[s-effect-rule0]

Thm* x:Id, k:Knd, A,T:Type, f:(ATA). Thm* A  T  Feasible(ma-single-effect0(x;A;k;T;f))

[ma-single-effect0-feasible]

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