mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Prop == Type

is mentioned by

Thm* P,Q:(TProp), R:(TTProp).
Thm* R preserves P  R preserves Q  R preserves P  Q		[and_preserved_by]
Thm* P:(TProp), R1,R2:(TTProp).
Thm* R1 preserves P  R2 preserves P  R1  R2 preserves P		[preserved_by_or]
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* 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]
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* n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n[rel_exp_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]
Thm* n:, T:Type, R:(TTProp). R^n  TTProp[rel_exp_wf]
Thm* m:, P:(mProp).
Thm* (i:m. Dec(P(i)))
Thm* 
Thm* (n,k:, f:(nm), g:(km).
Thm* (increasing(f;n)
Thm* (& increasing(g;k)
Thm* (& (i:n. P(f(i)))
Thm* (& (j:k. P(g(j)))
Thm* (& (i:m. (j:n. i = f(j))  (j:k. i = g(j))))		[increasing_split]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 mb basic

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

mb nat Sections MarkB generic Doc