Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x))

is mentioned by

Thm* n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)	[sum_switch]
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,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]
Def sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n)	[double_sum]

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