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

is mentioned by

Thm* R:(TTProp). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y)	[rel_star_symmetric]
Thm* R:(TTProp), x,y:T. (x R^*^-1 y)  (x (R^-1^*) y)	[rel_inverse_star]
Thm* x,y:T, R:(TTProp). x = y  (x (R^*) y)	[rel_star_weakening]
Thm* R:(TTProp), x,y,z:T. (x R y)  (y (R^*) z)  (x (R^*) z)	[rel_star_trans]
Thm* R:(TTProp), x,y:T. (x R y)  (x (R^*) y)	[rel_rel_star]
Thm* E:(TTProp), x,y:T. EquivRel(T)(_1 E _2)  (x (E^*) y)  (x E y)	[rel_star_of_equiv]
Thm* R,R2:(TTProp). Thm* Trans(T)(R2(_1,_2)) Thm*  Thm* (x,y:T. (x R y)  (x R2 y))  (x,y:T. (x (R^*) y)  (x R2 y)  x = y)	[rel_star_closure]
Thm* P:(TProp), R:(TTProp). R preserves P  R^* preserves P	[preserved_by_star]
Thm* R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y)	[rel_star_monotonic]
Thm* R:(TTProp), x,y,z:T. (x (R^*) y)  (y (R^*) z)  (x (R^*) z)	[rel_star_transitivity]
Thm* R1,R2:(TTProp). R1 => R2  R1^* => R2^*	[rel_star_monotone]

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