Selected Objects
THM | lt_to_le_rw | i,j: . i < j ![](FONT/if_big.png) i+1 j |
THM | le_to_lt_rw | i,j: . i j ![](FONT/if_big.png) i < j+1 |
THM | add_functionality_wrt_le | i1,i2,j1,j2: . i1 j1 ![](FONT/eq.png) i2 j2 ![](FONT/eq.png) i1+i2 j1+j2 |
THM | add_functionality_wrt_lt | i1,i2,j1,j2: . i1 < j1 ![](FONT/eq.png) i2 j2 ![](FONT/eq.png) i1+i2 < j1+j2 |
THM | add_cancel_in_eq | a,b,n: . a+n = b+n ![](FONT/eq.png) a = b |
THM | add_cancel_in_lt | a,b,n: . a+n < b+n ![](FONT/eq.png) a < b |
THM | add_cancel_in_le | a,b,n: . a+n b+n ![](FONT/eq.png) a b |
THM | add_mono_wrt_eq | a,b,n: . a = b ![](FONT/if_big.png) a+n = b+n |
THM | add_mono_wrt_eq_rw | a,b,n: . a = b ![](FONT/if_big.png) a+n = b+n |
THM | add_mono_wrt_lt | a,b,n: . a < b ![](FONT/if_big.png) a+n < b+n |
THM | add_mono_wrt_lt_rw | a,b,n: . a < b ![](FONT/if_big.png) a+n < b+n |
THM | add_mono_wrt_le | a,b,n: . a b ![](FONT/if_big.png) a+n b+n |
THM | add_mono_wrt_le_rw | a,b,n: . a b ![](FONT/if_big.png) a+n b+n |
THM | minus_functionality_wrt_le | i,j: . i j ![](FONT/eq.png) -i -j |
THM | minus_mono_wrt_lt | i,j: . i > j ![](FONT/if_big.png) -i < -j |
THM | sub_functionality_wrt_le | i1,i2,j1,j2: . i1 j1 ![](FONT/eq.png) i2 j2 ![](FONT/eq.png) i1-i2 j1-j2 |
THM | zero_ann_a | a,b: . a = 0 b = 0 ![](FONT/eq.png) a b = 0 |
THM | zero_ann_b | a,b: . a b = 0 ![](FONT/eq.png) a = 0 & b = 0 |
THM | mul_preserves_lt | a,b: , n:![](FONT/nat.png) . a < b ![](FONT/eq.png) n a < n b |
THM | mul_preserves_le | a,b: , n: . a b ![](FONT/eq.png) n a n b |
THM | mul_cancel_in_eq | a,b: , n:![](FONT/int.png) ![](FONT/minus.png) . n a = n b ![](FONT/eq.png) a = b |
THM | mul_cancel_in_lt | a,b: , n:![](FONT/nat.png) . n a < n b ![](FONT/eq.png) a < b |
THM | mul_cancel_in_le | a,b: , n:![](FONT/nat.png) . n a n b ![](FONT/eq.png) a b |
COM | mul_fun_comment | This is only for first quadrant. ... |
THM | multiply_functionality_wrt_le | i1,i2,j1,j2: . i1 j1 ![](FONT/eq.png) i2 j2 ![](FONT/eq.png) i1 i2 j1 j2 |
THM | int_entire | a,b: . a b = 0 ![](FONT/eq.png) a = 0 b = 0 |
THM | int_entire_a | a,b: . a 0 ![](FONT/eq.png) b 0 ![](FONT/eq.png) a b 0 |
THM | mul_bounds_1a | a,b: . 0 a b |
THM | mul_bounds_1b | a,b:![](FONT/nat.png) . 0 < a b |
THM | pos_mul_arg_bounds | a,b: . a b > 0 ![](FONT/if_big.png) a > 0 & b > 0 a < 0 & b < 0 |
THM | neg_mul_arg_bounds | a,b: . a b < 0 ![](FONT/if_big.png) 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![](FONT/le.png) 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 ![](FONT/if_big.png) i = 0 |
THM | absval_ubound | i: , n: . |i| n ![](FONT/if_big.png) -n i & i n |
THM | absval_lbound | i: , n: . |i| > n ![](FONT/if_big.png) i < -n i > n |
THM | absval_eq | x,y: . |x| = |y| ![](FONT/if_big.png) x = y |
THM | absval_sym | i: . |i| = |-i| |
THM | absval_elim | P:(![](FONT/int.png) ![](FONT/dash.png) Prop). ( x: . P(|x|)) ![](FONT/if_big.png) ( x: . P(x)) |
def | imax | imax(a;b) == if a![](FONT/le.png) b b else a fi |
def | imin | imin(a;b) == if a![](FONT/le.png) b 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 ![](FONT/if_big.png) a c & b c |
THM | imax_ub | a,b,c: . a imax(b;c) ![](FONT/if_big.png) a b a c |
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 ![](FONT/if_big.png) a c b c |
THM | imin_ub | a,b,c: . a imin(b;c) ![](FONT/if_big.png) a b & a c |
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 ![](FONT/if_big.png) a b |
COM | div_rem_com | DIVISION AND REMAINDER FUNCTIONS ... |
THM | div_rem_sum | a: , n:![](FONT/int.png) ![](FONT/minus.png) . a = (a n) n+(a rem n) |
THM | rem_to_div | a: , n:![](FONT/int.png) ![](FONT/minus.png) . (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:![](FONT/nat.png) . 0 (a rem n) & (a rem n) < n |
THM | rem_bounds_2 | a:{...0}, n:![](FONT/nat.png) . 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:![](FONT/nat.png) . (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:![](FONT/nat.png) . (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:![](FONT/int.png) ![](FONT/minus.png) . (a rem -b) = (a rem b) |
THM | rem_antisym | a: , b:![](FONT/int.png) ![](FONT/minus.png) . ((-a) rem b) = -(a rem b) |
THM | rem_bounds_z | a: , b:![](FONT/int.png) ![](FONT/minus.png) . |a rem b| < |b| |
THM | rem_sym_1 | a: , n:![](FONT/int.png) ![](FONT/minus.png) . -(a rem n) = ((-a) rem n) |
THM | rem_sym_1a | a: , n:![](FONT/int.png) ![](FONT/minus.png) . (a rem n) = -((-a) rem n) |
THM | rem_sym_2 | a: , n:![](FONT/int.png) ![](FONT/minus.png) . (a rem n) = (a rem -n) |
THM | rem_mag_bound | a: , n:![](FONT/int.png) ![](FONT/minus.png) . |a rem n| < |n| |
THM | div_bounds_1 | a: , n:![](FONT/nat.png) . 0 (a n) |
def | div_nrel | Div(a;n;q) == n q a < n (q+1) |
THM | div_fun_sat_div_nrel | a: , n:![](FONT/nat.png) . Div(a;n;a n) |
THM | div_elim | a: , n:![](FONT/nat.png) . q: . Div(a;n;q) & (a n) = q |
THM | div_unique | a: , n:![](FONT/nat.png) , p,q: . Div(a;n;p) ![](FONT/eq.png) Div(a;n;q) ![](FONT/eq.png) p = q |
THM | div_lbound_1 | a: , n:![](FONT/nat.png) , k: . k (a n) ![](FONT/if_big.png) k n a |
def | rem_nrel | Rem(a;n;r) == q: . Div(a;n;q) & q n+r = a |
THM | rem_fun_sat_rem_nrel | a: , n:![](FONT/nat.png) . Rem(a;n;a rem n) |
THM | div_base_case | a: , n:![](FONT/nat.png) . a < n ![](FONT/eq.png) (a n) = 0 |
THM | div_rec_case | a: , n:![](FONT/nat.png) . a n ![](FONT/eq.png) (a n) = ((a-n) n)+1 |
THM | rem_base_case | a: , n:![](FONT/nat.png) . a < n ![](FONT/eq.png) (a rem n) = a |
THM | rem_gen_base_case | a: , n:![](FONT/int.png) ![](FONT/minus.png) . |a| < |n| ![](FONT/eq.png) (a rem n) = a |
THM | rem_rec_case | a: , n:![](FONT/nat.png) . a n ![](FONT/eq.png) (a rem n) = ((a-n) rem n) |
THM | rem_invariant | a,b: , n:![](FONT/nat.png) . ((a+b n) rem n) = (a rem n) |
THM | rem_addition | i,j: , n:![](FONT/nat.png) . (((i rem n)+(j rem n)) rem n) = ((i+j) rem n) |
THM | rem_rem_to_rem | a: , n:![](FONT/nat.png) . ((a rem n) rem n) = (a rem n) |
THM | rem_base_case_z | a: , b:![](FONT/int.png) ![](FONT/minus.png) . |a| < |b| ![](FONT/eq.png) (a rem b) = a |
THM | rem_eq_args | a:![](FONT/nat.png) . (a rem a) = 0 |
THM | rem_eq_args_z | a: , b:![](FONT/int.png) ![](FONT/minus.png) . |a| = |b| ![](FONT/eq.png) (a rem b) = 0 |
def | modulus | a mod n == if 0![](FONT/le.png) a a rem n ;((-a) rem n)= 0 0 else n-((-a) rem n) fi |
def | div_floor | a ![](FONT/div.png) n == if 0![](FONT/le.png) a a n ;((-a) rem n)= 0 -((-a) n) else -((-a) n)+-1 fi |
THM | mod_bounds | a: , n:![](FONT/nat.png) . 0 (a mod n) & (a mod n) < n |
THM | div_floor_mod_sum | a: , n:![](FONT/nat.png) . a = (a ![](FONT/div.png) 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...}![](FONT/dash.png) Prop). E(i) ![](FONT/eq.png) ( k:{i+1...}. E(k-1) ![](FONT/eq.png) E(k)) ![](FONT/eq.png) ( k:{i...}. E(k)) |
THM | int_lower_well_founded | n: . WellFnd{i}({...n};x,y.x > y) |
THM | int_lower_ind | i: , E:({...i}![](FONT/dash.png) Prop). E(i) ![](FONT/eq.png) ( k:{...i-1}. E(k+1) ![](FONT/eq.png) E(k)) ![](FONT/eq.png) ( 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 }![](FONT/dash.png) Prop). E(i) ![](FONT/eq.png) ( k:{(i+1)..j }. E(k-1) ![](FONT/eq.png) E(k)) ![](FONT/eq.png) ( 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 }![](FONT/dash.png) Prop). ( k:{i..j }. Dec(F(k))) ![](FONT/eq.png) Dec( k:{i..j }. F(k)) |
THM | decidable__all_int_seg | i,j: , F:({i..j }![](FONT/dash.png) Prop). ( k:{i..j }. Dec(F(k))) ![](FONT/eq.png) Dec( k:{i..j }. F(k)) |