int 2 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))[decidable__all_int_seg]
Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))[decidable__ex_int_seg]
Thm* i,j:.
Thm* i<j
Thm* 
Thm* (F:({i..j}Prop). (k:{i..j}. F(k))  F(i) & (k:{(i+1)..j}. F(k)))		[split_int_seg_all_dom_sfa]
Thm* i,j:.
Thm* i<j
Thm* 
Thm* (F:({i..j}Prop). (k:{i..j}. F(k))  F(i)  (k:{(i+1)..j}. F(k)))		[split_int_seg_exist_dom_sfa]
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x>y)[int_seg_well_founded_down]
Thm* i:, j:{i+1...}, E:({i..j}Prop).
Thm* E(i)  (k:{(i+1)..j}. E(k-1)  E(k))  (k:{i..j}. E(k))		[int_seg_ind]
Thm* i:, j:{i...}. WellFnd{u}({i..j};x,y.x<y)[int_seg_well_founded_up]
Thm* i:, E:({...i}Prop).
Thm* E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))		[int_lower_ind]
Thm* n:. WellFnd{i}({...n};x,y.x>y)[int_lower_well_founded]
Thm* i:, E:({i...}Prop).
Thm* E(i)  (k:{i+1...}. E(k-1)  E(k))  (k:{i...}. E(k))		[int_upper_ind]
Thm* n:. WellFnd{i}({n...};x,y.x<y)[int_upper_well_founded]
Thm* a:, n:. a = (a  n)n+(a mod n)[div_floor_mod_sum]
Thm* a:, n:. 0(a mod n) & (a mod n)<n[mod_bounds]
Thm* a:, n:. (a mod n)  [modulus_wf]
Thm* a:, b:. |a| = |b|  (a rem b) = 0[rem_eq_args_z]
Thm* a:. (a rem a) = 0[rem_eq_args]
Thm* a:, b:. |a|<|b|  (a rem b) = a[rem_base_case_z]
Thm* a:, n:. ((a rem n) rem n) = (a rem n)[rem_rem_to_rem]
Thm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)[rem_addition]
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n)[rem_invariant]
Thm* a:, n:. an  (a rem n) = ((a-n) rem n)[rem_rec_case]
Thm* a:, n:. |a|<|n|  (a rem n) = a[rem_gen_base_case]
Thm* a:, n:. a<n  (a rem n) = a[rem_base_case]
Thm* a:, n:. an  (a  n) = ((a-n)  n)+1[div_rec_case]
Thm* a:, n:. a<n  (a  n) = 0[div_base_case]
Thm* a:, n:. Rem(a;n;a rem n)[rem_fun_sat_rem_nrel]
Thm* a:, n:, k:. k(a  n)  kna[div_lbound_1]
Thm* a:, n:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q[div_unique]
Thm* a:, n:. q:. Div(a;n;q) & (a  n) = q[div_elim]
Thm* a:, n:. Div(a;n;a  n)[div_fun_sat_div_nrel]
Thm* a:, n:. 0(a  n)[div_bounds_1]
Thm* a:, n:. |a rem n|<|n|[rem_mag_bound]
Thm* a:, n:. (a rem n) = (a rem -n)[rem_sym_2]
Thm* a:, n:. (a rem n) = -((-a) rem n)[rem_sym_1a]
Thm* a:, n:. -(a rem n) = ((-a) rem n)[rem_sym_1]
Thm* a:, b:. |a rem b|<|b|[rem_bounds_z]
Thm* a:, n:{...-1}. (a rem n) = (a rem -n)[rem_4_to_1]
Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)[rem_3_to_1]
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)[rem_2_to_1]
Thm* a:, n:{...-1}. (a  n)  {...0}[division_typing2b_sfa]
Thm* a:{...0}, n:. (a  n)  {...0}[division_typing1b_sfa]
Thm* a:{...0}, n:{...-1}. (a  n)  [division_typing2a_sfa]
Thm* a:, n:. (a  n)  [division_typing1a_sfa]
Thm* a:, b:{...-1}. (a  b) = -(a  (-b))[div_4_to_1]
Thm* a:{...0}, b:{...-1}. (a  b) = ((-a)  (-b))[div_3_to_1]
Thm* a:{...0}, b:. (a  b) = -((-a)  b)[div_2_to_1]
Thm* a:, b:. ((-a) rem b) = -(a rem b)[rem_antisym]
Thm* a:, b:. (a rem -b) = (a rem b)[rem_sym]
Thm* a:, n:{...-1}. (a rem n)  (-n)[rem_bounds_4_typing_sfa]
Thm* a:{...0}, n:{...-1}. -(a rem n)  (-n)[rem_bounds_3_typing_sfa]
Thm* a:{...0}, n:. -(a rem n)  n[rem_bounds_2_typing_sfa]
Thm* a:, n:. (a rem n)  n[rem_bounds_1_typing_sfa]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n)<-n[rem_bounds_4]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n)>-n[rem_bounds_2]
Thm* a:, n:. 0(a rem n) & (a rem n)<n[rem_bounds_1]
Thm* a:, n:. (a rem n) = a-(a  n)n[rem_to_div]
Thm* a:, n:. a = (a  n)n+(a rem n)[div_rem_sum]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1q2k-r2  q1q2[division_mono2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2  q1q2[division_mono1_sfa]
Thm* k:, r1,r2:k, q1,q2:.
Thm* q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1		[division4_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = -(q2k+r2)  q1 = -q2 & r1 = r2[division3_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = q2k-r2  q1 = q2 & r1 = r2[division2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2[division1_sfa]
Thm* a,b:. (a -- b) = 0  ab[ndiff_zero]
Thm* a,b:. (a -- b)+b = imax(a;b)[ndiff_add_eq_imax]
Thm* a,b:. (a -- (a -- b)) = imin(a;b)[ndiff_ndiff_eq_imin]
Thm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c))[ndiff_ndiff]
Thm* a:, b:. ((a+b) -- b) = a[ndiff_inv]
Thm* a:. (0 -- a) = 0[ndiff_ann_l]
Thm* a:. (a -- 0) = a[ndiff_id_r]
Thm* a,b,c:. aimin(b;c)  ab & ac[imin_ub]
Thm* a,b,c:. imin(a;b)c  ac  bc[imin_lb]
Thm* a,b,c:. imin(a;b)+c = imin(a+c;b+c)[imin_add_r]
Thm* a,b:. imin(a;b) = imin(b;a)[imin_com]
Thm* a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c)[imin_assoc]
Thm* a,b:. imax(a;b) = imax(b;a)[imax_com]
Thm* a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)[imax_assoc]
Thm* a,b,c:. imax(a;b)+c = imax(a+c;b+c)[imax_add_r]
Thm* a,b,c:. aimax(b;c)  ab  ac[imax_ub]
Thm* a,b,c:. imax(a;b)c  ac & bc[imax_lb]
Thm* a,b:. -imin(a;b) = imax(-a;-b)[minus_imin]
Thm* a,b:. -imax(a;b) = imin(-a;-b)[minus_imax]
Thm* P:(Prop). (x:. P(|x|))  (x:. P(x))[absval_elim]
Thm* i:. |i| = |-i|[absval_sym]
Thm* x,y:. |x| = |y|  x =  y[absval_eq]
Thm* i:, n:. |i|>n  i<-n  i>n[absval_lbound]
Thm* i:, n:. |i|n  -ni & in[absval_ubound]
Thm* i:. |i| = 0  i = 0[absval_zero]
Thm* i:{...0}. |i| = -i[absval_neg]
Thm* i:. |i| = i[absval_pos]
Thm* x:. |x|  [absval_wf]
Thm* i,j:. ij  [multiply_nat_wf]
Thm* a,b:. ab<0  a<0 & b>0  a>0 & b<0[neg_mul_arg_bounds]
Thm* a,b:. ab>0  a>0 & b>0  a<0 & b<0[pos_mul_arg_bounds]
Thm* a,b:. 0<ab[mul_bounds_1b]
Thm* a,b:. 0ab[mul_bounds_1a]
Thm* a,b:. a  0  b  0  ab  0[int_entire_a]
Thm* a,b:. ab = 0  a = 0  b = 0[int_entire]
Thm* i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2[multiply_functionality_wrt_le]
Thm* a,b:, n:. na<nb  a<b[mul_cancel_in_lt]
Thm* a,b:, n:. na = nb  a = b[mul_cancel_in_eq]
Thm* a,b:, n:. nanb  ab[mul_cancel_in_le]
Thm* a,b:, n:. a<b  na<nb[mul_preserves_lt]
Thm* a,b:, n:. ab  nanb[mul_preserves_le]
Thm* a,b:. ab = 0  a = 0 & b = 0[zero_ann_b]
Thm* a,b:. a = 0  b = 0  ab = 0[zero_ann_a]
Thm* a,b,n:. ab  a+nb+n[add_mono_wrt_le_rw]
Thm* a,b,n:. a<b  a+n<b+n[add_mono_wrt_lt_rw]
Thm* a,b,n:. a = b  a+n = b+n[add_mono_wrt_eq_rw]
Thm* i,j:. ij  i<j+1[le_to_lt_rw]
Thm* i,j:. i<j  i+1j[lt_to_le_rw]

In prior sections: core well fnd int 1 bool 1

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

int 2 Sections StandardLIB Doc