Nuprl - mb_list_2 LEMMAs for permute_by

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* k:, p:(kk). Bij(k; k; p) (L:(k-1) List. p = compose_flips(L))	[permute_by_flips]
cites the following:
0	Thm* k:, i,j:k. Bij(k; k; (i, j))	[flip_bijection]
0	Thm* f,g:(TT). Bij(T; T; f) Bij(T; T; g) Bij(T; T; f o g)	[compose_bij]
0	Thm* k:, f:(kk). Thm* 0<k Thm* Thm* Bij(k; k; f) Thm* Thm* f(k-1) = k-1 f (k-1)(k-1) & Bij((k-1); (k-1); f)	[bijection_restriction]
2	Thm* k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)	[flip_adjacent]
0	Thm* k:, x,y:k. (y, x) o (y, x) = (x.x)	[flip_inverse]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html