Def ma-single-pre1(x;A;a;T;y,v.P(y;v))
Def == (with ds: x : A
Def == (action a:T
Def == (precondition a(v) is
Def == (s,v. P(s(x);v) s v)

is mentioned by

Thm* i,a,x:Id, A,T:Type, P:(ATProp). Thm* @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  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) = locl(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) = locl(a)  Knd  P((x when e),val(e))) Thm* & (realizes es.& (& (e':E.  Thm* & (realizes es.& (& ((e <loc e')  e = e'  E Thm* & (realizes es.& (& (& kind(e') = locl(a)  Knd Thm* & (realizes es.& (& (&  (v:T. P((x after e'),v)))))

[s-pre-rule1]

Thm* a:Id, T,A:Type, x:Id, P:(ATProp). Thm* T Thm*  Thm* A Thm*  Thm* (a:A. Dec(v:T. P(a,v)))  Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))

[ma-single-pre1-feasible]

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