Def (i, j)(x) == if x=i j ; x=j i else x fi

is mentioned by

Thm* k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)	[flip_adjacent]
Thm* k:, x,y,z:k. Thm* y = z  x = y  (x, y) = compose_list([(x, z); (y, z); (x, z)])	[flip_lemma]
Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]	[swap_select]
Def compose_flips(L) == compose_list(map(i.(i, i+1);L))	[compose_flips]
Def swap(L;i;j) == (L o (i, j))	[swap]

In prior sections: mb nat

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