import
import_segment "hol4"
def_maps
"nat_elim__magic" > "nat_elim__magic_def"
"ODD" > "ODD_def"
"FACT" > "FACT_def"
"EVEN" > "EVEN_def"
const_maps
"num_case" > "Nat.nat.nat_case"
"nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1"
"NUMERAL" > "HOL4Compat.NUMERAL"
"MOD" > "Divides.op mod" :: "nat => nat => nat"
"MIN" > "Orderings.min" :: "nat => nat => nat"
"MAX" > "Orderings.max" :: "nat => nat => nat"
"FUNPOW" > "HOL4Compat.FUNPOW"
"EXP" > "Nat.power" :: "nat => nat => nat"
"DIV" > "Divides.op div" :: "nat => nat => nat"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO"
">=" > "HOL4Compat.nat_ge"
">" > "HOL4Compat.nat_gt"
"<=" > "op <=" :: "nat => nat => bool"
"-" > "op -" :: "nat => nat => nat"
"+" > "op +" :: "nat => nat => nat"
"*" > "op *" :: "nat => nat => nat"
thm_maps
"num_case_def" > "HOL4Compat.num_case_def"
"num_case_cong" > "HOL4Base.arithmetic.num_case_cong"
"num_case_compute" > "HOL4Base.arithmetic.num_case_compute"
"num_CASES" > "Nat.nat.nchotomy"
"nat_elim__magic_def" > "HOL4Base.arithmetic.nat_elim__magic_def"
"nat_elim__magic" > "HOL4Base.arithmetic.nat_elim__magic"
"ZERO_MOD" > "HOL4Base.arithmetic.ZERO_MOD"
"ZERO_LESS_EXP" > "HOL4Base.arithmetic.ZERO_LESS_EXP"
"ZERO_LESS_EQ" > "Nat.le0"
"ZERO_DIV" > "HOL4Base.arithmetic.ZERO_DIV"
"WOP" > "HOL4Base.arithmetic.WOP"
"TWO" > "HOL4Base.arithmetic.TWO"
"TIMES2" > "NatSimprocs.nat_mult_2"
"SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
"SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left"
"SUC_NOT" > "Nat.nat.simps_2"
"SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
"SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
"SUB_SUB" > "NatArith.diff_diff_right"
"SUB_RIGHT_SUB" > "Nat.diff_diff_left"
"SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ"
"SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS"
"SUB_RIGHT_GREATER_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER_EQ"
"SUB_RIGHT_GREATER" > "HOL4Base.arithmetic.SUB_RIGHT_GREATER"
"SUB_RIGHT_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_EQ"
"SUB_RIGHT_ADD" > "HOL4Base.arithmetic.SUB_RIGHT_ADD"
"SUB_PLUS" > "Nat.diff_diff_left"
"SUB_MONO_EQ" > "Nat.diff_Suc_Suc"
"SUB_LESS_OR" > "HOL4Base.arithmetic.SUB_LESS_OR"
"SUB_LESS_EQ_ADD" > "HOL4Base.arithmetic.SUB_LESS_EQ_ADD"
"SUB_LESS_EQ" > "Nat.diff_le_self"
"SUB_LESS_0" > "Nat.zero_less_diff"
"SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC"
"SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB"
"SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ"
"SUB_LEFT_LESS" > "NatArith.less_diff_conv"
"SUB_LEFT_GREATER_EQ" > "NatArith.le_diff_conv"
"SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER"
"SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ"
"SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD"
"SUB_EQ_EQ_0" > "HOL4Base.arithmetic.SUB_EQ_EQ_0"
"SUB_EQ_0" > "Nat.diff_is_0_eq"
"SUB_EQUAL_0" > "Nat.diff_self_eq_0"
"SUB_ELIM_THM" > "HOL4Base.arithmetic.SUB_ELIM_THM"
"SUB_CANCEL" > "HOL4Base.arithmetic.SUB_CANCEL"
"SUB_ADD" > "Nat.le_add_diff_inverse2"
"SUB_0" > "HOL4Base.arithmetic.SUB_0"
"SUB" > "HOL4Compat.SUB"
"RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
"RIGHT_ADD_DISTRIB" > "Nat.nat_distrib_1"
"PRE_SUC_EQ" > "HOL4Base.arithmetic.PRE_SUC_EQ"
"PRE_SUB1" > "HOL4Base.arithmetic.PRE_SUB1"
"PRE_SUB" > "HOL4Base.arithmetic.PRE_SUB"
"PRE_ELIM_THM" > "HOL4Base.arithmetic.PRE_ELIM_THM"
"OR_LESS" > "Nat.Suc_le_lessD"
"ONE" > "Nat.One_nat_def"
"ODD_OR_EVEN" > "HOL4Base.arithmetic.ODD_OR_EVEN"
"ODD_MULT" > "HOL4Base.arithmetic.ODD_MULT"
"ODD_EXISTS" > "HOL4Base.arithmetic.ODD_EXISTS"
"ODD_EVEN" > "HOL4Base.arithmetic.ODD_EVEN"
"ODD_DOUBLE" > "HOL4Base.arithmetic.ODD_DOUBLE"
"ODD_ADD" > "HOL4Base.arithmetic.ODD_ADD"
"ODD" > "HOL4Base.arithmetic.ODD"
"NUMERAL_DEF" > "HOL4Compat.NUMERAL_def"
"NUMERAL_BIT2" > "HOL4Compat.NUMERAL_BIT2_def"
"NUMERAL_BIT1" > "HOL4Compat.NUMERAL_BIT1_def"
"NOT_ZERO_LT_ZERO" > "Nat.neq0_conv"
"NOT_SUC_LESS_EQ_0" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ_0"
"NOT_SUC_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_LESS_EQ"
"NOT_SUC_ADD_LESS_EQ" > "HOL4Base.arithmetic.NOT_SUC_ADD_LESS_EQ"
"NOT_ODD_EQ_EVEN" > "HOL4Base.arithmetic.NOT_ODD_EQ_EVEN"
"NOT_NUM_EQ" > "HOL4Base.arithmetic.NOT_NUM_EQ"
"NOT_LESS_EQUAL" > "Orderings.linorder_not_le"
"NOT_LESS" > "Nat.le_def"
"NOT_LEQ" > "HOL4Base.arithmetic.NOT_LEQ"
"NOT_GREATER_EQ" > "HOL4Base.arithmetic.NOT_GREATER_EQ"
"NOT_GREATER" > "Nat.le_def"
"NOT_EXP_0" > "HOL4Base.arithmetic.NOT_EXP_0"
"NORM_0" > "HOL4Base.arithmetic.NORM_0"
"MULT_SYM" > "IntDef.zmult_ac_2"
"MULT_SUC_EQ" > "HOL4Base.arithmetic.MULT_SUC_EQ"
"MULT_SUC" > "Nat.mult_Suc_right"
"MULT_RIGHT_1" > "Finite_Set.AC_mult.f_e.ident"
"MULT_MONO_EQ" > "Nat.Suc_mult_cancel1"
"MULT_LESS_EQ_SUC" > "Nat.Suc_mult_le_cancel1"
"MULT_LEFT_1" > "Finite_Set.AC_mult.f_e.left_ident"
"MULT_INCREASES" > "HOL4Base.arithmetic.MULT_INCREASES"
"MULT_EXP_MONO" > "HOL4Base.arithmetic.MULT_EXP_MONO"
"MULT_EQ_1" > "HOL4Base.arithmetic.MULT_EQ_1"
"MULT_EQ_0" > "Nat.mult_is_0"
"MULT_DIV" > "Divides.div_mult_self_is_m"
"MULT_COMM" > "IntDef.zmult_ac_2"
"MULT_CLAUSES" > "HOL4Base.arithmetic.MULT_CLAUSES"
"MULT_ASSOC" > "IntDef.zmult_ac_1"
"MULT_0" > "Nat.mult_0_right"
"MULT" > "HOL4Compat.MULT"
"MOD_UNIQUE" > "HOL4Base.arithmetic.MOD_UNIQUE"
"MOD_TIMES2" > "HOL4Base.arithmetic.MOD_TIMES2"
"MOD_TIMES" > "HOL4Base.arithmetic.MOD_TIMES"
"MOD_PLUS" > "HOL4Base.arithmetic.MOD_PLUS"
"MOD_P" > "HOL4Base.arithmetic.MOD_P"
"MOD_ONE" > "Divides.mod_1"
"MOD_MULT_MOD" > "HOL4Base.arithmetic.MOD_MULT_MOD"
"MOD_MULT" > "HOL4Base.arithmetic.MOD_MULT"
"MOD_MOD" > "HOL4Base.arithmetic.MOD_MOD"
"MOD_EQ_0" > "HOL4Base.arithmetic.MOD_EQ_0"
"MOD_COMMON_FACTOR" > "HOL4Base.arithmetic.MOD_COMMON_FACTOR"
"MIN_MAX_PRED" > "HOL4Base.arithmetic.MIN_MAX_PRED"
"MIN_MAX_LT" > "HOL4Base.arithmetic.MIN_MAX_LT"
"MIN_MAX_EQ" > "HOL4Base.arithmetic.MIN_MAX_EQ"
"MIN_LT" > "HOL4Base.arithmetic.MIN_LT"
"MIN_LE" > "HOL4Base.arithmetic.MIN_LE"
"MIN_IDEM" > "Finite_Set.min.f.ACI_4"
"MIN_DEF" > "HOL4Compat.MIN_DEF"
"MIN_COMM" > "Finite_Set.min.f.ACI_2"
"MIN_ASSOC" > "Finite_Set.min.f.ACI_1"
"MIN_0" > "HOL4Base.arithmetic.MIN_0"
"MAX_LT" > "HOL4Base.arithmetic.MAX_LT"
"MAX_LE" > "HOL4Base.arithmetic.MAX_LE"
"MAX_IDEM" > "Finite_Set.max.f.ACI_4"
"MAX_DEF" > "HOL4Compat.MAX_DEF"
"MAX_COMM" > "Finite_Set.max.f.ACI_2"
"MAX_ASSOC" > "Finite_Set.max.f.ACI_1"
"MAX_0" > "HOL4Base.arithmetic.MAX_0"
"LESS_TRANS" > "Nat.less_trans"
"LESS_SUC_NOT" > "HOL4Base.arithmetic.LESS_SUC_NOT"
"LESS_SUC_EQ_COR" > "Nat.Suc_lessI"
"LESS_SUB_ADD_LESS" > "HOL4Base.arithmetic.LESS_SUB_ADD_LESS"
"LESS_OR_EQ_ADD" > "HOL4Base.arithmetic.LESS_OR_EQ_ADD"
"LESS_OR_EQ" > "HOL4Compat.LESS_OR_EQ"
"LESS_OR" > "Nat.Suc_leI"
"LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
"LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
"LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
"LESS_MONO_REV" > "Nat.Suc_less_SucD"
"LESS_MONO_MULT" > "Nat.mult_le_mono1"
"LESS_MONO_EQ" > "Nat.Suc_less_eq"
"LESS_MONO_ADD_INV" > "OrderedGroup.add_less_imp_less_right"
"LESS_MONO_ADD_EQ" > "OrderedGroup.add_less_cancel_right"
"LESS_MONO_ADD" > "Nat.add_less_mono1"
"LESS_MOD" > "Divides.mod_less"
"LESS_LESS_SUC" > "HOL4Base.arithmetic.LESS_LESS_SUC"
"LESS_LESS_EQ_TRANS" > "Nat.less_le_trans"
"LESS_LESS_CASES" > "HOL4Base.arithmetic.LESS_LESS_CASES"
"LESS_IMP_LESS_OR_EQ" > "Nat.le_simps_1"
"LESS_IMP_LESS_ADD" > "Nat.trans_less_add1"
"LESS_EXP_SUC_MONO" > "HOL4Base.arithmetic.LESS_EXP_SUC_MONO"
"LESS_EQ_TRANS" > "Nat.le_trans"
"LESS_EQ_SUC_REFL" > "HOL4Base.arithmetic.LESS_EQ_SUC_REFL"
"LESS_EQ_SUB_LESS" > "HOL4Base.arithmetic.LESS_EQ_SUB_LESS"
"LESS_EQ_REFL" > "Finite_Set.max.f_below.below_refl"
"LESS_EQ_MONO_ADD_EQ" > "OrderedGroup.add_le_cancel_right"
"LESS_EQ_MONO" > "Nat.Suc_le_mono"
"LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
"LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
"LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
"LESS_EQ_EXISTS" > "NatArith.le_iff_add"
"LESS_EQ_CASES" > "Nat.nat_le_linear"
"LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
"LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc"
"LESS_EQ_ADD" > "Nat.le_add1"
"LESS_EQ_0" > "Nat.le_0_eq"
"LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
"LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
"LESS_EQ" > "Nat.le_simps_3"
"LESS_DIV_EQ_ZERO" > "Divides.div_less"
"LESS_CASES_IMP" > "HOL4Base.arithmetic.LESS_CASES_IMP"
"LESS_CASES" > "HOL4Base.arithmetic.LESS_CASES"
"LESS_ANTISYM" > "HOL4Base.arithmetic.LESS_ANTISYM"
"LESS_ADD_SUC" > "HOL4Base.arithmetic.LESS_ADD_SUC"
"LESS_ADD_NONZERO" > "HOL4Base.arithmetic.LESS_ADD_NONZERO"
"LESS_ADD_1" > "HOL4Base.arithmetic.LESS_ADD_1"
"LESS_ADD" > "HOL4Base.arithmetic.LESS_ADD"
"LESS_0_CASES" > "HOL4Base.arithmetic.LESS_0_CASES"
"LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
"LEFT_ADD_DISTRIB" > "Nat.nat_distrib_2"
"LE" > "HOL4Base.arithmetic.LE"
"INV_PRE_LESS_EQ" > "HOL4Base.arithmetic.INV_PRE_LESS_EQ"
"INV_PRE_LESS" > "HOL4Base.arithmetic.INV_PRE_LESS"
"INV_PRE_EQ" > "HOL4Base.arithmetic.INV_PRE_EQ"
"GREATER_OR_EQ" > "HOL4Compat.GREATER_OR_EQ"
"GREATER_EQ" > "HOL4Compat.real_ge"
"GREATER_DEF" > "HOL4Compat.GREATER_DEF"
"FUN_EQ_LEMMA" > "HOL4Base.arithmetic.FUN_EQ_LEMMA"
"FUNPOW" > "HOL4Compat.FUNPOW"
"FACT_LESS" > "HOL4Base.arithmetic.FACT_LESS"
"FACT" > "HOL4Base.arithmetic.FACT"
"EXP_INJECTIVE" > "Power.power_inject_exp"
"EXP_EQ_1" > "HOL4Base.arithmetic.EXP_EQ_1"
"EXP_EQ_0" > "HOL4Base.arithmetic.EXP_EQ_0"
"EXP_ALWAYS_BIG_ENOUGH" > "HOL4Base.arithmetic.EXP_ALWAYS_BIG_ENOUGH"
"EXP_ADD" > "Power.power_add"
"EXP_1" > "HOL4Base.arithmetic.EXP_1"
"EXP" > "HOL4Compat.EXP"
"EXISTS_GREATEST" > "HOL4Base.arithmetic.EXISTS_GREATEST"
"EVEN_OR_ODD" > "HOL4Base.arithmetic.EVEN_OR_ODD"
"EVEN_ODD_EXISTS" > "HOL4Base.arithmetic.EVEN_ODD_EXISTS"
"EVEN_ODD" > "HOL4Base.arithmetic.EVEN_ODD"
"EVEN_MULT" > "HOL4Base.arithmetic.EVEN_MULT"
"EVEN_EXISTS" > "HOL4Base.arithmetic.EVEN_EXISTS"
"EVEN_DOUBLE" > "HOL4Base.arithmetic.EVEN_DOUBLE"
"EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
"EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
"EVEN" > "HOL4Base.arithmetic.EVEN"
"EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
"EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
"EQ_LESS_EQ" > "Orderings.order_eq_iff"
"EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
"EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
"DIV_UNIQUE" > "HOL4Base.arithmetic.DIV_UNIQUE"
"DIV_P" > "HOL4Base.arithmetic.DIV_P"
"DIV_ONE" > "Divides.div_1"
"DIV_MULT" > "HOL4Base.arithmetic.DIV_MULT"
"DIV_LESS_EQ" > "HOL4Base.arithmetic.DIV_LESS_EQ"
"DIV_LESS" > "Divides.div_less_dividend"
"DIV_DIV_DIV_MULT" > "HOL4Base.arithmetic.DIV_DIV_DIV_MULT"
"DIVMOD_ID" > "HOL4Base.arithmetic.DIVMOD_ID"
"DIVISION" > "HOL4Compat.DIVISION"
"DA" > "HOL4Base.arithmetic.DA"
"COMPLETE_INDUCTION" > "Nat.less_induct"
"CANCEL_SUB" > "NatArith.eq_diff_iff"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
"ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
"ADD_SUC" > "Nat.add_Suc_right"
"ADD_SUB" > "Nat.diff_add_inverse2"
"ADD_MONO_LESS_EQ" > "Nat.nat_add_left_cancel_le"
"ADD_INV_0_EQ" > "HOL4Base.arithmetic.ADD_INV_0_EQ"
"ADD_INV_0" > "Nat.add_eq_self_zero"
"ADD_EQ_SUB" > "HOL4Base.arithmetic.ADD_EQ_SUB"
"ADD_EQ_1" > "HOL4Base.arithmetic.ADD_EQ_1"
"ADD_EQ_0" > "Nat.add_is_0"
"ADD_DIV_ADD_DIV" > "HOL4Base.arithmetic.ADD_DIV_ADD_DIV"
"ADD_COMM" > "Finite_Set.AC_add.f.AC_2"
"ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
"ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
"ADD_0" > "Finite_Set.AC_add.f_e.ident"
"ADD1" > "Presburger.Suc_plus1"
"ADD" > "HOL4Compat.ADD"
end