mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)

is mentioned by

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top, x1:Id, k1:Knd,
Thm* d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm* 
Thm* da || d2
Thm* 
Thm* <k,x> = <k1,x1>
Thm* 
Thm* ma-single-effect(ds; da; k; x; f) ||+ ma-single-effect(d1; d2; k1; x1; f1)		[ma-single-effect-ma-single-effect-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* k1:Knd, l1:IdLnk, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:(IdTop) List.
Thm* ds || d1
Thm* 
Thm* da || d2
Thm* 
Thm* <k,l> = <k1,l1>
Thm* 
Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-sends(d1; d2; k1; l1; f1)		[ma-single-sends-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm* 
Thm* da || d2
Thm* 
Thm* ma-single-effect(d1; d2; k1; x; f1) ||+ ma-single-sends(ds; da; k; l; f)		[ma-single-effect-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List,
Thm* x:Id, k1:Knd, d1:x:Id fp-> Type, d2:a:Knd fp-> Type, f1:Top.
Thm* ds || d1
Thm* 
Thm* da || d2
Thm* 
Thm* ma-single-sends(ds; da; k; l; f) ||+ ma-single-effect(d1; d2; k1; x; f1)		[ma-single-sends-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, k:Knd, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* ma-single-effect(d1; da; k; x; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v)		[ma-single-effect-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* ma-single-sends(d1; da; k; l; f) ||+ (with ds: ds
Thm* maction a:T
Thm* mprecondition a(v) is
Thm* mP s v)		[ma-single-sends-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, k:Knd, l:IdLnk, d1:x:Id fp-> Type,
Thm* da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* (with ds: ds
Thm* (action a:T
Thm* (precondition a(v) is
Thm* (P s v) ||+ ma-single-sends(d1; da; k; l; f)		[ma-single-pre-ma-single-sends-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, k:Knd,
Thm* d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:Top.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-effect(d1; da; k; x; f)		[ma-single-pre-init-ma-single-effect-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, k:Knd,
Thm* l:IdLnk, d1:x:Id fp-> Type, da:a:Knd fp-> Type, f:(IdTop) List.
Thm* ds || d1
Thm* 
Thm* locl(a) : T || da
Thm* 
Thm* (with ds: ds
Thm* (init: init
Thm* action a:T
Thm* aprecondition a(v) is
Thm* aP) ||+ ma-single-sends(d1; da; k; l; f)		[ma-single-pre-init-ma-single-sends-compatible]

In prior sections: mb event system 5 mb event system 6 mb event system 2 mb event system 4

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

mb event system 7 Sections EventSystems Doc