mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* L:T List, P:(TTProp).
Thm* (x,y:T. Dec(P(x,y)))
Thm* 
Thm* (x,y:T. P(x,y)  P(y,x))
Thm* 
Thm* (L':T List. 
Thm* ((L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)])))		[partial_sort]
Thm* L:T List, P:(TT).
Thm* (x,y:T. P(x,y)  P(y,x))
Thm* 
Thm* (L':T List. 
Thm* ((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
Thm* (& (i:(||L'||-1). P(L'[i],L'[(i+1)])))		[partial_sort_exists_2]
Thm* L:T List, P:(TT), n:(||L||-1).
Thm* count(x < y in swap(L;n;n+1) | P(x,y))
Thm* =
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)]
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P,L[n])
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if 1
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+else 0 fi		[count_pairs_swap]
Thm* R:(TTProp), k:, x,y:T.
Thm* (x R^k y)
Thm* 
Thm* (L:T List. 
Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))		[rel_exp_list]
Thm* P:(L:(T List)(||L||-1)), m:((T List)).
Thm* (L:T List, i:(||L||-1).
Thm* (P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
Thm* 
Thm* (L:T List. 
Thm* (L':T List. 
Thm* ((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))		[partial_sort_exists]
Thm* P:(L:(T List)(||L||-1)Prop). 
Thm* Trans(T List)(_1 guarded_permutation(T;P) _2)		[guarded_permutation_transitivity]
Thm* f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j)[map_swap]
Thm* L:T List, i:(||L||-1), a,b:T.
Thm* a before b  swap(L;i;i+1)  a before b  L  a = L[(i+1)] & b = L[i]		[l_before_swap]
Thm* i:, L:A List.
Thm* i+1<||L||
Thm* 
Thm* (X,Y:A List.
Thm* (L = (X @ [L[i]; L[(i+1)]] @ Y)
Thm* (& swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))		[swap_adjacent_decomp]
Thm* L:T List, x:T, i,j:{1..(||L||+1)}.
Thm* swap([x / L];i;j) = [x / swap(L;i-1;j-1)]		[swap_cons]
Thm* L1,L2:T List, i,j:||L1||.
Thm* L2 = swap(L1;i;j)
Thm* 
Thm* L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j)
Thm* & (x:||L2||. x = i  x = j  L2[x] = L1[x])		[swapped_select]
Thm* L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1[swap_swap]
Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  [swap_length]
Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))][swap_select]
Thm* L:T List, f:(||L||||L||). ||(L o f)|| = ||L||  [permute_list_length]
Thm* L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[(f(i))][permute_list_select]
Thm* L:T List, P:(||L||Prop).
Thm* (x:||L||. Dec(P(x)))
Thm* 
Thm* (i:||L||. P(i))  (i:||L||. P(i) & (j:||L||. i<j  P(j)))		[last_with_property]
Thm* 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]
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 swap adjacent[P(x;y)](L1,L2)
Def == i:(||L1||-1). P(L1[i];L1[(i+1)]) & L2 = swap(L1;i;i+1)  A List		[swap_adjacent]
Def count(x < y in L | P(x;y))
Def == sum(if (i<j)P(L[i];L[j]) 1 else 0 fi | i < ||L||; j < ||L||)		[count_pairs]
Def guarded_permutation(T;P)
Def == (L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1)  T List)^*		[guarded_permutation]
Def (L o f) == mklist(||L||;i.L[(f(i))])[permute_list]
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 interleaving(T;L1;L2;L)
Def == ||L|| = ||L1||+||L2||   & disjoint_sublists(T;L1;L2;L)		[interleaving]
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: list 1 mb basic mb nat mb list 1

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

mb list 2 Sections MarkB generic Doc