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

is mentioned by

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]
Def interleaving_occurence(T;L1;L2;L;f1;f2) Def == ||L|| = ||L1||+||L2||   Def == & increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T) Def == & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T) Def == & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2)  )	[interleaving_occurence]
Def disjoint_sublists(T;L1;L2;L) Def == f1:(||L1||||L||), f2:(||L2||||L||). Def == increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T) Def == & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T) Def == & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2))	[disjoint_sublists]
Def sublist_occurence(T;L1;L2;f) Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist_occurence]

In prior sections: mb nat mb list 1

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