mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  == {i:| 0i }

is mentioned by

Thm* k:P:(k).
Thm* ((i:kP(i))  0<search(k;P))
Thm* & (0<search(k;P P(search(k;P)-1) & (j:kj<search(k;P)-1  P(j)))
[search_property]
Thm* k:i,j:k. Bij(kk; (ij))[flip_bijection]
Thm* k:i,j:k. (ij) = (ji)[flip_symmetry]
Thm* n:f:(n), i:(n-1). sum(f((ii+1)(x)) | x < n) = sum(f(x) | x < n)[sum_switch]
Thm* f:(TT), m:(T).
Thm* (x:Tm(f(x))m(x) & (m(f(x)) = m(x f(x) = x))
Thm* 
Thm* (x:Tn:f(f^n(x)) = f^n(x))
[iteration_terminates]
Thm* f:(TT), n:x:Tf(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,gf o g)[fun_exp_compose]
Thm* R:(TTProp), n:x,y:T. (x R^n^-1 y (x R^-1^n y)[rel_inverse_exp]
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:ny:mf(x,y) = g(x,y))
Thm* 
Thm* sum(f(x,y) | x < ny < m) = sum(g(x,y) | x < ny < m)
[double_sum_functionality]
Thm* n,m:f,g:(nm), d:.
Thm* sum(f(x,y)-g(x,y) | x < ny < m) = d
Thm* 
Thm* sum(f(x,y) | x < ny < m) = sum(g(x,y) | x < ny < m)+d
[double_sum_difference]
Thm* n,m:f:(nm), x1,x2:ny1,y2:m.
Thm* x1 = x2  y1 = y2
Thm* 
Thm* (x:ny:m(x = x1 & y = y1 (x = x2 & y = y2 f(x,y) = 0)
Thm* 
Thm* sum(f(x,y) | x < ny < 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:nx = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k)
[pair_support]
Thm* n,m:f:(nm). Inj(nmf nm[pigeon-hole]
Thm* n,k:c:(nk).
Thm* p:(k( List)). 
Thm* sum(||p(j)|| | j < k) = n
Thm* & (j:kx,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y])
Thm* & (j:kx:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)
[finite-partition]
Thm* n:f:(n), m:n.
Thm* (x:nx = m  f(x) = 0)  sum(f(x) | x < n) = f(m)
[singleton_support_sum]
Thm* n:f:(n). (x:nf(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:kbf(x))  bksum(f(x) | x < k)[sum_lower_bound]
Thm* k,b:f:(k). (x:kf(x)b sum(f(x) | x < k)bk[sum_bound]
Thm* k:f,g:(k).
Thm* (x:kf(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:nf(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:nP(f(i)))
Thm* (& (j:kP(g(j)))
Thm* (& (i:m. (j:ni = f(j))  (j:ki = g(j))))
[increasing_split]
Thm* n,m:f:(nm), x:mf[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:Tc:((n+m)TT).
Thm* primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,tc(i+m,t))
[primrec_add]
Thm* T:Type, n:b:Tc:(nTT). primrec(n;b;c T[primrec_wf]
Thm* k:f:(kk).
Thm* 0<k
Thm* 
Thm* Bij(kkf)
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:ni = f(j))  (j:ki = g(j)))
Thm* 
Thm* (j1:nj2:kf(j1) = g(j2))  m = n+k  
[disjoint_increasing_onto]
Thm* k,m:. (f:(km). Inj(kmf))  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:kf(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(kmf)[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:kx<y  f(x)<f(y))[increasing_implies]
Thm* k:. increasing(i.i;k)[id_increasing]
Def (R^*)(x,y) == n:x R^n y[rel_star]

In prior sections: int 1 bool 1 int 2 list 1 sqequal 1

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

mb nat Sections MarkB generic Doc