Selected Objects
| THM | lt_to_le_rw |  i,j: . i < j   i+1 j |
| THM | le_to_lt_rw | i,j:. ij i < j+1 |
| THM | add_functionality_wrt_le | i1,i2,j1,j2:. i1j1  i2j2 i1+i2j1+j2 |
| THM | add_functionality_wrt_lt | i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2 |
| THM | add_cancel_in_eq | a,b,n:. a+n = b+n a = b |
| THM | add_cancel_in_lt | a,b,n:. a+n < b+n a < b |
| THM | add_cancel_in_le | a,b,n:. a+nb+n ab |
| THM | add_mono_wrt_eq | a,b,n:. a = b a+n = b+n |
| THM | add_mono_wrt_eq_rw | a,b,n:. a = b a+n = b+n |
| THM | add_mono_wrt_lt | 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 | a,b,n:. ab a+nb+n |
| THM | add_mono_wrt_le_rw | a,b,n:. ab a+nb+n |
| THM | minus_functionality_wrt_le | i,j:. i j -i-j |
| THM | minus_mono_wrt_lt | i,j:. i > j -i < -j |
| THM | sub_functionality_wrt_le | i1,i2,j1,j2:. i1j1 i2j2 i1-i2j1-j2 |
| THM | zero_ann_a | a,b:. a = 0  b = 0 a b = 0 |
| THM | zero_ann_b | a,b:.  ab = 0 a = 0 & b = 0 |
| THM | mul_preserves_lt | a,b:, n:  . a < b na < nb |
| THM | mul_preserves_le | a,b:, n:. ab nanb |
| 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 | mul_cancel_in_le | a,b:, n:. nanb ab |
| COM | mul_fun_comment | This is only for first quadrant. ... |
| 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 0 i 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 | 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 | 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 | 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_sym | a:, b:. (a rem -b) = (a rem b) |
| THM | rem_antisym | a:, b:. ((-a) rem b) = -(a rem b) |
| 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 0aa rem n ;((-a) rem n)=00 else n-((-a) rem n) fi |
| def | div_floor | a  n == if 0aa 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 | 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)) |