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+b n) rem n) = (a rem n) | [rem_invariant] |
Thm* a: , n: . a n  (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: . a n  (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)  k n a | [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: . q1 k-r1 q2 k-r2  q1 q2 | [division_mono2_sfa] |
Thm* k: , r1,r2: k, q1,q2: . q1 k+r1 q2 k+r2  q1 q2 | [division_mono1_sfa] |
Thm* k: , r1,r2: k, q1,q2: .
Thm* q1 k+r1 = q2 k-r2  q1 = q2 & r1 = 0 & r2 = 0 q2 = q1+1 & r2 = k-r1 | [division4_sfa] |
Thm* k: , r1,r2: k, q1,q2: . q1 k-r1 = -(q2 k+r2)  q1 = -q2 & r1 = r2 | [division3_sfa] |
Thm* k: , r1,r2: k, q1,q2: . q1 k-r1 = q2 k-r2  q1 = q2 & r1 = r2 | [division2_sfa] |
Thm* k: , r1,r2: k, q1,q2: . q1 k+r1 = q2 k+r2  q1 = q2 & r1 = r2 | [division1_sfa] |
Thm* a,b: . (a -- b) = 0  a b | [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: . a imin(b;c)  a b & a c | [imin_ub] |
Thm* a,b,c: . imin(a;b) c  a c b c | [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: . a imax(b;c)  a b a c | [imax_ub] |
Thm* a,b,c: . imax(a;b) c  a c & b c | [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  -n i & i n | [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: . i j  | [multiply_nat_wf] |
Thm* a,b: . a b<0  a<0 & b>0 a>0 & b<0 | [neg_mul_arg_bounds] |
Thm* a,b: . a b>0  a>0 & b>0 a<0 & b<0 | [pos_mul_arg_bounds] |
Thm* a,b: . 0<a b | [mul_bounds_1b] |
Thm* a,b: . 0 a b | [mul_bounds_1a] |
Thm* a,b: . a 0  b 0  a b 0 | [int_entire_a] |
Thm* a,b: . a b = 0  a = 0 b = 0 | [int_entire] |
Thm* i1,i2,j1,j2: . i1 j1  i2 j2  i1 i2 j1 j2 | [multiply_functionality_wrt_le] |
Thm* a,b: , n: . n a<n b  a<b | [mul_cancel_in_lt] |
Thm* a,b: , n:  . n a = n b  a = b | [mul_cancel_in_eq] |
Thm* a,b: , n: . n a n b  a b | [mul_cancel_in_le] |
Thm* a,b: , n: . a<b  n a<n b | [mul_preserves_lt] |
Thm* a,b: , n: . a b  n a n b | [mul_preserves_le] |
Thm* a,b: . a b = 0  a = 0 & b = 0 | [zero_ann_b] |
Thm* a,b: . a = 0 b = 0  a b = 0 | [zero_ann_a] |
Thm* a,b,n: . a b  a+n b+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: . i j  i<j+1 | [le_to_lt_rw] |
Thm* i,j: . i<j  i+1 j | [lt_to_le_rw] |