Def ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v))
Def == (with ds: x : T
Def == (init: x : c
Def == action a:T'
Def == aprecondition a(v) is
Def == as,v. P(s(x);v))

is mentioned by

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

[s-pre-init-rule1]

Def once(loc;a;i) Def == if loc = i Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);  Def == if [only members of [locl(a)] affect "done" :;  Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] Def == else nil fi

[once]

In prior sections: mb event system 6

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