Def ma-is-empty(M)
Def == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M)))
Def == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M)))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(M))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(M)))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M))))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M)))))))))

is mentioned by

Thm* A,B:MsgA. ma-is-empty(A)  A  B	[ma-is-empty-sub]
Thm* ma-is-empty()	[ma-empty-is-empty]
Thm* M:MsgA. ma-is-empty(M)  M =   MsgA	[assert-ma-is-empty]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html