Def M1  M2
Def == mk-ma(1of(M1)  1of(M2);
Def == mk-ma(1of(2of(M1))  1of(2of(M2));
Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2)));
Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2))));
Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2)))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2))))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2)))))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))

is mentioned by

Thm* A,B:MsgAForm, ltg:(IdLnkIdType), i:Id. Thm* (ltg  ma-outlinks(A  B;i)) Thm*  Thm* (ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i))	[ma-outlinks-join]
Thm* A,B:MsgAForm. A  B  MsgAForm	[msg-form-join]
Thm* A,B,C:MsgA. A ||+ B  C ||+ A  C ||+ B  C ||+ A  B	[ma-compat-join]
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