mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def M1 || M2
Def == M1 ||decl 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* 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]

In prior sections: mb event system 5 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