Origin Definitions Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
int_2
Nuprl Section: int_2

Selected Objects
IntroductionIntroductory Remarks
COMint_2_begin Reworked (sfa) version of int_2. ...
THMlt_to_le_rw i,j:i<j  i+1j
THMle_to_lt_rw i,j:ij  i<j+1
THMadd_mono_wrt_eq_rw a,b,n:a = b  a+n = b+n
THMadd_mono_wrt_lt_rw a,b,n:a<b  a+n<b+n
THMadd_mono_wrt_le_rw a,b,n:ab  a+nb+n
THMzero_ann_a a,b:a = 0  b = 0  ab = 0
THMzero_ann_b a,b:ab = 0  a = 0 & b = 0
THMmul_preserves_le a,b:n:ab  nanb
THMmul_preserves_lt a,b:n:a<b  na<nb
THMmul_cancel_in_le a,b:n:nanb  ab
THMmul_cancel_in_eq a,b:n:na = nb  a = b
THMmul_cancel_in_lt a,b:n:na<nb  a<b
THMmultiply_functionality_wrt_le i1,i2,j1,j2:i1j1  i2j2  i1i2j1j2
THMint_entire a,b:ab = 0  a = 0  b = 0
THMint_entire_a a,b:a  0  b  0  ab  0
THMmul_bounds_1a a,b:. 0ab
THMmul_bounds_1b a,b:. 0<ab
THMpos_mul_arg_bounds a,b:ab>0  a>0 & b>0  a<0 & b<0
THMneg_mul_arg_bounds a,b:ab<0  a<0 & b>0  a>0 & b<0
COMadd_nat_wf_com It is a bad idea to make these usual wf lemmas since often one mixes integer funs and nat funs. ...
COMquasi_lin_com ======================
QUASI-LINEAR FUNCTIONS
======================
defabsval |i| == if 0i i else -i fi
THMabsval_pos i:. |i| = i
THMabsval_neg i:{...0}. |i| = -i
defpm_equal i =  j == i = j    i = -j
THMabsval_zero i:. |i| = 0  i = 0
THMabsval_ubound i:n:. |i|n  -ni & in
THMabsval_lbound i:n:. |i|>n  i<-n  i>n
THMabsval_eq x,y:. |x| = |y x =  y
THMabsval_sym i:. |i| = |-i|
THMabsval_elim P:(Prop). (x:P(|x|))  (x:P(x))
defimax imax(a;b) == if ab b else a fi
defimin imin(a;b) == if ab a else b fi
THMminus_imax a,b:. -imax(a;b) = imin(-a;-b)
THMminus_imin a,b:. -imin(a;b) = imax(-a;-b)
THMimax_lb a,b,c:. imax(a;b)c  ac & bc
THMimax_ub a,b,c:aimax(b;c ab  ac
THMimax_add_r a,b,c:. imax(a;b)+c = imax(a+c;b+c)
THMimax_assoc a,b,c:. imax(a;imax(b;c)) = imax(imax(a;b);c)
THMimax_com a,b:. imax(a;b) = imax(b;a)
THMimin_assoc a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c)
THMimin_com a,b:. imin(a;b) = imin(b;a)
THMimin_add_r a,b,c:. imin(a;b)+c = imin(a+c;b+c)
THMimin_lb a,b,c:. imin(a;b)c  ac  bc
THMimin_ub a,b,c:aimin(b;c ab & ac
defndiff a -- b == imax(a-b;0)
THMndiff_id_r a:. (a -- 0) = a
THMndiff_ann_l a:. (0 -- a) = 0
THMndiff_inv a:b:. ((a+b) -- b) = a
THMndiff_ndiff a,b:c:. ((a -- b) -- c) = (a -- (b+c))
THMndiff_ndiff_eq_imin a,b:. (a -- (a -- b)) = imin(a;b)
THMndiff_add_eq_imax a,b:. (a -- b)+b = imax(a;b)
THMndiff_zero a,b:. (a -- b) = 0  ab
COMdiv_rem_com ================================
DIVISION AND REMAINDER FUNCTIONS
================================
THMdivision1_sfa k:r1,r2:kq1,q2:q1k+r1 = q2k+r2  q1 = q2 & r1 = r2
THMdivision2_sfa k:r1,r2:kq1,q2:q1k-r1 = q2k-r2  q1 = q2 & r1 = r2
THMdivision3_sfa k:r1,r2:kq1,q2:q1k-r1 = -(q2k+r2 q1 = -q2 & r1 = r2
THMdivision4_sfa k:r1,r2:kq1,q2:.
q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1
THMdivision_mono1_sfa k:r1,r2:kq1,q2:q1k+r1q2k+r2  q1q2
THMdivision_mono2_sfa k:r1,r2:kq1,q2:q1k-r1q2k-r2  q1q2
THMdiv_rem_sum a:n:a = (a  n)n+(a rem n)
THMrem_to_div a:n:. (a rem n) = a-(a  n)n
COMquadrants_com Quadrants for a rem b and a b are numbered as follows: ...
THMrem_bounds_1 a:n:. 0(a rem n) & (a rem n)<n
THMrem_bounds_2 a:{...0}, n:. 0(a rem n) & (a rem n)>-n
THMrem_bounds_3 a:{...0}, n:{...-1}. 0(a rem n) & (a rem n)>n
THMrem_bounds_4 a:n:{...-1}. 0(a rem n) & (a rem n)<-n
THMrem_bounds_1_typing_sfa a:n:. (a rem n n
THMrem_bounds_2_typing_sfa a:{...0}, n:. -(a rem n n
THMrem_bounds_3_typing_sfa a:{...0}, n:{...-1}. -(a rem n (-n)
THMrem_bounds_4_typing_sfa a:n:{...-1}. (a rem n (-n)
THMrem_sym a:b:. (a rem -b) = (a rem b)
THMrem_antisym a:b:. ((-a) rem b) = -(a rem b)
THMdiv_2_to_1 a:{...0}, b:. (a  b) = -((-a b)
THMdiv_3_to_1 a:{...0}, b:{...-1}. (a  b) = ((-a (-b))
THMdiv_4_to_1 a:b:{...-1}. (a  b) = -(a  (-b))
THMdivision_typing1a_sfa a:n:. (a  n 
THMdivision_typing2a_sfa a:{...0}, n:{...-1}. (a  n 
THMdivision_typing1b_sfa a:{...0}, n:. (a  n {...0}
THMdivision_typing2b_sfa a:n:{...-1}. (a  n {...0}
THMrem_2_to_1 a:{...0}, n:. (a rem n) = -((-a) rem n)
THMrem_3_to_1 a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)
THMrem_4_to_1 a:n:{...-1}. (a rem n) = (a rem -n)
THMrem_bounds_z a:b:. |a rem b|<|b|
THMrem_sym_1 a:n:. -(a rem n) = ((-a) rem n)
THMrem_sym_1a a:n:. (a rem n) = -((-a) rem n)
THMrem_sym_2 a:n:. (a rem n) = (a rem -n)
THMrem_mag_bound a:n:. |a rem n|<|n|
THMdiv_bounds_1 a:n:. 0(a  n)
defdiv_nrel Div(a;n;q) == nq  a < n(q+1)
THMdiv_fun_sat_div_nrel a:n:. Div(a;n;a  n)
THMdiv_elim a:n:q:. Div(a;n;q) & (a  n) = q
THMdiv_unique a:n:p,q:. Div(a;n;p Div(a;n;q p = q
THMdiv_lbound_1 a:n:k:k(a  n kna
defrem_nrel Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a
THMrem_fun_sat_rem_nrel a:n:. Rem(a;n;a rem n)
THMdiv_base_case a:n:a<n  (a  n) = 0
THMdiv_rec_case a:n:an  (a  n) = ((a-n n)+1
THMrem_base_case a:n:a<n  (a rem n) = a
THMrem_gen_base_case a:n:. |a|<|n (a rem n) = a
THMrem_rec_case a:n:an  (a rem n) = ((a-n) rem n)
THMrem_invariant a,b:n:. ((a+bn) rem n) = (a rem n)
THMrem_addition i,j:n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)
THMrem_rem_to_rem a:n:. ((a rem n) rem n) = (a rem n)
THMrem_base_case_z a:b:. |a|<|b (a rem b) = a
THMrem_eq_args a:. (a rem a) = 0
THMrem_eq_args_z a:b:. |a| = |b (a rem b) = 0
defmodulus a mod n == if 0a a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi
defdiv_floor a  n == if 0a a  n ; ((-a) rem n)=0 -((-a n) else -((-a n)+-1 fi
THMmod_bounds a:n:. 0(a mod n) & (a mod n)<n
THMdiv_floor_mod_sum a:n:a = (a  n)n+(a mod n)
THMint_mag_well_founded WellFnd{i}(;x,y.|x|<|y|)
THMint_upper_well_founded n:. WellFnd{i}({n...};x,y.x<y)
THMint_upper_ind i:E:({i...}Prop).
E(i (k:{i+1...}. E(k-1)  E(k))  (k:{i...}. E(k))
THMint_lower_well_founded n:. WellFnd{i}({...n};x,y.x>y)
THMint_lower_ind i:E:({...i}Prop).
E(i (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))
THMint_seg_well_founded_up i:j:{i...}. WellFnd{u}({i..j};x,y.x<y)
THMint_seg_ind i:j:{i+1...}, E:({i..j}Prop).
E(i (k:{(i+1)..j}. E(k-1)  E(k))  (k:{i..j}. E(k))
THMint_seg_well_founded_down i:j:{i...}. WellFnd{u}({i..j};x,y.x>y)
THMsplit_int_seg_exist_dom_sfa i,j:.
i<j  (F:({i..j}Prop). (k:{i..j}. F(k))  F(i (k:{(i+1)..j}. F(k)))
THMsplit_int_seg_all_dom_sfa i,j:.
i<j  (F:({i..j}Prop). (k:{i..j}. F(k))  F(i) & (k:{(i+1)..j}. F(k)))
THMdecidable__ex_int_seg i,j:F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))
THMdecidable__all_int_seg i,j:F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections StandardLIB Search Doc