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+1 j |
THM | le_to_lt_rw |
i,j: . i j  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: . a b  a+n b+n |
THM | zero_ann_a |
a,b: . a = 0 b = 0  a b = 0 |
THM | zero_ann_b |
a,b: . a b = 0  a = 0 & b = 0 |
THM | mul_preserves_le |
a,b: , n: . a b  n a n b |
THM | mul_preserves_lt |
a,b: , n: . a<b  n a<n b |
THM | mul_cancel_in_le |
a,b: , n: . n a n b  a b |
THM | mul_cancel_in_eq |
a,b: , n:  . n a = n b  a = b |
THM | mul_cancel_in_lt |
a,b: , n: . n a<n b  a<b |
THM | multiply_functionality_wrt_le |
i1,i2,j1,j2: . i1 j1  i2 j2  i1 i2 j1 j2 |
THM | int_entire |
a,b: . a b = 0  a = 0 b = 0 |
THM | int_entire_a |
a,b: . a 0  b 0  a b 0 |
THM | mul_bounds_1a |
a,b: . 0 a b |
THM | mul_bounds_1b |
a,b: . 0<a b |
THM | pos_mul_arg_bounds |
a,b: . a b>0  a>0 & b>0 a<0 & b<0 |
THM | neg_mul_arg_bounds |
a,b: . a b<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  -n i & i n |
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 a b b else a fi |
def | imin |
imin(a;b) == if a 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  a c & b c |
THM | imax_ub |
a,b,c: . a imax(b;c)  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  a c b c |
THM | imin_ub |
a,b,c: . a imin(b;c)  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  a b |
COM | div_rem_com |
================================
DIVISION AND REMAINDER FUNCTIONS
================================ |
THM | division1_sfa |
k: , r1,r2: k, q1,q2: . q1 k+r1 = q2 k+r2  q1 = q2 & r1 = r2 |
THM | division2_sfa |
k: , r1,r2: k, q1,q2: . q1 k-r1 = q2 k-r2  q1 = q2 & r1 = r2 |
THM | division3_sfa |
k: , r1,r2: k, q1,q2: . q1 k-r1 = -(q2 k+r2)  q1 = -q2 & r1 = r2 |
THM | division4_sfa |
k: , r1,r2: k, q1,q2: .
q1 k+r1 = q2 k-r2  q1 = q2 & r1 = 0 & r2 = 0 q2 = q1+1 & r2 = k-r1 |
THM | division_mono1_sfa |
k: , r1,r2: k, q1,q2: . q1 k+r1 q2 k+r2  q1 q2 |
THM | division_mono2_sfa |
k: , r1,r2: k, q1,q2: . q1 k-r1 q2 k-r2  q1 q2 |
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) == n q 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)  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: . Rem(a;n;a rem n) |
THM | div_base_case |
a: , n: . a<n  (a n) = 0 |
THM | div_rec_case |
a: , n: . a n  (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: . a n  (a rem n) = ((a-n) rem n) |
THM | rem_invariant |
a,b: , n: . ((a+b n) 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 0 a a rem n ; ((-a) rem n)= 0 0 else n-((-a) rem n) fi |
def | div_floor |
a  n == if 0 a 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)) |