int_2 Theory

Gives many standard lemmas for standard arithmetic functions over the integers, involving both equalities and inequalities.

At end, are some induction lemmas for various subsets of the integers.

Summary of Definitions

Typed Definitions

absval *4

pm_equal *1

imax *1

imin *1

ndiff *1

div_nrel *1

rem_nrel *1

modulus *19

div_floor *3

Main Theorems

int_trichot *1

le_transitivity *1

lt_transitivity_1 *1

lt_transitivity_2 *1

eq_to_le *1

lt_to_le *1

le_to_lt_weaken *1

lt_to_le_rw *1

le_to_lt *1

le_to_lt_rw *1

add_ident *1

add_com *1

add_functionality_wrt_le *8

add_functionality_wrt_lt *4

add_functionality_wrt_eq *1

add_cancel_in_eq *3

add_cancel_in_lt *3

add_cancel_in_le *3

add_mono_wrt_eq *3

add_mono_wrt_eq_rw *1

add_mono_wrt_lt *3

add_mono_wrt_lt_rw *1

add_mono_wrt_le *4

add_mono_wrt_le_rw *1

minus_functionality_wrt_le *4

minus_mono_wrt_le *1

minus_functionality_wrt_eq *1

minus_mono_wrt_eq *1

minus_functionality_wrt_lt *1

minus_mono_wrt_lt *1

sub_functionality_wrt_le *3

minus_minus_cancel *1

mul_ident *1

mul_com *1

zero_ann *1

zero_ann_a *3

zero_ann_b *4

minus_thru_mul *1

mul_preserves_eq *1

mul_preserves_lt *7

mul_preserves_le *6

mul_cancel_in_eq *15

mul_cancel_in_lt *4

mul_cancel_in_le *5

multiply_functionality_wrt_le *7

mul_functionality_wrt_eq *1

int_entire *6

int_entire_a *5

mul_bounds_1a *4

mul_bounds_1b *4

pos_mul_arg_bounds *13

neg_mul_arg_bounds *6

absval_pos *5

absval_neg *5

absval_zero *6

absval_ubound *6

absval_lbound *6

absval_eq *13

absval_sym *4

absval_elim *15

minus_imax *2

minus_imin *2

imax_lb *3

imax_ub *3

imax_add_r *2

imax_assoc *3

imax_com *2

imin_assoc *4

imin_com *2

imin_add_r *5

imin_lb *3

imin_ub *3

ndiff_id_r *2

ndiff_ann_l *2

ndiff_inv *2

ndiff_ndiff *10

ndiff_ndiff_eq_imin *11

ndiff_add_eq_imax *2

ndiff_zero *3

div_rem_sum *4

rem_to_div *4

rem_bounds_1 *4

rem_bounds_2 *4

rem_bounds_3 *4

rem_bounds_4 *4

rem_bounds_z *13

div_2_to_1 *39

div_3_to_1 *45

div_4_to_1 *44

rem_2_to_1 *4

rem_3_to_1 *4

rem_4_to_1 *4

rem_sym *9

rem_antisym *9

rem_sym_1 *18

rem_sym_1a *2

rem_sym_2 *15

rem_mag_bound *32

div_bounds_1 *14

div_fun_sat_div_nrel *18

div_elim *4

div_unique *9

div_lbound_1 *22

rem_fun_sat_rem_nrel *5

div_base_case *4

div_rec_case *15

rem_base_case *4

rem_gen_base_case *28

rem_rec_case *6

rem_invariant *14

rem_addition *16

rem_rem_to_rem *4

rem_base_case_z *9

rem_eq_args *2

rem_eq_args_z *17

mod_bounds *22

div_floor_mod_sum *24

int_mag_well_founded *3

int_upper_well_founded *11

int_upper_ind *11

int_lower_well_founded *15

int_lower_ind *9

int_seg_well_founded_up *5

int_seg_ind *12

int_seg_well_founded_down *10

decidable__ex_int_seg *15