mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def M1  M2
Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2))
Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2)))
Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2))))
Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2)))))
Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2))))))
Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(
Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2)))))))
Def == & & 1of(2of(2of(2of(2of(2of(2of(2of(
Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))

is mentioned by

Thm* M1,M2:MsgA.
Thm* M1  M2
Thm* 
Thm* (k:Knd, l:IdLnk, tg:Id.
Thm* (M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>))		[ma-sframe-sub]
Thm* M1,M2:MsgA.
Thm* M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x))		[ma-frame-sub]
Thm* M1,M2:MsgA.
Thm* M1  M2
Thm* 
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg))
Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List.
Thm* (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))		[ma-send-sub]
Thm* M1,M2:MsgA.
Thm* M1  M2
Thm* 
Thm* (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
Thm* (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w))		[ma-ef-sub]
Thm* M1,M2:MsgA.
Thm* M1  M2
Thm* 
Thm* (a:Id, s:M2.state.
Thm* (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s))		[ma-npre-sub]
Thm* M1,M2:MsgA. M1  M2  (a:Id. a declared in M1  a declared in M2)[ma-decla-sub]
Thm* M1,M2:MsgA.
Thm* M1  M2
Thm* 
Thm* (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v))		[ma-pre-sub]
Thm* V:(IdType), M1,M2:MsgA.
Thm* (x:Id. V(x) r M2.ds(x))
Thm* 
Thm* M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v))		[ma-init-sub]
Thm* M1,M2:MsgA, k:Knd. M1  M2  (M2.da(k) r M1.da(k))[ma-da-sub]
Thm* M1,M2:MsgA, x:Id. M1  M2  (M2.ds(x) r M1.ds(x))[ma-ds-sub]
Thm* M1,M2:MsgA. M1 || M2  M2  M1  M2[ma-sub-join-right]
Thm* M1,M2:MsgA. M1  M1  M2[ma-sub-join-left]
Thm* A,B:MsgA. ma-is-empty(A)  A  B[ma-is-empty-sub]
Thm* M:MsgA.   M[ma-empty-sub]
Thm* M1,M2:MsgA. M1 = M2  M1  M2[ma-sub_weakening]
Thm* M1,M2,M3:MsgA. M1  M2  M2  M3  M1  M3[ma-sub_transitivity]
Def D1  D2 == i:Id. M(i)  M(i)[d-sub]

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

mb event system 5 Sections EventSystems Doc