Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* k:, P:(k). Thm* ((i:k. P(i))  0<search(k;P)) Thm* & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))	[search_property]
Thm* f:(TT), m:(T). Thm* (x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)) Thm*  Thm* (x:T. n:. f(f^n(x)) = f^n(x))	[iteration_terminates]
Thm* n,k:, c:(nk). Thm* p:(k( List)).  Thm* sum(||p(j)|| | j < k) = n Thm* & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]) Thm* & (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)	[finite-partition]
Thm* m:, P:(mProp). Thm* (i:m. Dec(P(i))) Thm*  Thm* (n,k:, f:(nm), g:(km). Thm* (increasing(f;n) Thm* (& increasing(g;k) Thm* (& (i:n. P(f(i))) Thm* (& (j:k. P(g(j))) Thm* (& (i:m. (j:n. i = f(j))  (j:k. i = g(j))))	[increasing_split]
Thm* m,n,k:, f:(nm), g:(km). Thm* increasing(f;n) Thm*  Thm* increasing(g;k) Thm*  Thm* (i:m. (j:n. i = f(j))  (j:k. i = g(j))) Thm*  Thm* (j1:n, j2:k. f(j1) = g(j2))  m = n+k	[disjoint_increasing_onto]
Thm* k,m:. (f:(km). Inj(k; m; f))  km	[injection_le]
Thm* k,m:. (f:(km). increasing(f;k))  km	[increasing_le]
Def (R^*)(x,y) == n:. x R^n y	[rel_star]
Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)	[rel_exp]

In prior sections: core fun 1 int 2

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