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

is mentioned by

Thm* P,Q:(TProp), R:(TTProp). Thm* R preserves P  R preserves Q  R preserves P  Q	[and_preserved_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* k:, x,y,i:k. (y, x)((y, x)(i)) = i	[flip_twice]
Thm* k:, x,y:k. (y, x) o (y, x) = (x.x)	[flip_inverse]
Thm* k:, i,j:k. Bij(k; k; (i, j))	[flip_bijection]
Thm* k:, i,j:k. (i, j) = (j, i)	[flip_symmetry]
Thm* n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)	[sum_switch]
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* f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x)	[fun_exp_add1_sub]
Thm* f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)	[fun_exp_add1]
Thm* n,m:, f:(TT). f^n+m = f^n o f^m	[fun_exp_add]
Thm* n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)	[fun_exp_compose]
Thm* P:(TProp), R1,R2:(TTProp). Thm* R1 preserves P  R2 preserves P  R1  R2 preserves P	[preserved_by_or]
Thm* R1,R2:(TTProp). Thm* (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1  R2) y)	[symmetric_rel_or]
Thm* R:(TTProp). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y)	[rel_star_symmetric]
Thm* R:(TTProp), x,y:T. (x R^*^-1 y)  (x (R^-1^*) y)	[rel_inverse_star]
Thm* R:(TTProp), n:, x,y:T. (x R^n^-1 y)  (x R^-1^n y)	[rel_inverse_exp]
Thm* x,y:T, R:(TTProp). x = y  (x (R^*) y)	[rel_star_weakening]
Thm* R:(TTProp), x,y,z:T. (x R y)  (y (R^*) z)  (x (R^*) z)	[rel_star_trans]
Thm* R:(TTProp), x,y:T. (x R y)  (x (R^*) y)	[rel_rel_star]
Thm* E:(TTProp), x,y:T. EquivRel(T)(_1 E _2)  (x (E^*) y)  (x E y)	[rel_star_of_equiv]
Thm* R,R2:(TTProp). Thm* Trans(T)(R2(_1,_2)) Thm*  Thm* (x,y:T. (x R y)  (x R2 y))  (x,y:T. (x (R^*) y)  (x R2 y)  x = y)	[rel_star_closure]
Thm* P:(TProp), R:(TTProp). R preserves P  R^* preserves P	[preserved_by_star]
Thm* R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y)	[rel_star_monotonic]
Thm* R:(TTProp), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z)	[rel_star_transitivity]
Thm* R1,R2:(TTProp). R1 => R2  R1^* => R2^*	[rel_star_monotone]
Thm* P:(TProp), R1,R2:(TTProp). Thm* (x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P	[preserved_by_monotone]
Thm* n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n	[rel_exp_monotone]
Thm* R:(TTProp), m,n:, x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z)	[rel_exp_add]
Thm* k,n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i R^k j))	[decidable__rel_exp]
Thm* n:, T:Type, R:(TTProp). R^n  TTProp	[rel_exp_wf]
Thm* n,m:, f,g:(nm). Thm* (x:n, y:m. f(x,y) = g(x,y)) Thm*  Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)	[double_sum_functionality]
Thm* n,m:, f,g:(nm), d:. Thm* sum(f(x,y)-g(x,y) | x < n; y < m) = d Thm*  Thm* sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d	[double_sum_difference]
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:, f:(n), m:(n+1). Thm* sum(f(x) | x < n) = sum(f(x) | x < m)+sum(f(x+m) | x < n-m)	[sum_split]
Thm* n:, f:(n), m,k:n. Thm* m = k Thm*  Thm* (x:n. x = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k)	[pair_support]
Thm* n,m:, f:(nm). Inj(n; m; f)  nm	[pigeon-hole]
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* n:, f:(n), m:n. Thm* (x:n. x = m  f(x) = 0)  sum(f(x) | x < n) = f(m)	[singleton_support_sum]
Thm* n:, f:(n). (x:n. f(x) = 0)  sum(f(x) | x < n) = 0	[empty_support]
Thm* n:, f:(n), m:n. Thm* sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n)	[isolate_summand]
Thm* k:, f,g:(k), p:(k). Thm* sum(if p(i) f(i)+g(i) else f(i) fi | i < k) Thm* = Thm* sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)	[sum-ite]
Thm* k,b:, f:(k). (x:k. bf(x))  bksum(f(x) | x < k)	[sum_lower_bound]
Thm* k,b:, f:(k). (x:k. f(x)b)  sum(f(x) | x < k)bk	[sum_bound]
Thm* k:, f,g:(k). Thm* (x:k. f(x)g(x))  sum(f(x) | x < k)sum(g(x) | x < k)	[sum_le]
Thm* n:, f,g:(n), d:. Thm* sum(f(x)-g(x) | x < n) = d  sum(f(x) | x < n) = sum(g(x) | x < n)+d	[sum_difference]
Thm* n:, f,g:(n). Thm* (i:n. f(i) = g(i))  sum(f(x) | x < n) = sum(g(x) | x < n)	[sum_functionality]
Thm* n:, a:. sum(a | x < n) = an	[sum_constant]
Thm* n:, f,g:(n). Thm* sum(f(x) | x < n)+sum(g(x) | x < n) = sum(f(x)+g(x) | x < n)	[sum_linear]
Thm* n:, f:(n). (x:n. 0f(x))  0sum(f(x) | x < n)	[non_neg_sum]
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* n,m:, f:(nm), x:m. f[n:=x]  (n+1)m	[fappend_wf]
Thm* n:, f,g:(n). Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n)	[fadd_increasing]
Thm* k:, x:. nondecreasing(i.x;k)	[const_nondecreasing]
Thm* n,m:, b:T, c:((n+m)TT). Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))	[primrec_add]
Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c)  T	[primrec_wf]
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]
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:, f:(k), x:k. increasing(f;k)  f(0)+xf(x)	[increasing_lower_bound]
Thm* k:, f:(kk). increasing(f;k)  (i:k. f(i) = i)	[increasing_is_id]
Thm* k,m:. (f:(km). increasing(f;k))  km	[increasing_le]
Thm* k,m:, f:(km). increasing(f;k)  Inj(k; m; f)	[increasing_inj]
Thm* k,m:, f:(km), g:(m). Thm* increasing(f;k)  increasing(g;m)  increasing(g o f;k)	[compose_increasing]
Thm* k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y))	[increasing_implies]
Thm* k:. increasing(i.i;k)	[id_increasing]
Def (ternary) R preserves P  == x,y,z:T. P(x)  P(y)  R(x,y,z)  P(z)	[preserved_by2]
Def R preserves P == x,y:T. P(x)  (x R y)  P(y)	[preserved_by]
Def R1 => R2 == x,y:T. (x R1 y)  (x R2 y)	[rel_implies]
Def nondecreasing(f;k) == i:(k-1). f(i)f(i+1)	[nondecreasing]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 sqequal 1 mb basic

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