mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ma-sframe-compatible(A; B)
Def == kl:(KndIdLnk), tg:Id.
Def == (kl  dom(1of(2of(2of(2of(2of(2of(A)))))))
Def == (
Def == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl)))
Def == (
Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A)))))))))
Def == (
Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B)))))))))
Def == (
Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of(
Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>)))
Def == & (kl  dom(1of(2of(2of(2of(2of(2of(B)))))))
Def == & (
Def == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl)))
Def == & (
Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B)))))))))
Def == & (
Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A)))))))))
Def == & (
Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of(
Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))

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-sframe-compatible(; A)[ma-empty-sframe-compatible-left]
Thm* A:MsgA. ma-sframe-compatible(A; )[ma-empty-sframe-compatible-right]

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