is mentioned by

Thm* eq,x,v:Top. x : v(x) ~ v	[fpf-ap-single]
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]
Def ma-sframe-compatible(A; B) Def == kl:(KndIdLnk), tg:Id. Def == (kl  dom(1of(2of(2of(2of(2of(2of(A))))))) Def == ( Def == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == ( Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == ( Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>))) Def == & (kl  dom(1of(2of(2of(2of(2of(2of(B))))))) Def == & ( Def == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == & ( Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))	[ma-sframe-compatible]
Def ma-frame-compatible(A; B) Def == kx:(KndId).  Def == (kx  dom(1of(2of(2of(2of(2of(A)))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == ( Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == ( Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx)))) Def == & (kx  dom(1of(2of(2of(2of(2of(B)))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == & ( Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))	[ma-frame-compatible]
Def da-outlink-f(da;k) == <lnk(k),tag(k),da(k)>	[da-outlink-f]
Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))	[fpf-all]
Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>	[fpf-join]
Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)	[fpf-compatible]

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