Def increasing(f;k) == i:(k-1). f(i)<f(i+1)

is mentioned by

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:, f,g:(n). Thm* increasing(f;n)  nondecreasing(g;n)  increasing(fadd(f;g);n)	[fadd_increasing]
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:, 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]

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