mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* 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]
cites the following:
0Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L[sublist_pair]
0Thm* k:, i,j:k. (i, j)  kk[flip_wf]
4Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))][swap_select]
3Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  [swap_length]
0Thm* k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y))[increasing_implies]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc