mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x f y == f(x,y)

is mentioned by

Thm* P:(AAProp), f:(BA), x,y:B List.
Thm* (x swap adjacent[P(f(x),f(y))] y)
Thm* 
Thm* (map(f;x) swap adjacent[P(x,y)] map(f;y))		[swap_adjacent_map]
Thm* P:(AAProp), f:(A), L1,L2:A List.
Thm* (L1 swap adjacent[P(x,y)] L2)
Thm* 
Thm* (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))
Thm*  filter(f;L1) = filter(f;L2)		[filter_swap_adjacent]
Thm* P:(AAProp), X,Y:A List, a,b:A.
Thm* P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))		[swap_adjacent_instance]
Thm* P:(AAProp). 
Thm* (Sym x,y:A. P(x,y))  (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)		[symmetric_swap_adjacent]
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* n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i (R^*) j))[decidable__rel_star]
Thm* n:, R:(nnProp), x,y:n. (x (R^*) y)  (k:(n+1). x R^k y)[rel_star_finite]
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]

In prior sections: mb nat rel 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