is mentioned by

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* 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* 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]
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 guarded_permutation(T;P) Def == (L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1)  T List)^*	[guarded_permutation]

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