mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ma-frame-compatible(A; B)
Def == kx:(KndId). 
Def == (kx  dom(1of(2of(2of(2of(2of(A))))))
Def == (
Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == (
Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == (
Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx))))
Def == & (kx  dom(1of(2of(2of(2of(2of(B))))))
Def == & (
Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == & (
Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == & (
Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))

is mentioned by

Thm* A,B:MsgA.
Thm* A || B
Thm* 
Thm* ma-frame-compatible(A; B)
Thm* 
Thm* ma-sframe-compatible(A; B)  Feasible(A)  Feasible(B)  Feasible(A  B)		[ma-join-feasible]
Thm* A,B,C:MsgA.
Thm* A || B
Thm* 
Thm* ma-frame-compatible(A; B)
Thm* 
Thm* ma-sframe-compatible(A; B)
Thm* 
Thm* C || A
Thm* 
Thm* ma-frame-compatible(C; A)
Thm* 
Thm* ma-sframe-compatible(C; A)
Thm* 
Thm* C || B
Thm* 
Thm* ma-frame-compatible(C; B)
Thm* 
Thm* ma-sframe-compatible(C; B)
Thm* 
Thm* C || A  B & ma-frame-compatible(C; A  B) & ma-sframe-compatible(C; A  B)		[ma-compatible-join]
Thm* A:MsgA. ma-frame-compatible(A; )[ma-empty-frame-compatible-right]
Thm* A:MsgA. ma-frame-compatible(; A)[ma-empty-frame-compatible-left]

In prior sections: 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 6 Sections EventSystems Doc