mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
4Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi		[fpf-join-cap-sq]
cites the following:
3Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x  dom(f  g)  x  dom(f)  x  dom(g)		[fpf-join-dom]
0Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi		[fpf-join-ap-sq]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 5 Sections EventSystems Doc