Nuprl - mb_list_2 LEMMAs for range

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

Theorem	Name
Thm* L:T List, n:, f:(n\|\|L\|\|). Thm* increasing(f;n) Thm* Thm* (L1:T List. \|\|L1\|\| = n & sublist_occurence(T;L1;L;f))	[range_sublist]
cites the following:
Thm* n:, f,g:(n). Thm* increasing(f;n) nondecreasing(g;n) increasing(fadd(f;g);n)	[fadd_increasing]
Thm* k:, f:(k), x:k. increasing(f;k) f(0)+xf(x)	[increasing_lower_bound]
Thm* a:T, as:T List, i:. 0<i i\|\|as\|\| [a / as][i] = as[(i-1)]	[select_cons_tl]

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