Def P & Q == PQ

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,m:, f:(nm), x1,x2:n, y1,y2:m. Thm* x1 = x2  y1 = y2 Thm*  Thm* (x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0) Thm*  Thm* sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)	[pair_support_double_sum]
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* k:, f:(kk). Thm* 0<k Thm*  Thm* Bij(k; k; f) Thm*  Thm* f(k-1) = k-1  f  (k-1)(k-1) & Bij((k-1); (k-1); f)	[bijection_restriction]
Def (P  Q)(L) == P(L) & Q(L)	[prop_and]
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 int 1 bool 1 int 2 fun 1 rel 1

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