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* M1,M2:MsgA. M1 || M2  M2  M1  M2	[ma-sub-join-right]
Thm* M1,M2:MsgA. M1  M1  M2	[ma-sub-join-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