Who Cites fpf-join?
fpf-join	Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)>
fpf-cap	Def f(x)?z == if x  dom(f) f(x) else z fi
fpf-ap	Def f(x) == 2of(f)(x)
fpf-dom	Def x  dom(f) == deq-member(eq;x;1of(f))
deq-member	Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L)
eqof	Def eqof(d) == 1of(d)
	Thm* T:Type, d:EqDecider(T). eqof(d)  TT
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A
bnot	Def b == if b false else true fi
	Thm* b:. b
filter	Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l)
	Thm* T:Type, P:(T), l:T List. filter(P;l)  T List
append	Def as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
	Thm* T:Type, as,bs:T List. (as @ bs)  T List
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))
reduce	Def reduce(f;k;as) == Case of as; nil  k ; a.as'  f(a,reduce(f;k;as')) Def (recursive)
	Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as)  B
bor	Def p  q == if p true else q fi
	Thm* p,q:. (p  q)

Syntax:

f  g

has structure:

fpf-join(eq; f; g)

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