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

is mentioned by

Thm* 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]
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]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x  dom(f  g)  x  dom(f)  x  dom(g)	[fpf-join-dom2]
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]
Def ma-single-sends1(A; B; T; x; a; l; tg; f) Def == ma-single-sends(x : A; Def == ma-single-sends(a : B  rcv(l; tg) : T; Def == ma-single-sends(a; Def == ma-single-sends(l; Def == ma-single-sends([<tg,s,v. f(s(x),v)>])	[ma-single-sends1]
Def ma-single-effect1(x;A;y;B;k;T;f) Def == ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))	[ma-single-effect1]
Def M1 || M2 Def == M1 ||decl M2 Def == & 1of(2of(2of(M1))) || 1of(2of(2of(M2))) Def == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2)))) Def == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2))))) Def == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2)))))) Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of( Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2))))))) Def == & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-compatible]
Def M1  M2 Def == mk-ma(1of(M1)  1of(M2); Def == mk-ma(1of(2of(M1))  1of(2of(M2)); Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2))); Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2)))); Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of( Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2)))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2))))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))	[ma-join]

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