is mentioned by

Thm* a:Id, T,A:Type, x:Id, P:(ATProp). Thm* ma-single-pre1(x;A;a;T;x,v.P(x,v))  MsgA	[ma-single-pre1_wf]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* (with ds: ds action a:T precondition a(v) is P s v)  MsgA	[ma-single-pre_wf]
Thm* M1,M2:MsgA. M1 || M2  Prop{i'}	[ma-compatible_wf]
Thm* M1,M2:MsgA. M1  M2  Prop{i'}	[ma-sub_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>)  Prop	[ma-sframe_wf]
Thm* M:MsgA, k:Knd, x:Id. M.frame(k affects x)  Prop	[ma-frame_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg)) Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List. Thm* M.send(k;l;s;v;ms;i)  Prop	[ma-send_wf]
Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). Thm* M.ef(k,x,s,v,w)  Prop	[ma-ef_wf]
Thm* M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v)  Prop	[ma-pre_wf]
Thm* M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s)  Prop	[ma-npre_wf]
Thm* M:MsgA, x:Id, v:M.ds(x). M.init(x,v)  Prop	[ma-init_wf]
Thm* M:MsgA, a:Id. a declared in M  Prop	[ma-decla_wf]
Thm* eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. Thm* ydom(f). w=f(y)   P(y,w) Thm*  Thm* ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)	[fpf-all-join-decl]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, Thm* P:(a:{a:A| a  dom(f) }B(a)Prop). z != f(x) ==> P(x,z)  Prop	[fpf-val_wf]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 mb basic rel 1 mb nat mb list 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 4

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