Def (R^*)(x,y) == n:. x R^n y

is mentioned by

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* 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]
Def guarded_permutation(T;P) Def == (L1,L2. i:(||L1||-1). P(L1,i) & L2 = swap(L1;i;i+1)  T List)^*	[guarded_permutation]

In prior sections: mb nat

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