Def fpf-is-empty(f) == ||1of(f)||=0

is mentioned by

Thm* eq:EqDecider(A), f,g:x:A fp-> Top. Thm* fpf-is-empty(f  g) ~ (fpf-is-empty(f)fpf-is-empty(g))	[fpf-join-is-empty]
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)))))))))	[ma-is-empty]

In prior sections: mb event system 3

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