Selected Objects

Introduction		Introductory Remarks
COM	int_2_begin	Reworked (sfa) version of int_2. ...
THM	lt_to_le_rw	i,j:. i<j  i+1j
THM	le_to_lt_rw	i,j:. ij  i<j+1
THM	add_mono_wrt_eq_rw	a,b,n:. a = b  a+n = b+n
THM	add_mono_wrt_lt_rw	a,b,n:. a<b  a+n<b+n
THM	add_mono_wrt_le_rw	a,b,n:. ab  a+nb+n
THM	zero_ann_a	a,b:. a = 0  b = 0  ab = 0
THM	zero_ann_b	a,b:. ab = 0  a = 0 & b = 0
THM	mul_preserves_le	a,b:, n:. ab  nanb
THM	mul_preserves_lt	a,b:, n:. a<b  na<nb
THM	mul_cancel_in_le	a,b:, n:. nanb  ab
THM	mul_cancel_in_eq	a,b:, n:. na = nb  a = b
THM	mul_cancel_in_lt	a,b:, n:. na<nb  a<b
THM	multiply_functionality_wrt_le	i1,i2,j1,j2:. i1j1  i2j2  i1i2j1j2
THM	int_entire	a,b:. ab = 0  a = 0  b = 0
THM	int_entire_a	a,b:. a  0  b  0  ab  0
THM	mul_bounds_1a	a,b:. 0ab
THM	mul_bounds_1b	a,b:. 0<ab
THM	pos_mul_arg_bounds	a,b:. ab>0  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_2	a:{...0}, 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:. a<n  (a  n) = 0
THM	div_rec_case	a:, n:. an  (a  n) = ((a-n)  n)+1
THM	rem_base_case	a:, n:. a<n  (a rem n) = a
THM	rem_gen_base_case	a:, n:. |a|<|n|  (a rem n) = a
THM	rem_rec_case	a:, n:. an  (a rem n) = ((a-n) rem n)
THM	rem_invariant	a,b:, n:. ((a+bn) rem n) = (a rem n)
THM	rem_addition	i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)
THM	rem_rem_to_rem	a:, n:. ((a rem n) rem n) = (a rem n)
THM	rem_base_case_z	a:, b:. |a|<|b|  (a rem b) = a
THM	rem_eq_args	a:. (a rem a) = 0
THM	rem_eq_args_z	a:, b:. |a| = |b|  (a rem b) = 0
def	modulus	a mod n == if 0a a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi
def	div_floor	a  n == if 0a a  n ; ((-a) rem n)=0 -((-a)  n) else -((-a)  n)+-1 fi
THM	mod_bounds	a:, n:. 0(a mod n) & (a mod n)<n
THM	div_floor_mod_sum	a:, n:. a = (a  n)n+(a mod n)
THM	int_mag_well_founded	WellFnd{i}(;x,y.|x|<|y|)
THM	int_upper_well_founded	n:. WellFnd{i}({n...};x,y.x<y)
THM	int_upper_ind	i:, E:({i...}Prop). E(i)  (k:{i+1...}. E(k-1)  E(k))  (k:{i...}. E(k))
THM	int_lower_well_founded	n:. WellFnd{i}({...n};x,y.x>y)
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.x<y)
THM	int_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))
THM	int_seg_well_founded_down	i:, j:{i...}. WellFnd{u}({i..j};x,y.x>y)
THM	split_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)))
THM	split_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)))
THM	decidable__ex_int_seg	i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k)))  Dec(k:{i..j}. F(k))
THM	decidable__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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html