Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>

is mentioned by

Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg  da-outlinks(da1  da2;i)) Thm*  Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))	[da-outlinks-join]
Thm* eq:EqDecider(T), f,g,h:x:T fp-> Type. Thm* f || g Thm*  Thm* h || f Thm*  Thm* h || g Thm*  Thm* g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g	[fpf-compatible-triple]
Thm* eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. Thm* ydom(f). w=f(y)   P(y,w) Thm*  Thm* ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)	[fpf-all-join-decl]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* f || h  g || h  f  g || h	[fpf-compatible-join2]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* h || f  h || g  h || f  g	[fpf-compatible-join]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g	[fpf-sub-join-right]
Thm* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). Thm* f  f  g	[fpf-sub-join-left]
Thm* 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]
Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. Thm* x  dom(f)  f  g(x) = f(x)  B(x)	[fpf-join-ap-left]
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]

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