Selected Objects

THM	id_increasing	k:. increasing(i.i;k)
THM	increasing_implies	k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y))
THM	compose_increasing	k,m:, f:(km), g:(m). increasing(f;k)  increasing(g;m)  increasing(g o f;k)
THM	increasing_inj	k,m:, f:(km). increasing(f;k)  Inj(k; m; f)
THM	increasing_le	k,m:. (f:(km). increasing(f;k))  km
THM	increasing_is_id	k:, f:(kk). increasing(f;k)  (i:k. f(i) = i)
THM	increasing_lower_bound	k:, f:(k), x:k. increasing(f;k)  f(0)+xf(x)
THM	injection_le	k,m:. (f:(km). Inj(k; m; f))  km
THM	disjoint_increasing_onto	m,n,k:, f:(nm), g:(km). increasing(f;n) increasing(g;k) (i:m. (j:n. i = f(j))  (j:k. i = g(j))) (j1:n, j2:k. f(j1) = g(j2))  m = n+k
THM	bijection_restriction	k:, f:(kk). 0<k Bij(k; k; f)  f(k-1) = k-1  f  (k-1)(k-1) & Bij((k-1); (k-1); f)
def	primrec	primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi  (recursive)
THM	primrec_add	n,m:, b:T, c:((n+m)TT). primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))
def	nondecreasing	nondecreasing(f;k) == i:(k-1). f(i)f(i+1)
THM	const_nondecreasing	k:, x:. nondecreasing(i.x;k)
def	fadd	fadd(f;g)(i) == f(i)+g(i)
THM	fadd_increasing	n:, f,g:(n). increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n)
def	fappend	f[n:=x](i) == if i=n x else f(i) fi
THM	increasing_split	m:, P:(mProp). (i:m. Dec(P(i))) (n,k:, f:(nm), g:(km). (increasing(f;n) (& increasing(g;k) (& (i:n. P(f(i))) (& (j:k. P(g(j))) (& (i:m. (j:n. i = f(j))  (j:k. i = g(j))))
def	sum	sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x))
THM	non_neg_sum	n:, f:(n). (x:n. 0f(x))  0sum(f(x) | x < n)
THM	sum_linear	n:, f,g:(n). sum(f(x) | x < n)+sum(g(x) | x < n) = sum(f(x)+g(x) | x < n)
THM	sum_constant	n:, a:. sum(a | x < n) = an
THM	sum_functionality	n:, f,g:(n). (i:n. f(i) = g(i))  sum(f(x) | x < n) = sum(g(x) | x < n)
THM	sum_difference	n:, f,g:(n), d:. sum(f(x)-g(x) | x < n) = d  sum(f(x) | x < n) = sum(g(x) | x < n)+d
THM	sum_le	k:, f,g:(k). (x:k. f(x)g(x))  sum(f(x) | x < k)sum(g(x) | x < k)
THM	sum_bound	k,b:, f:(k). (x:k. f(x)b)  sum(f(x) | x < k)bk
THM	sum_lower_bound	k,b:, f:(k). (x:k. bf(x))  bksum(f(x) | x < k)
THM	sum-ite	k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)
THM	isolate_summand	n:, f:(n), m:n. sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n)
THM	empty_support	n:, f:(n). (x:n. f(x) = 0)  sum(f(x) | x < n) = 0
THM	singleton_support_sum	n:, f:(n), m:n. (x:n. x = m  f(x) = 0)  sum(f(x) | x < n) = f(m)
THM	finite-partition	n,k:, c:(nk). p:(k( List)).  sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x<y  (p(j))[x]>(p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x]<n & c((p(j))[x]) = j)
THM	pigeon-hole	n,m:, f:(nm). Inj(n; m; f)  nm
THM	pair_support	n:, f:(n), m,k:n. m = k  (x:n. x = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k)
THM	sum_split	n:, f:(n), m:(n+1). sum(f(x) | x < n) = sum(f(x) | x < m)+sum(f(x+m) | x < n-m)
def	double_sum	sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n)
THM	pair_support_double_sum	n,m:, f:(nm), x1,x2:n, y1,y2:m. x1 = x2  y1 = y2 (x:n, y:m. (x = x1 & y = y1)  (x = x2 & y = y2)  f(x,y) = 0) sum(f(x,y) | x < n; y < m) = f(x1,y1)+f(x2,y2)
THM	double_sum_difference	n,m:, f,g:(nm), d:. sum(f(x,y)-g(x,y) | x < n; y < m) = d sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)+d
THM	double_sum_functionality	n,m:, f,g:(nm). (x:n, y:m. f(x,y) = g(x,y)) sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)
def	rel_exp	R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi (recursive)
THM	decidable__rel_exp	k,n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i R^k j))
THM	rel_exp_add	R:(TTProp), m,n:, x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z)
def	rel_implies	R1 => R2 == x,y:T. (x R1 y)  (x R2 y)
THM	rel_exp_monotone	n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n
def	preserved_by	R preserves P == x,y:T. P(x)  (x R y)  P(y)
THM	preserved_by_monotone	P:(TProp), R1,R2:(TTProp). (x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P
def	rel_star	(R^*)(x,y) == n:. x R^n y
THM	rel_star_monotone	R1,R2:(TTProp). R1 => R2  R1^* => R2^*
THM	rel_star_transitivity	R:(TTProp), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z)
THM	rel_star_monotonic	R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y)
THM	preserved_by_star	P:(TProp), R:(TTProp). R preserves P  R^* preserves P
THM	rel_star_closure	R,R2:(TTProp). Trans(T)(R2(_1,_2)) (x,y:T. (x R y)  (x R2 y))  (x,y:T. (x (R^*) y)  (x R2 y)  x = y)
THM	rel_star_of_equiv	E:(TTProp), x,y:T. EquivRel(T)(_1 E _2)  (x (E^*) y)  (x E y)
THM	rel_rel_star	R:(TTProp), x,y:T. (x R y)  (x (R^*) y)
THM	rel_star_trans	R:(TTProp), x,y,z:T. (x R y)  (y (R^*) z)  (x (R^*) z)
THM	rel_star_weakening	x,y:T, R:(TTProp). x = y  (x (R^*) y)
def	rel_inverse	R^-1(x,y) == y R x
THM	rel_inverse_exp	R:(TTProp), n:, x,y:T. (x R^n^-1 y)  (x R^-1^n y)
THM	rel_inverse_star	R:(TTProp), x,y:T. (x R^*^-1 y)  (x (R^-1^*) y)
THM	rel_star_symmetric	R:(TTProp). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y)
def	rel_or	(R1  R2)(x,y) == (x R1 y)  (x R2 y)
THM	symmetric_rel_or	R1,R2:(TTProp). (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1  R2) y)
THM	preserved_by_or	P:(TProp), R1,R2:(TTProp). R1 preserves P  R2 preserves P  R1  R2 preserves P
def	fun_exp	f^n == primrec(n;x.x;i,g. f o g)
THM	fun_exp_compose	n:, h,f:(TT). f^n o h = primrec(n;h;i,g. f o g)
THM	fun_exp_add	n,m:, f:(TT). f^n+m = f^n o f^m
THM	fun_exp_add1	f:(TT), n:, x:T. f(f^n(x)) = f^n+1(x)
THM	fun_exp_add1_sub	f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x)
THM	iteration_terminates	f:(TT), m:(T). (x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)) (x:T. n:. f(f^n(x)) = f^n(x))
def	flip	(i, j)(x) == if x=i j ; x=j i else x fi
THM	sum_switch	n:, f:(n), i:(n-1). sum(f((i, i+1)(x)) | x < n) = sum(f(x) | x < n)
THM	flip_symmetry	k:, i,j:k. (i, j) = (j, i)
THM	flip_bijection	k:, i,j:k. Bij(k; k; (i, j))
THM	flip_inverse	k:, x,y:k. (y, x) o (y, x) = (x.x)
THM	flip_twice	k:, x,y,i:k. (y, x)((y, x)(i)) = i
def	search	search(k;P) == primrec(k;0;i,j. if 0<j j ; P(i) i+1 else 0 fi)
THM	search_property	k:, P:(k). ((i:k. P(i))  0<search(k;P)) & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))
def	prop_and	(P  Q)(L) == P(L) & Q(L)
THM	and_preserved_by	P,Q:(TProp), R:(TTProp). R preserves P  R preserves Q  R preserves P  Q
def	preserved_by2	(ternary) R preserves P  == x,y,z:T. P(x)  P(y)  R(x,y,z)  P(z)

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html