mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm* L:T List, P:(||L||Prop).
Thm* (x:||L||. Dec(P(x)))
Thm* 
Thm* (L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
Thm* (interleaving_occurence(T;L1;L2;L;f1;f2)
Thm* (& (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
Thm* (& (i:||L||. 
Thm* (& ((P(i)  (j:||L1||. f1(j) = i))
Thm* (& (& (P(i)  (j:||L2||. f2(j) = i))))		[interleaving_split]
cites the following:
0Thm* 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]
1Thm* 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]
2Thm* 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]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc