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

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]

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