IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
int_2
Nuprl Section: int_2

 Introduction Introductory Remarks COM int_2_begin Reworked (sfa) version of int_2. ... THM lt_to_le_rw i,j:. i0  a>0 & b>0  a<0 & b<0 THM neg_mul_arg_bounds a,b:. ab<0  a<0 & b>0  a>0 & b<0 COM add_nat_wf_com It is a bad idea to make these usual wf lemmas since often one mixes integer funs and nat funs. ... COM quasi_lin_com ====================== QUASI-LINEAR FUNCTIONS ====================== def absval |i| == if 0i i else -i fi THM absval_pos i:. |i| = i THM absval_neg i:{...0}. |i| = -i def pm_equal i =  j == i = j    i = -j THM absval_zero i:. |i| = 0  i = 0 THM absval_ubound i:, n:. |i|n  -ni & in THM absval_lbound i:, n:. |i|>n  i<-n  i>n THM absval_eq x,y:. |x| = |y|  x =  y THM absval_sym i:. |i| = |-i| THM absval_elim P:(Prop). (x:. P(|x|))  (x:. P(x)) def imax imax(a;b) == if ab b else a fi def imin imin(a;b) == if ab a else b fi THM minus_imax a,b:. -imax(a;b) = imin(-a;-b) THM minus_imin a,b:. -imin(a;b) = imax(-a;-b) THM imax_lb a,b,c:. imax(a;b)c  ac & bc THM imax_ub a,b,c:. aimax(b;c)  ab  ac THM imax_add_r a,b,c:. imax(a;b)+c = imax(a+c;b+c) THM imax_assoc a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c) THM imax_com a,b:. imax(a;b) = imax(b;a) THM imin_assoc a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c) THM imin_com a,b:. imin(a;b) = imin(b;a) THM imin_add_r a,b,c:. imin(a;b)+c = imin(a+c;b+c) THM imin_lb a,b,c:. imin(a;b)c  ac  bc THM imin_ub a,b,c:. aimin(b;c)  ab & ac def ndiff a -- b == imax(a-b;0) THM ndiff_id_r a:. (a -- 0) = a THM ndiff_ann_l a:. (0 -- a) = 0 THM ndiff_inv a:, b:. ((a+b) -- b) = a THM ndiff_ndiff a,b:, c:. ((a -- b) -- c) = (a -- (b+c)) THM ndiff_ndiff_eq_imin a,b:. (a -- (a -- b)) = imin(a;b) THM ndiff_add_eq_imax a,b:. (a -- b)+b = imax(a;b) THM ndiff_zero a,b:. (a -- b) = 0  ab COM div_rem_com ================================ DIVISION AND REMAINDER FUNCTIONS ================================ THM division1_sfa k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2 THM division2_sfa k:, r1,r2:k, q1,q2:. q1k-r1 = q2k-r2  q1 = q2 & r1 = r2 THM division3_sfa k:, r1,r2:k, q1,q2:. q1k-r1 = -(q2k+r2)  q1 = -q2 & r1 = r2 THM division4_sfa k:, r1,r2:k, q1,q2:. q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1 THM division_mono1_sfa k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2  q1q2 THM division_mono2_sfa k:, r1,r2:k, q1,q2:. q1k-r1q2k-r2  q1q2 THM div_rem_sum a:, n:. a = (a  n)n+(a rem n) THM rem_to_div a:, n:. (a rem n) = a-(a  n)n COM quadrants_com Quadrants for a rem b and a b are numbered as follows: ... THM rem_bounds_1 a:, n:. 0(a rem n) & (a rem n)-n THM rem_bounds_3 a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n THM rem_bounds_4 a:, n:{...-1}. 0(a rem n) & (a rem n)<-n THM rem_bounds_1_typing_sfa a:, n:. (a rem n)  n THM rem_bounds_2_typing_sfa a:{...0}, n:. -(a rem n)  n THM rem_bounds_3_typing_sfa a:{...0}, n:{...-1}. -(a rem n)  (-n) THM rem_bounds_4_typing_sfa a:, n:{...-1}. (a rem n)  (-n) THM rem_sym a:, b:. (a rem -b) = (a rem b) THM rem_antisym a:, b:. ((-a) rem b) = -(a rem b) THM div_2_to_1 a:{...0}, b:. (a  b) = -((-a)  b) THM div_3_to_1 a:{...0}, b:{...-1}. (a  b) = ((-a)  (-b)) THM div_4_to_1 a:, b:{...-1}. (a  b) = -(a  (-b)) THM division_typing1a_sfa a:, n:. (a  n) THM division_typing2a_sfa a:{...0}, n:{...-1}. (a  n) THM division_typing1b_sfa a:{...0}, n:. (a  n)  {...0} THM division_typing2b_sfa a:, n:{...-1}. (a  n)  {...0} THM rem_2_to_1 a:{...0}, n:. (a rem n) = -((-a) rem n) THM rem_3_to_1 a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n) THM rem_4_to_1 a:, n:{...-1}. (a rem n) = (a rem -n) THM rem_bounds_z a:, b:. |a rem b|<|b| THM rem_sym_1 a:, n:. -(a rem n) = ((-a) rem n) THM rem_sym_1a a:, n:. (a rem n) = -((-a) rem n) THM rem_sym_2 a:, n:. (a rem n) = (a rem -n) THM rem_mag_bound a:, n:. |a rem n|<|n| THM div_bounds_1 a:, n:. 0(a  n) def div_nrel Div(a;n;q) == nq  a < n(q+1) THM div_fun_sat_div_nrel a:, n:. Div(a;n;a  n) THM div_elim a:, n:. q:. Div(a;n;q) & (a  n) = q THM div_unique a:, n:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q THM div_lbound_1 a:, n:, k:. k(a  n)  kna def rem_nrel Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a THM rem_fun_sat_rem_nrel a:, n:. Rem(a;n;a rem n) THM div_base_case a:, n:. ay) THM int_lower_ind i:, E:({...i}Prop). E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k)) THM int_seg_well_founded_up i:, j:{i...}. WellFnd{u}({i..j};x,y.xy) THM split_int_seg_exist_dom_sfa i,j:. i
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html