Def {i..j} == {k:| i  k < j }

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* 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* k,n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i R^k j))	[decidable__rel_exp]
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:, 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* 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]
Def nondecreasing(f;k) == i:(k-1). f(i)f(i+1)	[nondecreasing]

In prior sections: int 1 bool 1 int 2 list 1 mb basic

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