int_1 Theory

Also includes induction lemmas for naturals, and experiment proving theorem with Ycombinator extract.

Summary of Definitions

Typed Definitions

lelt *

lele *

nat *1

nat_plus *1

int_nzero *1

int_upper *1

int_lower *1

int_seg *1

int_iseg *1

Main Theorems

int_lt_to_int_upper *4

int_le_to_int_upper *2

nat_plus_inc_nat *1

nat_plus_inc_int_nzero *2

nat_ind_a *5

nat_ind_tp *19

nat_ind *4

comp_nat_ind_tp *62

comp_nat_ind_a *10

nat_well_founded *4

complete_nat_ind *3

complete_nat_ind_with_y *31