Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_sub_DASH_join_DASH

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
5	Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f \|\| g g f g	[fpf-sub-join-right]
cites the following:
3	Thm* 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]
4	Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x dom(f g) f g(x) = if x dom(f) f(x) else g(x) fi B(x)	[fpf-join-ap]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html