is mentioned by

Thm* R1,R2:(TTProp). Thm* (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1  R2) y)	[symmetric_rel_or]
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* R:(TTProp), n:, x,y:T. (x R^n^-1 y)  (x R^-1^n y)	[rel_inverse_exp]
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* 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* P:(TProp), R1,R2:(TTProp). Thm* (x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P	[preserved_by_monotone]
Thm* R:(TTProp), m,n:, x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z)	[rel_exp_add]
Thm* k,n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i R^k j))	[decidable__rel_exp]
Def (R1  R2)(x,y) == (x R1 y)  (x R2 y)	[rel_or]
Def R^-1(x,y) == y R x	[rel_inverse]
Def (R^*)(x,y) == n:. x R^n y	[rel_star]
Def R preserves P == x,y:T. P(x)  (x R y)  P(y)	[preserved_by]
Def R1 => R2 == x,y:T. (x R1 y)  (x R2 y)	[rel_implies]
Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)	[rel_exp]

In prior sections: rel 1

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