Def guarded_permutation(T;P)
Def == (L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1)  T List)^*

is mentioned by

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* 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]

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