Structure combinatoricsTheory
signature combinatoricsTheory =
sig
type thm = Thm.thm
(* Definitions *)
val MDILATE_def : thm
val PROD : thm
val PROD_ACC_DEF : thm
val arrange_def : thm
val choose_def : thm
val interleave_def : thm
val lcm_upto_def : thm
val leibniz_def : thm
val leibniz_zigzag_def : thm
val list_count_def : thm
val list_lcm_def : thm
val monocoloured_def : thm
val multicoloured_def : thm
val necklace_def : thm
val perm_count_def : thm
val perm_def : thm
val perm_set_def : thm
val recordtype_triple_seldef_a_def : thm
val recordtype_triple_seldef_a_fupd_def : thm
val recordtype_triple_seldef_b_def : thm
val recordtype_triple_seldef_b_fupd_def : thm
val recordtype_triple_seldef_c_def : thm
val recordtype_triple_seldef_c_fupd_def : thm
val rotate_def : thm
val set_lcm_def : thm
val sub_count_def : thm
val sub_sets_def : thm
val triple_TY_DEF : thm
val triple_case_def : thm
val triple_size_def : thm
val triplet_def : thm
val turn_def : thm
(* Theorems *)
val CARD_LIST_TO_SET_EQ : thm
val DILATE_0_0 : thm
val DILATE_0_CONS : thm
val DILATE_0_EL : thm
val DILATE_0_EQ_NIL : thm
val DILATE_0_LAST : thm
val DILATE_0_LENGTH : thm
val DILATE_0_LENGTH_LOWER : thm
val DILATE_0_LENGTH_UPPER : thm
val DILATE_0_SUC : thm
val DILATE_CONS : thm
val DILATE_NIL : thm
val DILATE_SING : thm
val DILATE_def : thm
val DILATE_ind : thm
val EL_ALL_PROPERTY : thm
val EL_MAP3 : thm
val EVERY_ELEMENT_PROPERTY : thm
val EVERY_LT_IMP_EVERY_LE : thm
val EVERY_MONOTONIC_MAP : thm
val EXISTS_triple : thm
val FILTER_EL_NEXT_IDX : thm
val FINITE_SURJ_IFF : thm
val FORALL_triple : thm
val FUNPOW_cons_eq_map_0 : thm
val FUNPOW_cons_eq_map_1 : thm
val FUNPOW_cons_head : thm
val FUNSET_ALT : thm
val GENLIST_MONO_DEC : thm
val GENLIST_MONO_INC : thm
val GENLIST_binomial_index_shift : thm
val INJ_IFF_BIJ_IMAGE : thm
val INJ_IMAGE_BIJ_IFF : thm
val INJ_IMAGE_IFF : thm
val LENGTH_MAP3 : thm
val LIST_TO_SET_REDUCTION : thm
val LUPDATE_APPEND_0 : thm
val LUPDATE_APPEND_0_1 : thm
val LUPDATE_APPEND_1 : thm
val LUPDATE_DIFF_SPOT : thm
val LUPDATE_EL : thm
val LUPDATE_LEN : thm
val LUPDATE_SAME_SPOT : thm
val MAP2_LE : thm
val MAP3 : thm
val MAP3_DEF : thm
val MAP3_IND : thm
val MAP3_LE : thm
val MAP_LE : thm
val MAX_LIST_MONO_MAP : thm
val MDILATE_0 : thm
val MDILATE_1 : thm
val MDILATE_CONS : thm
val MDILATE_EL : thm
val MDILATE_EQ_NIL : thm
val MDILATE_LAST : thm
val MDILATE_LENGTH : thm
val MDILATE_LENGTH_LOWER : thm
val MDILATE_LENGTH_UPPER : thm
val MDILATE_NIL : thm
val MDILATE_SING : thm
val MEM_MAP2 : thm
val MEM_MAP2_LOWER : thm
val MEM_MAP2_UPPER : thm
val MEM_MAP3 : thm
val MEM_MAP3_LOWER : thm
val MEM_MAP3_UPPER : thm
val MEM_MAP_LOWER : thm
val MEM_MAP_UPPER : thm
val MIN_LIST_MONO_MAP : thm
val MONO_LIST_TO_SET : thm
val PAD_LEFT_0 : thm
val PAD_LEFT_BY_LEFT : thm
val PAD_LEFT_BY_RIGHT : thm
val PAD_LEFT_CONS : thm
val PAD_LEFT_EQ_NIL : thm
val PAD_LEFT_ID : thm
val PAD_LEFT_LAST : thm
val PAD_LEFT_LENGTH : thm
val PAD_LEFT_NIL : thm
val PAD_LEFT_NIL_EQ : thm
val PAD_RIGHT_0 : thm
val PAD_RIGHT_BY_LEFT : thm
val PAD_RIGHT_BY_RIGHT : thm
val PAD_RIGHT_CONS : thm
val PAD_RIGHT_EQ_NIL : thm
val PAD_RIGHT_ID : thm
val PAD_RIGHT_LENGTH : thm
val PAD_RIGHT_NIL : thm
val PAD_RIGHT_NIL_EQ : thm
val PAD_RIGHT_SNOC : thm
val POSITIVE_THM : thm
val PROD_ACC_PROD_LEM : thm
val PROD_ACC_SUM_LEM : thm
val PROD_APPEND : thm
val PROD_CONS : thm
val PROD_CONSTANT : thm
val PROD_EQ_0 : thm
val PROD_GENLIST_K : thm
val PROD_IMAGE_eq_PROD_MAP_SET_TO_LIST : thm
val PROD_MAP_FOLDL : thm
val PROD_NIL : thm
val PROD_POS : thm
val PROD_POS_ALT : thm
val PROD_PROD_ACC : thm
val PROD_SING : thm
val PROD_SNOC : thm
val PROD_SQUARING_LIST : thm
val PROD_eq_1 : thm
val PROD_eval : thm
val SUM_ADD_GENLIST : thm
val SUM_CONS : thm
val SUM_CONSTANT : thm
val SUM_DECOMPOSE_FIRST : thm
val SUM_DECOMPOSE_FIRST_LAST : thm
val SUM_DECOMPOSE_LAST : thm
val SUM_DOUBLING_LIST : thm
val SUM_EQ_0 : thm
val SUM_GENLIST : thm
val SUM_GENLIST_APPEND : thm
val SUM_GENLIST_K : thm
val SUM_GENLIST_MOD : thm
val SUM_GENLIST_REVERSE : thm
val SUM_IMAGE_count : thm
val SUM_IMAGE_upto : thm
val SUM_LE : thm
val SUM_LEFT_ADD_DISTRIB : thm
val SUM_LE_EL : thm
val SUM_LE_MEM : thm
val SUM_LE_SUM_EL : thm
val SUM_LOWER : thm
val SUM_MAP2_K : thm
val SUM_MAP2_UPPER : thm
val SUM_MAP3_K : thm
val SUM_MAP3_UPPER : thm
val SUM_MAP_K : thm
val SUM_MAP_K_LE : thm
val SUM_MAP_LE : thm
val SUM_MAP_LT : thm
val SUM_MAP_UPPER : thm
val SUM_MOD : thm
val SUM_MONO_MAP : thm
val SUM_MONO_MAP2 : thm
val SUM_MONO_MAP3 : thm
val SUM_MULT : thm
val SUM_NIL : thm
val SUM_RIGHT_ADD_DISTRIB : thm
val SUM_SING : thm
val SUM_UPPER : thm
val SURJ_CARD_IMAGE_EQ : thm
val arithmetic_sum_eqn : thm
val arithmetic_sum_eqn_alt : thm
val arrange_0_n : thm
val arrange_alt : thm
val arrange_eq_0 : thm
val arrange_eqn : thm
val arrange_formula : thm
val arrange_formula2 : thm
val arrange_n_0 : thm
val arrange_n_n : thm
val arrange_n_n_alt : thm
val beta_0_n : thm
val beta_alt : thm
val beta_divides_beta_factor : thm
val beta_eq_0 : thm
val beta_eqn : thm
val beta_horizontal_0 : thm
val beta_horizontal_alt : thm
val beta_horizontal_element : thm
val beta_horizontal_eqn : thm
val beta_horizontal_len : thm
val beta_horizontal_mem : thm
val beta_horizontal_mem_iff : thm
val beta_horizontal_member : thm
val beta_less_0 : thm
val beta_n_0 : thm
val beta_pos : thm
val beta_sym : thm
val big_lcm_corner_transform : thm
val big_lcm_count_lower_bound : thm
val big_lcm_eq_list_lcm : thm
val big_lcm_ge_max : thm
val big_lcm_lower_bound : thm
val big_lcm_natural_eqn : thm
val big_lcm_non_decreasing : thm
val big_lcm_row_transform : thm
val big_lcm_seg_transform : thm
val bij_eq_card : thm
val bij_eq_card_eq : thm
val bij_eq_count : thm
val bij_eq_empty : thm
val bij_eq_equiv_on : thm
val bij_eq_finite : thm
val bij_eq_refl : thm
val bij_eq_sym : thm
val bij_eq_trans : thm
val bij_iff_preimage_card_eq_1 : thm
val bij_preimage_sing : thm
val binomial_0_n : thm
val binomial_1_n : thm
val binomial_alt : thm
val binomial_compute : thm
val binomial_def : thm
val binomial_eq_0 : thm
val binomial_fact : thm
val binomial_formula : thm
val binomial_formula2 : thm
val binomial_formula3 : thm
val binomial_horizontal_0 : thm
val binomial_horizontal_element : thm
val binomial_horizontal_len : thm
val binomial_horizontal_max : thm
val binomial_horizontal_mem : thm
val binomial_horizontal_mem_iff : thm
val binomial_horizontal_member : thm
val binomial_horizontal_pos : thm
val binomial_horizontal_pos_alt : thm
val binomial_horizontal_sum : thm
val binomial_iff : thm
val binomial_ind : thm
val binomial_index_shift : thm
val binomial_is_integer : thm
val binomial_less_0 : thm
val binomial_max : thm
val binomial_middle_by_stirling : thm
val binomial_middle_upper_bound : thm
val binomial_mod_zero : thm
val binomial_mod_zero_alt : thm
val binomial_monotone : thm
val binomial_n_0 : thm
val binomial_n_1 : thm
val binomial_n_k : thm
val binomial_n_n : thm
val binomial_pos : thm
val binomial_product_identity : thm
val binomial_range_shift : thm
val binomial_range_shift_alt : thm
val binomial_recurrence : thm
val binomial_right : thm
val binomial_right_eqn : thm
val binomial_row_max : thm
val binomial_sum : thm
val binomial_sum_alt : thm
val binomial_sym : thm
val binomial_term_merge_x : thm
val binomial_term_merge_y : thm
val binomial_thm : thm
val binomial_thm_alt : thm
val binomial_thm_prime : thm
val binomial_up : thm
val binomial_up_eqn : thm
val choose_0_n : thm
val choose_1_n : thm
val choose_alt : thm
val choose_eq_0 : thm
val choose_eqn : thm
val choose_n_0 : thm
val choose_n_1 : thm
val choose_n_n : thm
val choose_recurrence : thm
val choose_sum_over_all : thm
val choose_sum_over_count : thm
val count_power_partition : thm
val datatype_triple : thm
val divides_binomials_imp_prime : thm
val feq_set_equiv : thm
val finite_surj_inj_iff : thm
val gcd_prime_product_property : thm
val geometric_sum_eqn : thm
val geometric_sum_eqn_alt : thm
val head_turn : thm
val head_turn_exp : thm
val inj_iff_preimage_card_le_1 : thm
val inj_preimage_empty_or_sing : thm
val interleave_alt : thm
val interleave_card : thm
val interleave_count_inj : thm
val interleave_disjoint : thm
val interleave_distinct : thm
val interleave_distinct_alt : thm
val interleave_element : thm
val interleave_eq : thm
val interleave_finite : thm
val interleave_has_cons : thm
val interleave_length : thm
val interleave_nil : thm
val interleave_not_empty : thm
val interleave_revert : thm
val interleave_revert_count : thm
val interleave_set : thm
val interleave_set_alt : thm
val lcm_lower_bound : thm
val lcm_lower_bound_by_big_lcm : thm
val lcm_lower_bound_by_big_lcm_stirling : thm
val lcm_lower_bound_by_list_lcm : thm
val lcm_lower_bound_by_list_lcm_stirling : thm
val lcm_prime_product_property : thm
val lcm_run_0 : thm
val lcm_run_1 : thm
val lcm_run_alt : thm
val lcm_run_beta_divisor : thm
val lcm_run_bound_recurrence : thm
val lcm_run_by_FOLDL : thm
val lcm_run_by_FOLDR : thm
val lcm_run_by_beta_horizontal : thm
val lcm_run_divides_property : thm
val lcm_run_divides_property_alt : thm
val lcm_run_divisors : thm
val lcm_run_even_lower : thm
val lcm_run_even_lower_alt : thm
val lcm_run_leibniz_divisor : thm
val lcm_run_lower : thm
val lcm_run_lower_better : thm
val lcm_run_lower_better_iff : thm
val lcm_run_lower_even : thm
val lcm_run_lower_even_iff : thm
val lcm_run_lower_good : thm
val lcm_run_lower_odd : thm
val lcm_run_lower_odd_iff : thm
val lcm_run_lower_simple : thm
val lcm_run_monotone : thm
val lcm_run_odd_factor : thm
val lcm_run_odd_lower : thm
val lcm_run_odd_lower_alt : thm
val lcm_run_pos : thm
val lcm_run_small : thm
val lcm_run_suc : thm
val lcm_run_upper_bound : thm
val lcm_upto_0 : thm
val lcm_upto_1 : thm
val lcm_upto_SUC : thm
val lcm_upto_alt : thm
val lcm_upto_compute : thm
val lcm_upto_divisors : thm
val lcm_upto_eq_list_lcm : thm
val lcm_upto_leibniz_divisor : thm
val lcm_upto_lower : thm
val lcm_upto_lower_better : thm
val lcm_upto_lower_even : thm
val lcm_upto_lower_odd : thm
val lcm_upto_monotone : thm
val lcm_upto_pos : thm
val lcm_upto_small : thm
val leibniz_0_n : thm
val leibniz_alt : thm
val leibniz_binomial_identity : thm
val leibniz_col_arm_0 : thm
val leibniz_col_arm_1 : thm
val leibniz_col_arm_cons : thm
val leibniz_col_arm_el : thm
val leibniz_col_arm_len : thm
val leibniz_col_arm_n_0 : thm
val leibniz_col_arm_wriggle_row_arm : thm
val leibniz_col_def : thm
val leibniz_col_eq_natural : thm
val leibniz_def_alt : thm
val leibniz_divides_leibniz_factor : thm
val leibniz_eq_0 : thm
val leibniz_eqn : thm
val leibniz_formula : thm
val leibniz_horizontal_0 : thm
val leibniz_horizontal_alt : thm
val leibniz_horizontal_average : thm
val leibniz_horizontal_average_eqn : thm
val leibniz_horizontal_divisor : thm
val leibniz_horizontal_el : thm
val leibniz_horizontal_element : thm
val leibniz_horizontal_head : thm
val leibniz_horizontal_lcm_alt : thm
val leibniz_horizontal_lcm_lower : thm
val leibniz_horizontal_len : thm
val leibniz_horizontal_mem : thm
val leibniz_horizontal_mem_iff : thm
val leibniz_horizontal_member : thm
val leibniz_horizontal_member_divides : thm
val leibniz_horizontal_pos : thm
val leibniz_horizontal_pos_alt : thm
val leibniz_horizontal_sum : thm
val leibniz_horizontal_sum_eqn : thm
val leibniz_horizontal_wriggle : thm
val leibniz_horizontal_wriggle_step : thm
val leibniz_horizontal_zigzag : thm
val leibniz_lcm_exchange : thm
val leibniz_lcm_invariance : thm
val leibniz_lcm_property : thm
val leibniz_less_0 : thm
val leibniz_middle_lower : thm
val leibniz_monotone : thm
val leibniz_n_0 : thm
val leibniz_n_k : thm
val leibniz_n_n : thm
val leibniz_pos : thm
val leibniz_property : thm
val leibniz_recurrence : thm
val leibniz_right : thm
val leibniz_right_alt : thm
val leibniz_right_entry : thm
val leibniz_right_eqn : thm
val leibniz_row_def : thm
val leibniz_seg_arm_0 : thm
val leibniz_seg_arm_1 : thm
val leibniz_seg_arm_el : thm
val leibniz_seg_arm_head : thm
val leibniz_seg_arm_len : thm
val leibniz_seg_arm_n_0 : thm
val leibniz_seg_arm_wriggle_row_arm : thm
val leibniz_seg_arm_wriggle_step : thm
val leibniz_seg_arm_zigzag_step : thm
val leibniz_seg_def : thm
val leibniz_sym : thm
val leibniz_triplet_0 : thm
val leibniz_triplet_lcm : thm
val leibniz_triplet_member : thm
val leibniz_triplet_property : thm
val leibniz_up : thm
val leibniz_up_0 : thm
val leibniz_up_alt : thm
val leibniz_up_cons : thm
val leibniz_up_entry : thm
val leibniz_up_eqn : thm
val leibniz_up_lcm_eq_horizontal_lcm : thm
val leibniz_up_len : thm
val leibniz_up_mem : thm
val leibniz_up_pos : thm
val leibniz_up_wriggle_horizontal : thm
val leibniz_up_wriggle_horizontal_alt : thm
val leibniz_vertical_0 : thm
val leibniz_vertical_alt : thm
val leibniz_vertical_divisor : thm
val leibniz_vertical_lcm_lower : thm
val leibniz_vertical_len : thm
val leibniz_vertical_mem : thm
val leibniz_vertical_not_nil : thm
val leibniz_vertical_pos : thm
val leibniz_vertical_pos_alt : thm
val leibniz_vertical_snoc : thm
val leibniz_wriggle_refl : thm
val leibniz_wriggle_tail : thm
val leibniz_wriggle_trans : thm
val leibniz_zigzag_tail : thm
val leibniz_zigzag_wriggle : thm
val listRangeINC_MONO_INC : thm
val listRangeINC_PROD : thm
val listRangeINC_PROD_pos : thm
val listRangeLHI_MONO_INC : thm
val listRangeLHI_PROD : thm
val listRangeLHI_PROD_pos : thm
val list_count_0_n : thm
val list_count_alt : thm
val list_count_by_image : thm
val list_count_element : thm
val list_count_element_alt : thm
val list_count_element_perm_set_not_empty : thm
val list_count_element_set_card : thm
val list_count_eq_empty : thm
val list_count_eqn : thm
val list_count_finite : thm
val list_count_n_0 : thm
val list_count_n_n : thm
val list_count_set_eq_class : thm
val list_count_set_eq_class_card : thm
val list_count_set_map_bij : thm
val list_count_set_map_element : thm
val list_count_set_map_inj : thm
val list_count_set_map_surj : thm
val list_count_set_partititon_element_card : thm
val list_count_subset : thm
val list_lcm_absorption : thm
val list_lcm_append : thm
val list_lcm_append_3 : thm
val list_lcm_by_FOLDL : thm
val list_lcm_by_FOLDR : thm
val list_lcm_cons : thm
val list_lcm_divisor_lcm_pair : thm
val list_lcm_eq_if_set_eq : thm
val list_lcm_ge_max : thm
val list_lcm_is_common_multiple : thm
val list_lcm_is_least_common_multiple : thm
val list_lcm_lower_bound : thm
val list_lcm_lower_bound_alt : thm
val list_lcm_lower_by_lcm_pair : thm
val list_lcm_map_times : thm
val list_lcm_nil : thm
val list_lcm_nonempty_lower : thm
val list_lcm_nonempty_lower_alt : thm
val list_lcm_nub : thm
val list_lcm_nub_eq_if_set_eq : thm
val list_lcm_pos : thm
val list_lcm_pos_alt : thm
val list_lcm_prime_factor : thm
val list_lcm_prime_factor_member : thm
val list_lcm_reverse : thm
val list_lcm_sing : thm
val list_lcm_snoc : thm
val list_lcm_suc : thm
val list_lcm_upper_by_common_multiple : thm
val list_lcm_wriggle : thm
val list_lcm_zigzag : thm
val list_length_eq_sum : thm
val list_length_le_sum : thm
val list_product_prime_factor : thm
val monocoloured_0 : thm
val monocoloured_0_card : thm
val monocoloured_1 : thm
val monocoloured_card : thm
val monocoloured_card_eqn : thm
val monocoloured_element : thm
val monocoloured_empty : thm
val monocoloured_eqn : thm
val monocoloured_finite : thm
val monocoloured_mono : thm
val monocoloured_necklace : thm
val monocoloured_subset : thm
val monocoloured_suc : thm
val multi_mono_disjoint : thm
val multi_mono_exhaust : thm
val multicoloured_0 : thm
val multicoloured_1 : thm
val multicoloured_card : thm
val multicoloured_card_eqn : thm
val multicoloured_element : thm
val multicoloured_empty : thm
val multicoloured_finite : thm
val multicoloured_n_0 : thm
val multicoloured_n_1 : thm
val multicoloured_necklace : thm
val multicoloured_nonempty : thm
val multicoloured_not_monocoloured : thm
val multicoloured_not_monocoloured_iff : thm
val multicoloured_or_monocoloured : thm
val multicoloured_subset : thm
val necklace_0 : thm
val necklace_1 : thm
val necklace_1_monocoloured : thm
val necklace_card : thm
val necklace_colors : thm
val necklace_element : thm
val necklace_empty : thm
val necklace_eqn : thm
val necklace_finite : thm
val necklace_length : thm
val necklace_not_nil : thm
val necklace_property : thm
val necklace_suc : thm
val nub_all_distinct : thm
val nub_cons : thm
val nub_nil : thm
val nub_sing : thm
val over_bij : thm
val over_inj : thm
val over_surj : thm
val pairwise_coprime_prod_set_divides : thm
val pairwise_coprime_prod_set_eq_set_lcm : thm
val perm_0 : thm
val perm_1 : thm
val perm_alt : thm
val perm_count_0 : thm
val perm_count_1 : thm
val perm_count_element : thm
val perm_count_element_length : thm
val perm_count_element_no_self : thm
val perm_count_eqn : thm
val perm_count_finite : thm
val perm_count_interleave_card : thm
val perm_count_interleave_disjoint : thm
val perm_count_interleave_finite : thm
val perm_count_interleave_inj : thm
val perm_count_subset : thm
val perm_count_suc : thm
val perm_count_suc_alt : thm
val perm_eq_fact : thm
val perm_set_bij_eq_perm_count : thm
val perm_set_card : thm
val perm_set_card_alt : thm
val perm_set_element : thm
val perm_set_empty : thm
val perm_set_eq_empty_sing : thm
val perm_set_finite : thm
val perm_set_has_self_list : thm
val perm_set_list_not_empty : thm
val perm_set_map_bij : thm
val perm_set_map_element : thm
val perm_set_map_inj : thm
val perm_set_map_surj : thm
val perm_set_not_empty : thm
val perm_set_perm_count : thm
val perm_set_sing : thm
val perm_suc : thm
val perm_suc_alt : thm
val power_predecessor_eqn : thm
val prime_divides_binomials : thm
val prime_divides_binomials_alt : thm
val prime_divisor_property : thm
val prime_iff_divides_binomials : thm
val prime_iff_divides_binomials_alt : thm
val prod_1_to_n_eq_fact_n : thm
val rotate_0 : thm
val rotate_add : thm
val rotate_full : thm
val rotate_lcancel : thm
val rotate_nil : thm
val rotate_rcancel : thm
val rotate_same_length : thm
val rotate_same_set : thm
val rotate_shift_element : thm
val rotate_suc : thm
val set_lcm_empty : thm
val set_lcm_eq_big_lcm : thm
val set_lcm_eq_list_lcm : thm
val set_lcm_insert : thm
val set_lcm_is_common_multiple : thm
val set_lcm_is_least_common_multiple : thm
val set_lcm_nonempty : thm
val set_lcm_sing : thm
val sub_count_0_n : thm
val sub_count_alt : thm
val sub_count_count_inj : thm
val sub_count_disjoint : thm
val sub_count_element : thm
val sub_count_element_finite : thm
val sub_count_element_no_self : thm
val sub_count_eq_empty : thm
val sub_count_eqn : thm
val sub_count_equiv_class : thm
val sub_count_finite : thm
val sub_count_insert : thm
val sub_count_insert_card : thm
val sub_count_n_0 : thm
val sub_count_n_1 : thm
val sub_count_n_n : thm
val sub_count_subset : thm
val sub_count_union : thm
val sub_sets_element : thm
val sub_sets_equiv_class : thm
val sub_sets_sub_count : thm
val sum_1_to_n_double : thm
val sum_1_to_n_eq_tri_n : thm
val sum_1_to_n_eqn : thm
val surj_iff_preimage_card_not_0 : thm
val surj_preimage_not_empty : thm
val tail_turn : thm
val triple_11 : thm
val triple_Axiom : thm
val triple_accessors : thm
val triple_accfupds : thm
val triple_case_cong : thm
val triple_case_eq : thm
val triple_component_equality : thm
val triple_fn_updates : thm
val triple_fupdcanon : thm
val triple_fupdcanon_comp : thm
val triple_fupdfupds : thm
val triple_fupdfupds_comp : thm
val triple_induction : thm
val triple_literal_11 : thm
val triple_literal_nchotomy : thm
val triple_nchotomy : thm
val triple_updates_eq_literal : thm
val turn_eq_nil : thm
val turn_exp_0 : thm
val turn_exp_1 : thm
val turn_exp_2 : thm
val turn_exp_SUC : thm
val turn_exp_length : thm
val turn_exp_suc : thm
val turn_length : thm
val turn_nil : thm
val turn_not_nil : thm
val turn_snoc : thm
(*
[number] Parent theory of "combinatorics"
[MDILATE_def] Definition
⊢ (∀e n. MDILATE e n [] = []) ∧
∀e n h t.
MDILATE e n (h::t) =
if t = [] then [h] else h::GENLIST (K e) (PRE n) ⧺ MDILATE e n t
[PROD] Definition
⊢ PROD [] = 1 ∧ ∀h t. PROD (h::t) = h * PROD t
[PROD_ACC_DEF] Definition
⊢ (∀acc. PROD_ACC [] acc = acc) ∧
∀h t acc. PROD_ACC (h::t) acc = PROD_ACC t (h * acc)
[arrange_def] Definition
⊢ ∀n k. n arrange k = CARD (list_count n k)
[choose_def] Definition
⊢ ∀n k. n choose k = CARD (sub_count n k)
[interleave_def] Definition
⊢ ∀x ls.
x interleave ls =
IMAGE (λk. TAKE k ls ⧺ x::DROP k ls) (upto (LENGTH ls))
[lcm_upto_def] Definition
⊢ lcm_upto 0 = 1 ∧ ∀n. lcm_upto (SUC n) = lcm (SUC n) (lcm_upto n)
[leibniz_def] Definition
⊢ ∀n k. leibniz n k = (n + 1) * binomial n k
[leibniz_zigzag_def] Definition
⊢ ∀p1 p2.
p1 zigzag p2 ⇔
∃n k x y. p1 = x ⧺ [tb; ta] ⧺ y ∧ p2 = x ⧺ [tb; tc] ⧺ y
[list_count_def] Definition
⊢ ∀n k.
list_count n k =
{ls | ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ LENGTH ls = k}
[list_lcm_def] Definition
⊢ list_lcm [] = 1 ∧ ∀h t. list_lcm (h::t) = lcm h (list_lcm t)
[monocoloured_def] Definition
⊢ ∀n a.
monocoloured n a =
{ls | ls ∈ necklace n a ∧ (ls ≠ [] ⇒ SING (set ls))}
[multicoloured_def] Definition
⊢ ∀n a. multicoloured n a = necklace n a DIFF monocoloured n a
[necklace_def] Definition
⊢ ∀n a. necklace n a = {ls | LENGTH ls = n ∧ set ls ⊆ count a}
[perm_count_def] Definition
⊢ ∀n. perm_count n = {ls | ALL_DISTINCT ls ∧ set ls = count n}
[perm_def] Definition
⊢ ∀n. perm n = CARD (perm_count n)
[perm_set_def] Definition
⊢ ∀s. perm_set s = {ls | ALL_DISTINCT ls ∧ set ls = s}
[recordtype_triple_seldef_a_def] Definition
⊢ ∀n n0 n1. (triple n n0 n1).a = n
[recordtype_triple_seldef_a_fupd_def] Definition
⊢ ∀f n n0 n1. triple n n0 n1 with a updated_by f = triple (f n) n0 n1
[recordtype_triple_seldef_b_def] Definition
⊢ ∀n n0 n1. (triple n n0 n1).b = n0
[recordtype_triple_seldef_b_fupd_def] Definition
⊢ ∀f n n0 n1. triple n n0 n1 with b updated_by f = triple n (f n0) n1
[recordtype_triple_seldef_c_def] Definition
⊢ ∀n n0 n1. (triple n n0 n1).c = n1
[recordtype_triple_seldef_c_fupd_def] Definition
⊢ ∀f n n0 n1. triple n n0 n1 with c updated_by f = triple n n0 (f n1)
[rotate_def] Definition
⊢ ∀n l. rotate n l = DROP n l ⧺ TAKE n l
[set_lcm_def] Definition
⊢ ∀s. set_lcm s = list_lcm (SET_TO_LIST s)
[sub_count_def] Definition
⊢ ∀n k. sub_count n k = {s | s ⊆ count n ∧ CARD s = k}
[sub_sets_def] Definition
⊢ ∀P k. sub_sets P k = {s | s ⊆ P ∧ CARD s = k}
[triple_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('triple').
(∀a0'.
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR 0 (a0,a1,a2)
(λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
$var$('triple') a0') ⇒
$var$('triple') a0') rep
[triple_case_def] Definition
⊢ ∀a0 a1 a2 f. triple_CASE (triple a0 a1 a2) f = f a0 a1 a2
[triple_size_def] Definition
⊢ ∀a0 a1 a2. triple_size (triple a0 a1 a2) = 1 + (a0 + (a1 + a2))
[triplet_def] Definition
⊢ ∀n k.
triplet n k =
<|a := leibniz n k; b := leibniz (n + 1) k;
c := leibniz (n + 1) (k + 1)|>
[turn_def] Definition
⊢ ∀l. turn l = if l = [] then [] else LAST l::FRONT l
[CARD_LIST_TO_SET_EQ] Theorem
⊢ ∀l. CARD (set l) = LENGTH (nub l)
[DILATE_0_0] Theorem
⊢ ∀l e. DILATE e 0 0 l = l
[DILATE_0_CONS] Theorem
⊢ ∀n h t e.
DILATE e 0 n (h::t) =
if t = [] then [h] else h::(GENLIST (K e) n ⧺ DILATE e 0 n t)
[DILATE_0_EL] Theorem
⊢ ∀l e n k.
k < LENGTH (DILATE e 0 n l) ⇒
EL k (DILATE e 0 n l) =
if k MOD SUC n = 0 then EL (k DIV SUC n) l else e
[DILATE_0_EQ_NIL] Theorem
⊢ ∀l e n. DILATE e 0 n l = [] ⇔ l = []
[DILATE_0_LAST] Theorem
⊢ ∀l e n. LAST (DILATE e 0 n l) = LAST l
[DILATE_0_LENGTH] Theorem
⊢ ∀l e n.
LENGTH (DILATE e 0 n l) =
if l = [] then 0 else SUC (SUC n * PRE (LENGTH l))
[DILATE_0_LENGTH_LOWER] Theorem
⊢ ∀l e n. LENGTH l ≤ LENGTH (DILATE e 0 n l)
[DILATE_0_LENGTH_UPPER] Theorem
⊢ ∀l e n. LENGTH (DILATE e 0 n l) ≤ SUC (SUC n * PRE (LENGTH l))
[DILATE_0_SUC] Theorem
⊢ ∀l e n. DILATE e 0 (SUC n) l = DILATE e n 1 (DILATE e 0 n l)
[DILATE_CONS] Theorem
⊢ ∀n m h t e.
DILATE e n m (h::t) =
if t = [] then [h]
else h::(TAKE n t ⧺ GENLIST (K e) m ⧺ DILATE e n m (DROP n t))
[DILATE_NIL] Theorem
⊢ ∀n m e. DILATE e n m [] = []
[DILATE_SING] Theorem
⊢ ∀n m h e. DILATE e n m [h] = [h]
[DILATE_def] Theorem
⊢ (∀n m e. DILATE e n m [] = []) ∧
(∀n m h e. DILATE e n m [h] = [h]) ∧
∀v9 v8 n m h e.
DILATE e n m (h::v8::v9) =
h::
(TAKE n (v8::v9) ⧺ GENLIST (K e) m ⧺
DILATE e n m (DROP n (v8::v9)))
[DILATE_ind] Theorem
⊢ ∀P. (∀e n m. P e n m []) ∧ (∀e n m h. P e n m [h]) ∧
(∀e n m h v8 v9.
P e n m (DROP n (v8::v9)) ⇒ P e n m (h::v8::v9)) ⇒
∀v v1 v2 v3. P v v1 v2 v3
[EL_ALL_PROPERTY] Theorem
⊢ ∀h1 t1 h2 t2 P.
LENGTH (h1::t1) = LENGTH (h2::t2) ∧
(∀k. k < LENGTH (h1::t1) ⇒ P (EL k (h1::t1)) (EL k (h2::t2))) ⇒
P h1 h2 ∧ ∀k. k < LENGTH t1 ⇒ P (EL k t1) (EL k t2)
[EL_MAP3] Theorem
⊢ ∀lx ly lz n.
n < MIN (MIN (LENGTH lx) (LENGTH ly)) (LENGTH lz) ⇒
∀f. EL n (MAP3 f lx ly lz) = f (EL n lx) (EL n ly) (EL n lz)
[EVERY_ELEMENT_PROPERTY] Theorem
⊢ ∀p R. EVERY (λc. c ∈ R) p ⇒ ∀k. k < LENGTH p ⇒ EL k p ∈ R
[EVERY_LT_IMP_EVERY_LE] Theorem
⊢ ∀ls n. EVERY (λj. j < n) ls ⇒ EVERY (λj. j ≤ n) ls
[EVERY_MONOTONIC_MAP] Theorem
⊢ ∀l f P Q. (∀x. P x ⇒ (Q ∘ f) x) ∧ EVERY P l ⇒ EVERY Q (MAP f l)
[EXISTS_triple] Theorem
⊢ ∀P. (∃t. P t) ⇔ ∃n1 n0 n. P <|a := n1; b := n0; c := n|>
[FILTER_EL_NEXT_IDX] Theorem
⊢ ∀P ls l1 l2 l3 x y.
(let
fs = FILTER P ls
in
ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ⇒
(findi y fs = 1 + findi x fs ⇔ FILTER P l2 = []))
[FINITE_SURJ_IFF] Theorem
⊢ ∀f s t.
FINITE t ⇒ (SURJ f s t ⇔ CARD (IMAGE f s) = CARD t ∧ over f s t)
[FORALL_triple] Theorem
⊢ ∀P. (∀t. P t) ⇔ ∀n1 n0 n. P <|a := n1; b := n0; c := n|>
[FUNPOW_cons_eq_map_0] Theorem
⊢ ∀f u n.
FUNPOW (λls. f (HD ls)::ls) n [u] =
MAP (λj. FUNPOW f j u) (n downto 0)
[FUNPOW_cons_eq_map_1] Theorem
⊢ ∀f u n.
0 < n ⇒
FUNPOW (λls. f (HD ls)::ls) (n − 1) [f u] =
MAP (λj. FUNPOW f j u) (n downto 1)
[FUNPOW_cons_head] Theorem
⊢ ∀f n ls. HD (FUNPOW (λls. f (HD ls)::ls) n ls) = FUNPOW f n (HD ls)
[FUNSET_ALT] Theorem
⊢ ∀P Q. FUNSET P Q = {f | over f P Q}
[GENLIST_MONO_DEC] Theorem
⊢ ∀f n. RMONO f ⇒ MONO_DEC (GENLIST f n)
[GENLIST_MONO_INC] Theorem
⊢ ∀f n. MONO f ⇒ MONO_INC (GENLIST f n)
[GENLIST_binomial_index_shift] Theorem
⊢ ∀n x y.
GENLIST ((λk. binomial n k * x ** SUC (n − k) * y ** k) ∘ SUC) n =
GENLIST (λk. binomial n (SUC k) * x ** (n − k) * y ** SUC k) n
[INJ_IFF_BIJ_IMAGE] Theorem
⊢ ∀f s t. over f s t ⇒ (INJ f s t ⇔ BIJ f s (IMAGE f s))
[INJ_IMAGE_BIJ_IFF] Theorem
⊢ ∀f s t. INJ f s t ⇔ BIJ f s (IMAGE f s) ∧ over f s t
[INJ_IMAGE_IFF] Theorem
⊢ ∀f s t. INJ f s t ⇔ INJ f s (IMAGE f s) ∧ over f s t
[LENGTH_MAP3] Theorem
⊢ ∀lx ly lz f.
LENGTH (MAP3 f lx ly lz) =
MIN (MIN (LENGTH lx) (LENGTH ly)) (LENGTH lz)
[LIST_TO_SET_REDUCTION] Theorem
⊢ ∀l1 l2 h.
¬MEM h l1 ∧ set (h::l1) = set l2 ⇒
∃p1 p2.
¬MEM h p1 ∧ ¬MEM h p2 ∧ nub l2 = p1 ⧺ [h] ⧺ p2 ∧
set l1 = set (p1 ⧺ p2)
[LUPDATE_APPEND_0] Theorem
⊢ ∀ls a h t. LUPDATE a (LENGTH ls) (ls ⧺ h::t) = ls ⧺ a::t
[LUPDATE_APPEND_0_1] Theorem
⊢ ∀ls a b h k t.
LUPDATE b (LENGTH ls + 1) (LUPDATE a (LENGTH ls) (ls ⧺ h::k::t)) =
ls ⧺ a::b::t
[LUPDATE_APPEND_1] Theorem
⊢ ∀ls b h k t.
LUPDATE b (LENGTH ls + 1) (ls ⧺ h::k::t) = ls ⧺ h::b::t
[LUPDATE_DIFF_SPOT] Theorem
⊢ ∀ls m n p q.
m ≠ n ⇒
LUPDATE q n (LUPDATE p m ls) = LUPDATE p m (LUPDATE q n ls)
[LUPDATE_EL] Theorem
⊢ ∀e n l p.
p < LENGTH l ⇒ EL p (LUPDATE e n l) = if p = n then e else EL p l
[LUPDATE_LEN] Theorem
⊢ ∀e n l. LENGTH (LUPDATE e n l) = LENGTH l
[LUPDATE_SAME_SPOT] Theorem
⊢ ∀ls n p q. LUPDATE q n (LUPDATE p n ls) = LUPDATE q n ls
[MAP2_LE] Theorem
⊢ ∀f g.
(∀x y. f x y ≤ g x y) ⇒
∀lx ly n. EL n (MAP2 f lx ly) ≤ EL n (MAP2 g lx ly)
[MAP3] Theorem
⊢ (∀f. MAP3 f [] [] [] = []) ∧
∀f h1 t1 h2 t2 h3 t3.
MAP3 f (h1::t1) (h2::t2) (h3::t3) = f h1 h2 h3::MAP3 f t1 t2 t3
[MAP3_DEF] Theorem
⊢ (∀t3 t2 t1 h3 h2 h1 f.
MAP3 f (h1::t1) (h2::t2) (h3::t3) = f h1 h2 h3::MAP3 f t1 t2 t3) ∧
(∀z y f. MAP3 f [] y z = []) ∧
(∀z v5 v4 f. MAP3 f (v4::v5) [] z = []) ∧
∀v5 v4 v13 v12 f. MAP3 f (v4::v5) (v12::v13) [] = []
[MAP3_IND] Theorem
⊢ ∀P. (∀f h1 t1 h2 t2 h3 t3.
P f t1 t2 t3 ⇒ P f (h1::t1) (h2::t2) (h3::t3)) ∧
(∀f y z. P f [] y z) ∧ (∀f v4 v5 z. P f (v4::v5) [] z) ∧
(∀f v4 v5 v12 v13. P f (v4::v5) (v12::v13) []) ⇒
∀v v1 v2 v3. P v v1 v2 v3
[MAP3_LE] Theorem
⊢ ∀f g.
(∀x y z. f x y z ≤ g x y z) ⇒
∀lx ly lz n. EL n (MAP3 f lx ly lz) ≤ EL n (MAP3 g lx ly lz)
[MAP_LE] Theorem
⊢ ∀f g. (∀x. f x ≤ g x) ⇒ ∀ls n. EL n (MAP f ls) ≤ EL n (MAP g ls)
[MAX_LIST_MONO_MAP] Theorem
⊢ ∀f. MONO f ⇒ ∀ls. ls ≠ [] ⇒ MAX_LIST (MAP f ls) = f (MAX_LIST ls)
[MDILATE_0] Theorem
⊢ ∀l e. MDILATE e 0 l = l
[MDILATE_1] Theorem
⊢ ∀l e. MDILATE e 1 l = l
[MDILATE_CONS] Theorem
⊢ ∀e n h t.
MDILATE e n (h::t) =
if t = [] then [h] else h::GENLIST (K e) (PRE n) ⧺ MDILATE e n t
[MDILATE_EL] Theorem
⊢ ∀l e n k.
k < LENGTH (MDILATE e n l) ⇒
EL k (MDILATE e n l) =
if n = 0 then EL k l
else if k MOD n = 0 then EL (k DIV n) l
else e
[MDILATE_EQ_NIL] Theorem
⊢ ∀l e n. MDILATE e n l = [] ⇔ l = []
[MDILATE_LAST] Theorem
⊢ ∀l e n. LAST (MDILATE e n l) = LAST l
[MDILATE_LENGTH] Theorem
⊢ ∀l e n.
LENGTH (MDILATE e n l) =
if n = 0 then LENGTH l
else if l = [] then 0
else SUC (n * PRE (LENGTH l))
[MDILATE_LENGTH_LOWER] Theorem
⊢ ∀l e n. LENGTH l ≤ LENGTH (MDILATE e n l)
[MDILATE_LENGTH_UPPER] Theorem
⊢ ∀l e n. 0 < n ⇒ LENGTH (MDILATE e n l) ≤ SUC (n * PRE (LENGTH l))
[MDILATE_NIL] Theorem
⊢ ∀e n. MDILATE e n [] = []
[MDILATE_SING] Theorem
⊢ ∀e n x. MDILATE e n [x] = [x]
[MEM_MAP2] Theorem
⊢ ∀f x l1 l2.
MEM x (MAP2 f l1 l2) ⇒
∃y1 y2. x = f y1 y2 ∧ MEM y1 l1 ∧ MEM y2 l2
[MEM_MAP2_LOWER] Theorem
⊢ ∀f. MONO2 f ⇒
∀lx ly e.
MEM e (MAP2 f lx ly) ⇒ f (MIN_LIST lx) (MIN_LIST ly) ≤ e
[MEM_MAP2_UPPER] Theorem
⊢ ∀f. MONO2 f ⇒
∀lx ly e.
MEM e (MAP2 f lx ly) ⇒ e ≤ f (MAX_LIST lx) (MAX_LIST ly)
[MEM_MAP3] Theorem
⊢ ∀f x l1 l2 l3.
MEM x (MAP3 f l1 l2 l3) ⇒
∃y1 y2 y3. x = f y1 y2 y3 ∧ MEM y1 l1 ∧ MEM y2 l2 ∧ MEM y3 l3
[MEM_MAP3_LOWER] Theorem
⊢ ∀f. MONO3 f ⇒
∀lx ly lz e.
MEM e (MAP3 f lx ly lz) ⇒
f (MIN_LIST lx) (MIN_LIST ly) (MIN_LIST lz) ≤ e
[MEM_MAP3_UPPER] Theorem
⊢ ∀f. MONO3 f ⇒
∀lx ly lz e.
MEM e (MAP3 f lx ly lz) ⇒
e ≤ f (MAX_LIST lx) (MAX_LIST ly) (MAX_LIST lz)
[MEM_MAP_LOWER] Theorem
⊢ ∀f. MONO f ⇒ ∀ls e. MEM e (MAP f ls) ⇒ f (MIN_LIST ls) ≤ e
[MEM_MAP_UPPER] Theorem
⊢ ∀f. MONO f ⇒ ∀ls e. MEM e (MAP f ls) ⇒ e ≤ f (MAX_LIST ls)
[MIN_LIST_MONO_MAP] Theorem
⊢ ∀f. MONO f ⇒ ∀ls. ls ≠ [] ⇒ MIN_LIST (MAP f ls) = f (MIN_LIST ls)
[MONO_LIST_TO_SET] Theorem
⊢ ∀x. set [x] = {x}
[PAD_LEFT_0] Theorem
⊢ ∀l c. PAD_LEFT c 0 l = l
[PAD_LEFT_BY_LEFT] Theorem
⊢ ∀ls c n. PAD_LEFT c n ls = PAD_LEFT c (n − LENGTH ls) [] ⧺ ls
[PAD_LEFT_BY_RIGHT] Theorem
⊢ ∀ls c n. PAD_LEFT c n ls = PAD_RIGHT c (n − LENGTH ls) [] ⧺ ls
[PAD_LEFT_CONS] Theorem
⊢ ∀l n. LENGTH l ≤ n ⇒ ∀c. PAD_LEFT c (SUC n) l = c::PAD_LEFT c n l
[PAD_LEFT_EQ_NIL] Theorem
⊢ ∀l c n. PAD_LEFT c n l = [] ⇔ l = [] ∧ n = 0
[PAD_LEFT_ID] Theorem
⊢ ∀l c n. n ≤ LENGTH l ⇒ PAD_LEFT c n l = l
[PAD_LEFT_LAST] Theorem
⊢ ∀l c n. l ≠ [] ⇒ LAST (PAD_LEFT c n l) = LAST l
[PAD_LEFT_LENGTH] Theorem
⊢ ∀n c s. LENGTH (PAD_LEFT c n s) = MAX n (LENGTH s)
[PAD_LEFT_NIL] Theorem
⊢ ∀n c. PAD_LEFT c n [] = GENLIST (K c) n
[PAD_LEFT_NIL_EQ] Theorem
⊢ ∀n c. 0 < n ⇒ PAD_LEFT c n [] = PAD_LEFT c n [c]
[PAD_RIGHT_0] Theorem
⊢ ∀l c. PAD_RIGHT c 0 l = l
[PAD_RIGHT_BY_LEFT] Theorem
⊢ ∀ls c n. PAD_RIGHT c n ls = ls ⧺ PAD_LEFT c (n − LENGTH ls) []
[PAD_RIGHT_BY_RIGHT] Theorem
⊢ ∀ls c n. PAD_RIGHT c n ls = ls ⧺ PAD_RIGHT c (n − LENGTH ls) []
[PAD_RIGHT_CONS] Theorem
⊢ ∀h t c n. h::PAD_RIGHT c n t = PAD_RIGHT c (SUC n) (h::t)
[PAD_RIGHT_EQ_NIL] Theorem
⊢ ∀l c n. PAD_RIGHT c n l = [] ⇔ l = [] ∧ n = 0
[PAD_RIGHT_ID] Theorem
⊢ ∀l c n. n ≤ LENGTH l ⇒ PAD_RIGHT c n l = l
[PAD_RIGHT_LENGTH] Theorem
⊢ ∀n c s. LENGTH (PAD_RIGHT c n s) = MAX n (LENGTH s)
[PAD_RIGHT_NIL] Theorem
⊢ ∀n c. PAD_RIGHT c n [] = GENLIST (K c) n
[PAD_RIGHT_NIL_EQ] Theorem
⊢ ∀n c. 0 < n ⇒ PAD_RIGHT c n [] = PAD_RIGHT c n [c]
[PAD_RIGHT_SNOC] Theorem
⊢ ∀l n.
LENGTH l ≤ n ⇒
∀c. PAD_RIGHT c (SUC n) l = SNOC c (PAD_RIGHT c n l)
[POSITIVE_THM] Theorem
⊢ ∀ls. EVERY_POSITIVE ls ⇔ POSITIVE ls
[PROD_ACC_PROD_LEM] Theorem
⊢ ∀L n. PROD_ACC L n = PROD L * n
[PROD_ACC_SUM_LEM] Theorem
⊢ ∀L n. PROD_ACC L n = PROD L * n
[PROD_APPEND] Theorem
⊢ ∀l1 l2. PROD (l1 ⧺ l2) = PROD l1 * PROD l2
[PROD_CONS] Theorem
⊢ ∀h t. PROD (h::t) = h * PROD t
[PROD_CONSTANT] Theorem
⊢ ∀n x. PROD (GENLIST (λj. x) n) = x ** n
[PROD_EQ_0] Theorem
⊢ ∀l. PROD l = 0 ⇔ MEM 0 l
[PROD_GENLIST_K] Theorem
⊢ ∀m n. PROD (GENLIST (K m) n) = m ** n
[PROD_IMAGE_eq_PROD_MAP_SET_TO_LIST] Theorem
⊢ ∀s. FINITE s ⇒ ∀f. Π f s = PROD (MAP f (SET_TO_LIST s))
[PROD_MAP_FOLDL] Theorem
⊢ ∀ls f. PROD (MAP f ls) = FOLDL (λa e. a * f e) 1 ls
[PROD_NIL] Theorem
⊢ PROD [] = 1
[PROD_POS] Theorem
⊢ ∀l. EVERY_POSITIVE l ⇒ 0 < PROD l
[PROD_POS_ALT] Theorem
⊢ ∀l. POSITIVE l ⇒ 0 < PROD l
[PROD_PROD_ACC] Theorem
⊢ ∀L. PROD L = PROD_ACC L 1
[PROD_SING] Theorem
⊢ ∀n. PROD [n] = n
[PROD_SNOC] Theorem
⊢ ∀x l. PROD (SNOC x l) = PROD l * x
[PROD_SQUARING_LIST] Theorem
⊢ ∀m n. PROD (GENLIST (λj. n ** 2 ** j) m) = n ** tops 2 m
[PROD_eq_1] Theorem
⊢ ∀ls. PROD ls = 1 ⇔ ∀x. MEM x ls ⇒ x = 1
[PROD_eval] Theorem
⊢ ∀ls. PROD ls = if ls = [] then 1 else HD ls * PROD (TL ls)
[SUM_ADD_GENLIST] Theorem
⊢ ∀a b n.
SUM (GENLIST a n) + SUM (GENLIST b n) =
SUM (GENLIST (λk. a k + b k) n)
[SUM_CONS] Theorem
⊢ ∀h t. SUM (h::t) = h + SUM t
[SUM_CONSTANT] Theorem
⊢ ∀n x. SUM (GENLIST (λj. x) n) = n * x
[SUM_DECOMPOSE_FIRST] Theorem
⊢ ∀f n. SUM (GENLIST f (SUC n)) = f 0 + SUM (GENLIST (f ∘ SUC) n)
[SUM_DECOMPOSE_FIRST_LAST] Theorem
⊢ ∀f n.
0 < n ⇒
SUM (GENLIST f (SUC n)) =
f 0 + SUM (GENLIST (f ∘ SUC) (PRE n)) + f n
[SUM_DECOMPOSE_LAST] Theorem
⊢ ∀f n. SUM (GENLIST f (SUC n)) = SUM (GENLIST f n) + f n
[SUM_DOUBLING_LIST] Theorem
⊢ ∀m n. SUM (GENLIST (λj. n * 2 ** j) m) = n * tops 2 m
[SUM_EQ_0] Theorem
⊢ ∀l. SUM l = 0 ⇔ EVERY (λx. x = 0) l
[SUM_GENLIST] Theorem
⊢ ∀f n. SUM (GENLIST f n) = ∑ f (count n)
[SUM_GENLIST_APPEND] Theorem
⊢ ∀a b n.
SUM (GENLIST a n ⧺ GENLIST b n) = SUM (GENLIST (λk. a k + b k) n)
[SUM_GENLIST_K] Theorem
⊢ ∀m n. SUM (GENLIST (K m) n) = m * n
[SUM_GENLIST_MOD] Theorem
⊢ ∀n. 0 < n ⇒
∀f. SUM (GENLIST ((λk. f k) ∘ SUC) (PRE n)) MOD n =
SUM (GENLIST ((λk. f k MOD n) ∘ SUC) (PRE n)) MOD n
[SUM_GENLIST_REVERSE] Theorem
⊢ ∀f n. SUM (GENLIST (λj. f (n − j)) n) = SUM (MAP f [1 .. n])
[SUM_IMAGE_count] Theorem
⊢ ∀f n. ∑ f (count n) = SUM (MAP f [0 ..< n])
[SUM_IMAGE_upto] Theorem
⊢ ∀f n. ∑ f (upto n) = SUM (MAP f [0 .. n])
[SUM_LE] Theorem
⊢ ∀l1 l2.
LENGTH l1 = LENGTH l2 ∧ (∀k. k < LENGTH l1 ⇒ EL k l1 ≤ EL k l2) ⇒
SUM l1 ≤ SUM l2
[SUM_LEFT_ADD_DISTRIB] Theorem
⊢ ∀s m n. SUM s * (m + n) = SUM (MAP ($* m) s) + SUM (MAP ($* n) s)
[SUM_LE_EL] Theorem
⊢ ∀l n. n < LENGTH l ⇒ EL n l ≤ SUM l
[SUM_LE_MEM] Theorem
⊢ ∀l x. MEM x l ⇒ x ≤ SUM l
[SUM_LE_SUM_EL] Theorem
⊢ ∀l m n. m < n ∧ n < LENGTH l ⇒ EL m l + EL n l ≤ SUM l
[SUM_LOWER] Theorem
⊢ ∀ls. MIN_LIST ls * LENGTH ls ≤ SUM ls
[SUM_MAP2_K] Theorem
⊢ ∀lx ly c.
SUM (MAP2 (λx y. c) lx ly) = c * LENGTH (MAP2 (λx y. c) lx ly)
[SUM_MAP2_UPPER] Theorem
⊢ ∀f. MONO2 f ⇒
∀lx ly.
SUM (MAP2 f lx ly) ≤
f (MAX_LIST lx) (MAX_LIST ly) * LENGTH (MAP2 f lx ly)
[SUM_MAP3_K] Theorem
⊢ ∀lx ly lz c.
SUM (MAP3 (λx y z. c) lx ly lz) =
c * LENGTH (MAP3 (λx y z. c) lx ly lz)
[SUM_MAP3_UPPER] Theorem
⊢ ∀f. MONO3 f ⇒
∀lx ly lz.
SUM (MAP3 f lx ly lz) ≤
f (MAX_LIST lx) (MAX_LIST ly) (MAX_LIST lz) *
LENGTH (MAP3 f lx ly lz)
[SUM_MAP_K] Theorem
⊢ ∀ls c. SUM (MAP (K c) ls) = c * LENGTH ls
[SUM_MAP_K_LE] Theorem
⊢ ∀ls a b. a ≤ b ⇒ SUM (MAP (K a) ls) ≤ SUM (MAP (K b) ls)
[SUM_MAP_LE] Theorem
⊢ ∀f g ls. EVERY (λx. f x ≤ g x) ls ⇒ SUM (MAP f ls) ≤ SUM (MAP g ls)
[SUM_MAP_LT] Theorem
⊢ ∀f g ls.
EVERY (λx. f x < g x) ls ∧ ls ≠ [] ⇒
SUM (MAP f ls) < SUM (MAP g ls)
[SUM_MAP_UPPER] Theorem
⊢ ∀f. MONO f ⇒ ∀ls. SUM (MAP f ls) ≤ f (MAX_LIST ls) * LENGTH ls
[SUM_MOD] Theorem
⊢ ∀n. 0 < n ⇒ ∀l. SUM l MOD n = SUM (MAP (λx. x MOD n) l) MOD n
[SUM_MONO_MAP] Theorem
⊢ ∀f1 f2. (∀x. f1 x ≤ f2 x) ⇒ ∀ls. SUM (MAP f1 ls) ≤ SUM (MAP f2 ls)
[SUM_MONO_MAP2] Theorem
⊢ ∀f1 f2.
(∀x y. f1 x y ≤ f2 x y) ⇒
∀lx ly. SUM (MAP2 f1 lx ly) ≤ SUM (MAP2 f2 lx ly)
[SUM_MONO_MAP3] Theorem
⊢ ∀f1 f2.
(∀x y z. f1 x y z ≤ f2 x y z) ⇒
∀lx ly lz. SUM (MAP3 f1 lx ly lz) ≤ SUM (MAP3 f2 lx ly lz)
[SUM_MULT] Theorem
⊢ ∀s k. k * SUM s = SUM (MAP ($* k) s)
[SUM_NIL] Theorem
⊢ SUM [] = 0
[SUM_RIGHT_ADD_DISTRIB] Theorem
⊢ ∀s m n. (m + n) * SUM s = SUM (MAP ($* m) s) + SUM (MAP ($* n) s)
[SUM_SING] Theorem
⊢ ∀n. SUM [n] = n
[SUM_UPPER] Theorem
⊢ ∀ls. SUM ls ≤ MAX_LIST ls * LENGTH ls
[SURJ_CARD_IMAGE_EQ] Theorem
⊢ ∀f s t.
FINITE t ∧ over f s t ⇒ (SURJ f s t ⇔ CARD (IMAGE f s) = CARD t)
[arithmetic_sum_eqn] Theorem
⊢ ∀n. SUM [1 ..< n] = HALF (n * (n − 1))
[arithmetic_sum_eqn_alt] Theorem
⊢ ∀n. SUM [1 .. n] = HALF (n * (n + 1))
[arrange_0_n] Theorem
⊢ ∀n. 0 < n ⇒ 0 arrange n = 0
[arrange_alt] Theorem
⊢ ∀n k. n arrange k = (n choose k) * FACT k
[arrange_eq_0] Theorem
⊢ ∀n k. n arrange k = 0 ⇔ n < k
[arrange_eqn] Theorem
⊢ ∀n k. n arrange k = (n choose k) * perm k
[arrange_formula] Theorem
⊢ ∀n k. n arrange k = binomial n k * FACT k
[arrange_formula2] Theorem
⊢ ∀n k. k ≤ n ⇒ n arrange k = FACT n DIV FACT (n − k)
[arrange_n_0] Theorem
⊢ ∀n. n arrange 0 = 1
[arrange_n_n] Theorem
⊢ ∀n. n arrange n = perm n
[arrange_n_n_alt] Theorem
⊢ ∀n. n arrange n = FACT n
[beta_0_n] Theorem
⊢ ∀n. beta 0 n = 0
[beta_alt] Theorem
⊢ ∀n k. 0 < n ∧ 0 < k ⇒ beta n k = leibniz (n − 1) (k − 1)
[beta_divides_beta_factor] Theorem
⊢ ∀m n k. k ≤ m ∧ m ≤ n ⇒ beta n k divides beta m k * binomial n m
[beta_eq_0] Theorem
⊢ ∀n k. beta n k = 0 ⇔ k = 0 ∨ n < k
[beta_eqn] Theorem
⊢ ∀n k. beta (n + 1) (k + 1) = leibniz n k
[beta_horizontal_0] Theorem
⊢ beta_horizontal 0 = []
[beta_horizontal_alt] Theorem
⊢ ∀n. 0 < n ⇒ beta_horizontal n = leibniz_horizontal (n − 1)
[beta_horizontal_element] Theorem
⊢ ∀n k. k < n ⇒ EL k (beta_horizontal n) = beta n (k + 1)
[beta_horizontal_eqn] Theorem
⊢ ∀n. beta_horizontal (n + 1) = leibniz_horizontal n
[beta_horizontal_len] Theorem
⊢ ∀n. LENGTH (beta_horizontal n) = n
[beta_horizontal_mem] Theorem
⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ MEM (beta n k) (beta_horizontal n)
[beta_horizontal_mem_iff] Theorem
⊢ ∀n k. MEM (beta n k) (beta_horizontal n) ⇔ 0 < k ∧ k ≤ n
[beta_horizontal_member] Theorem
⊢ ∀n x. MEM x (beta_horizontal n) ⇔ ∃k. 0 < k ∧ k ≤ n ∧ x = beta n k
[beta_less_0] Theorem
⊢ ∀n k. n < k ⇒ beta n k = 0
[beta_n_0] Theorem
⊢ ∀n. beta n 0 = 0
[beta_pos] Theorem
⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ 0 < beta n k
[beta_sym] Theorem
⊢ ∀n k. k ≤ n ⇒ beta n k = beta n (n − k + 1)
[big_lcm_corner_transform] Theorem
⊢ ∀n. big_lcm (leibniz_col (n + 1)) = big_lcm (leibniz_row n (n + 1))
[big_lcm_count_lower_bound] Theorem
⊢ ∀f n.
(∀x. x ∈ count (n + 1) ⇒ 0 < f x) ⇒
SUM (GENLIST f (n + 1)) ≤
(n + 1) * big_lcm (IMAGE f (count (n + 1)))
[big_lcm_eq_list_lcm] Theorem
⊢ ∀l. big_lcm (set l) = list_lcm l
[big_lcm_ge_max] Theorem
⊢ ∀s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < x) ⇒ MAX_SET s ≤ big_lcm s
[big_lcm_lower_bound] Theorem
⊢ ∀n. 2 ** n ≤ big_lcm (natural (n + 1))
[big_lcm_natural_eqn] Theorem
⊢ ∀n. big_lcm (natural (n + 1)) =
(n + 1) * big_lcm (IMAGE (binomial n) (count (n + 1)))
[big_lcm_non_decreasing] Theorem
⊢ ∀n. big_lcm (natural n) ≤ big_lcm (natural (n + 1))
[big_lcm_row_transform] Theorem
⊢ ∀n h.
lcm (leibniz (n + 1) 0) (big_lcm (leibniz_row n h)) =
big_lcm (leibniz_row (n + 1) (h + 1))
[big_lcm_seg_transform] Theorem
⊢ ∀n k h.
lcm (leibniz (n + 1) k) (big_lcm (leibniz_seg n k h)) =
big_lcm (leibniz_seg (n + 1) k (h + 1))
[bij_eq_card] Theorem
⊢ ∀s t. s =b= t ∧ (FINITE s ∨ FINITE t) ⇒ CARD s = CARD t
[bij_eq_card_eq] Theorem
⊢ ∀s t. FINITE s ∧ FINITE t ⇒ (s =b= t ⇔ CARD s = CARD t)
[bij_eq_count] Theorem
⊢ ∀s. FINITE s ⇒ s =b= count (CARD s)
[bij_eq_empty] Theorem
⊢ ∀s t. s =b= t ⇒ (s = ∅ ⇔ t = ∅)
[bij_eq_equiv_on] Theorem
⊢ ∀P. (λs t. s =b= t) equiv_on P
[bij_eq_finite] Theorem
⊢ ∀s t. s =b= t ⇒ (FINITE s ⇔ FINITE t)
[bij_eq_refl] Theorem
⊢ ∀s. s =b= s
[bij_eq_sym] Theorem
⊢ ∀s t. s =b= t ⇔ t =b= s
[bij_eq_trans] Theorem
⊢ ∀s t u. s =b= t ∧ t =b= u ⇒ s =b= u
[bij_iff_preimage_card_eq_1] Theorem
⊢ ∀f s t.
FINITE s ∧ over f s t ⇒
(BIJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) = 1)
[bij_preimage_sing] Theorem
⊢ ∀f s t. BIJ f s t ⇔ over f s t ∧ ∀y. y ∈ t ⇒ SING (preimage f s y)
[binomial_0_n] Theorem
⊢ ∀n. binomial 0 n = if n = 0 then 1 else 0
[binomial_1_n] Theorem
⊢ ∀n. binomial 1 n = if 1 < n then 0 else 1
[binomial_alt] Theorem
⊢ ∀n k.
binomial n 0 = 1 ∧ binomial 0 (k + 1) = 0 ∧
binomial (n + 1) (k + 1) = binomial n k + binomial n (k + 1)
[binomial_compute] Theorem
⊢ binomial 0 0 = 1 ∧ (∀n. binomial (NUMERAL (BIT1 n)) 0 = 1) ∧
(∀n. binomial (NUMERAL (BIT2 n)) 0 = 1) ∧
(∀k. binomial 0 (NUMERAL (BIT1 k)) = 0) ∧
(∀k. binomial 0 (NUMERAL (BIT2 k)) = 0) ∧
(∀n k.
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k)) =
binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k) − 1) +
binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k))) ∧
(∀n k.
binomial (NUMERAL (BIT2 n)) (NUMERAL (BIT1 k)) =
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k) − 1) +
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k))) ∧
(∀n k.
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT2 k)) =
binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 k)) +
binomial (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT2 k))) ∧
∀n k.
binomial (NUMERAL (BIT2 n)) (NUMERAL (BIT2 k)) =
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT1 k)) +
binomial (NUMERAL (BIT1 n)) (NUMERAL (BIT2 k))
[binomial_def] Theorem
⊢ binomial 0 0 = 1 ∧ (∀n. binomial (SUC n) 0 = 1) ∧
(∀k. binomial 0 (SUC k) = 0) ∧
∀n k. binomial (SUC n) (SUC k) = binomial n k + binomial n (SUC k)
[binomial_eq_0] Theorem
⊢ ∀n k. binomial n k = 0 ⇔ n < k
[binomial_fact] Theorem
⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV (FACT k * FACT (n − k))
[binomial_formula] Theorem
⊢ ∀n k. binomial (n + k) k * (FACT n * FACT k) = FACT (n + k)
[binomial_formula2] Theorem
⊢ ∀n k. k ≤ n ⇒ FACT n = binomial n k * (FACT (n − k) * FACT k)
[binomial_formula3] Theorem
⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV (FACT k * FACT (n − k))
[binomial_horizontal_0] Theorem
⊢ binomial_horizontal 0 = [1]
[binomial_horizontal_element] Theorem
⊢ ∀n k. k ≤ n ⇒ EL k (binomial_horizontal n) = binomial n k
[binomial_horizontal_len] Theorem
⊢ ∀n. LENGTH (binomial_horizontal n) = n + 1
[binomial_horizontal_max] Theorem
⊢ ∀n. MAX_LIST (binomial_horizontal n) = binomial n (HALF n)
[binomial_horizontal_mem] Theorem
⊢ ∀n k. k < n + 1 ⇒ MEM (binomial n k) (binomial_horizontal n)
[binomial_horizontal_mem_iff] Theorem
⊢ ∀n k. MEM (binomial n k) (binomial_horizontal n) ⇔ k ≤ n
[binomial_horizontal_member] Theorem
⊢ ∀n x. MEM x (binomial_horizontal n) ⇔ ∃k. k ≤ n ∧ x = binomial n k
[binomial_horizontal_pos] Theorem
⊢ ∀n. EVERY_POSITIVE (binomial_horizontal n)
[binomial_horizontal_pos_alt] Theorem
⊢ ∀n x. MEM x (binomial_horizontal n) ⇒ 0 < x
[binomial_horizontal_sum] Theorem
⊢ ∀n. SUM (binomial_horizontal n) = 2 ** n
[binomial_iff] Theorem
⊢ ∀f. f = binomial ⇔
∀n k.
f n 0 = 1 ∧ f 0 (k + 1) = 0 ∧
f (n + 1) (k + 1) = f n k + f n (k + 1)
[binomial_ind] Theorem
⊢ ∀P. P 0 0 ∧ (∀n. P (SUC n) 0) ∧ (∀k. P 0 (SUC k)) ∧
(∀n k. P n k ∧ P n (SUC k) ⇒ P (SUC n) (SUC k)) ⇒
∀v v1. P v v1
[binomial_index_shift] Theorem
⊢ ∀n x y.
(λk. binomial (SUC n) k * x ** (SUC n − k) * y ** k) ∘ SUC =
(λk. binomial (SUC n) (SUC k) * x ** (n − k) * y ** SUC k)
[binomial_is_integer] Theorem
⊢ ∀n k. k ≤ n ⇒ FACT k * FACT (n − k) divides FACT n
[binomial_less_0] Theorem
⊢ ∀n k. n < k ⇒ binomial n k = 0
[binomial_max] Theorem
⊢ ∀n k. binomial n k ≤ binomial n (HALF n)
[binomial_middle_by_stirling] Theorem
⊢ Stirling ⇒
∀n. 0 < n ∧ EVEN n ⇒
binomial n (HALF n) = 2 ** (n + 1) DIV SQRT (TWICE pi * n)
[binomial_middle_upper_bound] Theorem
⊢ ∀n. binomial n (HALF n) ≤ 4 ** HALF n
[binomial_mod_zero] Theorem
⊢ ∀n. 0 < n ⇒
∀k. binomial n k MOD n = 0 ⇔
∀x y. (binomial n k * x ** (n − k) * y ** k) MOD n = 0
[binomial_mod_zero_alt] Theorem
⊢ ∀n. 0 < n ⇒
((∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0) ⇔
∀x y.
SUM
(GENLIST
((λk. (binomial n k * x ** (n − k) * y ** k) MOD n) ∘
SUC) (PRE n)) =
0)
[binomial_monotone] Theorem
⊢ ∀n k. k < HALF n ⇒ binomial n k < binomial n (k + 1)
[binomial_n_0] Theorem
⊢ ∀n. binomial n 0 = 1
[binomial_n_1] Theorem
⊢ ∀n. binomial n 1 = n
[binomial_n_k] Theorem
⊢ ∀n k. k ≤ n ⇒ binomial n k = FACT n DIV FACT k DIV FACT (n − k)
[binomial_n_n] Theorem
⊢ ∀n. binomial n n = 1
[binomial_pos] Theorem
⊢ ∀n k. k ≤ n ⇒ 0 < binomial n k
[binomial_product_identity] Theorem
⊢ ∀m n k.
k ≤ m ∧ m ≤ n ⇒
binomial m k * binomial n m =
binomial n k * binomial (n − k) (m − k)
[binomial_range_shift] Theorem
⊢ ∀n. 0 < n ⇒
((∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0) ⇔
∀h. h < PRE n ⇒ binomial n (SUC h) MOD n = 0)
[binomial_range_shift_alt] Theorem
⊢ ∀n. 0 < n ⇒
((∀k. 0 < k ∧ k < n ⇒
∀x y. (binomial n k * x ** (n − k) * y ** k) MOD n = 0) ⇔
∀h. h < PRE n ⇒
∀x y.
(binomial n (SUC h) * x ** (n − SUC h) * y ** SUC h) MOD
n =
0)
[binomial_recurrence] Theorem
⊢ ∀n k. binomial (SUC n) (SUC k) = binomial n k + binomial n (SUC k)
[binomial_right] Theorem
⊢ ∀n. 0 < n ⇒
∀k. binomial n (k + 1) = (n − k) * binomial n k DIV (k + 1)
[binomial_right_eqn] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. beta n (k + 1) = (n − k) * binomial n k
[binomial_row_max] Theorem
⊢ ∀n. MAX_SET (IMAGE (binomial n) (count (n + 1))) =
binomial n (HALF n)
[binomial_sum] Theorem
⊢ ∀n. SUM (GENLIST (binomial n) (SUC n)) = 2 ** n
[binomial_sum_alt] Theorem
⊢ ∀n. SUM (binomial_horizontal n) = 2 ** n
[binomial_sym] Theorem
⊢ ∀n k. k ≤ n ⇒ binomial n k = binomial n (n − k)
[binomial_term_merge_x] Theorem
⊢ ∀n x y.
(λk. x * k) ∘ (λk. binomial n k * x ** (n − k) * y ** k) =
(λk. binomial n k * x ** SUC (n − k) * y ** k)
[binomial_term_merge_y] Theorem
⊢ ∀n x y.
(λk. y * k) ∘ (λk. binomial n k * x ** (n − k) * y ** k) =
(λk. binomial n k * x ** (n − k) * y ** SUC k)
[binomial_thm] Theorem
⊢ ∀n x y.
(x + y) ** n =
SUM (GENLIST (λk. binomial n k * x ** (n − k) * y ** k) (SUC n))
[binomial_thm_alt] Theorem
⊢ ∀n x y.
(x + y) ** n =
SUM (GENLIST (λk. binomial n k * x ** (n − k) * y ** k) (n + 1))
[binomial_thm_prime] Theorem
⊢ ∀p. prime p ⇒ ∀x y. (x + y) ** p MOD p = (x ** p + y ** p) MOD p
[binomial_up] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. binomial (n − 1) k = (n − k) * binomial n k DIV n
[binomial_up_eqn] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. n * binomial (n − 1) k = (n − k) * binomial n k
[choose_0_n] Theorem
⊢ ∀n. 0 choose n = if n = 0 then 1 else 0
[choose_1_n] Theorem
⊢ ∀n. 1 choose n = if 1 < n then 0 else 1
[choose_alt] Theorem
⊢ ∀n k.
n choose 0 = 1 ∧ 0 choose (k + 1) = 0 ∧
(n + 1) choose (k + 1) = n choose k + n choose (k + 1)
[choose_eq_0] Theorem
⊢ ∀n k. n choose k = 0 ⇔ n < k
[choose_eqn] Theorem
⊢ ∀n k. n choose k = binomial n k
[choose_n_0] Theorem
⊢ ∀n. n choose 0 = 1
[choose_n_1] Theorem
⊢ ∀n. n choose 1 = n
[choose_n_n] Theorem
⊢ ∀n. n choose n = 1
[choose_recurrence] Theorem
⊢ ∀n k. (n + 1) choose (k + 1) = n choose k + n choose (k + 1)
[choose_sum_over_all] Theorem
⊢ ∀n. SUM (MAP ($choose n) [0 .. n]) = 2 ** n
[choose_sum_over_count] Theorem
⊢ ∀n. ∑ ($choose n) (upto n) = 2 ** n
[count_power_partition] Theorem
⊢ ∀n. partition (λs t. s =b= t) (POW (count n)) =
IMAGE (sub_count n) (upto n)
[datatype_triple] Theorem
⊢ DATATYPE (record triple a b c)
[divides_binomials_imp_prime] Theorem
⊢ ∀n. 1 < n ∧ (∀k. 0 < k ∧ k < n ⇒ n divides binomial n k) ⇒ prime n
[feq_set_equiv] Theorem
⊢ ∀s. feq set equiv_on s
[finite_surj_inj_iff] Theorem
⊢ ∀f s t.
FINITE s ∧ SURJ f s t ⇒
(INJ f s t ⇔ ∀e. e ∈ IMAGE (preimage f s) t ⇒ CARD e = 1)
[gcd_prime_product_property] Theorem
⊢ ∀p m n.
prime p ∧ m divides n ∧ ¬(p * m divides n) ⇒ gcd (p * m) n = m
[geometric_sum_eqn] Theorem
⊢ ∀t n.
1 < t ⇒ SUM (MAP (λj. t ** j) [0 ..< n]) = tops t n DIV (t − 1)
[geometric_sum_eqn_alt] Theorem
⊢ ∀t n.
1 < t ⇒
SUM (MAP (λj. t ** j) [0 .. n]) = tops t (n + 1) DIV (t − 1)
[head_turn] Theorem
⊢ ∀ls. ls ≠ [] ⇒ HD (turn ls) = LAST ls
[head_turn_exp] Theorem
⊢ ∀ls n.
n < LENGTH ls ⇒
HD (turn_exp ls n) = EL (if n = 0 then 0 else (LENGTH ls − n)) ls
[inj_iff_preimage_card_le_1] Theorem
⊢ ∀f s t.
FINITE s ∧ over f s t ⇒
(INJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) ≤ 1)
[inj_preimage_empty_or_sing] Theorem
⊢ ∀f s t.
INJ f s t ⇔
over f s t ∧
∀y. y ∈ t ⇒ preimage f s y = ∅ ∨ SING (preimage f s y)
[interleave_alt] Theorem
⊢ ∀ls x.
x interleave ls = {TAKE k ls ⧺ x::DROP k ls | k | k ≤ LENGTH ls}
[interleave_card] Theorem
⊢ ∀ls x. ¬MEM x ls ⇒ CARD (x interleave ls) = 1 + LENGTH ls
[interleave_count_inj] Theorem
⊢ ∀ls x.
¬MEM x ls ⇒
INJ (λk. TAKE k ls ⧺ x::DROP k ls) (upto (LENGTH ls)) 𝕌(:α list)
[interleave_disjoint] Theorem
⊢ ∀l1 l2 x.
¬MEM x l1 ∧ l1 ≠ l2 ⇒
DISJOINT (x interleave l1) (x interleave l2)
[interleave_distinct] Theorem
⊢ ∀ls x y.
ALL_DISTINCT (x::ls) ∧ y ∈ x interleave ls ⇒ ALL_DISTINCT y
[interleave_distinct_alt] Theorem
⊢ ∀ls x y.
ALL_DISTINCT ls ∧ ¬MEM x ls ∧ y ∈ x interleave ls ⇒
ALL_DISTINCT y
[interleave_element] Theorem
⊢ ∀ls x y.
y ∈ x interleave ls ⇔
∃k. k ≤ LENGTH ls ∧ y = TAKE k ls ⧺ x::DROP k ls
[interleave_eq] Theorem
⊢ ∀n x y.
¬MEM n x ∧ ¬MEM n y ⇒ (n interleave x = n interleave y ⇔ x = y)
[interleave_finite] Theorem
⊢ ∀ls x. FINITE (x interleave ls)
[interleave_has_cons] Theorem
⊢ ∀ls x. x::ls ∈ x interleave ls
[interleave_length] Theorem
⊢ ∀ls x y. y ∈ x interleave ls ⇒ LENGTH y = 1 + LENGTH ls
[interleave_nil] Theorem
⊢ ∀x. x interleave [] = {[x]}
[interleave_not_empty] Theorem
⊢ ∀ls x. x interleave ls ≠ ∅
[interleave_revert] Theorem
⊢ ∀ls h.
ALL_DISTINCT ls ∧ MEM h ls ⇒
∃t. ALL_DISTINCT t ∧ ls ∈ h interleave t ∧
set t = set ls DELETE h
[interleave_revert_count] Theorem
⊢ ∀ls n.
ALL_DISTINCT ls ∧ set ls = upto n ⇒
∃t. ALL_DISTINCT t ∧ ls ∈ n interleave t ∧ set t = count n
[interleave_set] Theorem
⊢ ∀ls x y. y ∈ x interleave ls ⇒ set y = set (x::ls)
[interleave_set_alt] Theorem
⊢ ∀ls x y. y ∈ x interleave ls ⇒ set y = x INSERT set ls
[lcm_lower_bound] Theorem
⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)
[lcm_lower_bound_by_big_lcm] Theorem
⊢ ∀n. (n + 1) * binomial n (HALF n) ≤ big_lcm (natural (n + 1))
[lcm_lower_bound_by_big_lcm_stirling] Theorem
⊢ Stirling ∧ (∀n c. n DIV SQRT (c * (n − 1)) = SQRT (n DIV c)) ⇒
∀n. ODD n ⇒ SQRT (n DIV TWICE pi) * 2 ** n ≤ big_lcm (natural n)
[lcm_lower_bound_by_list_lcm] Theorem
⊢ ∀n. (n + 1) * binomial n (HALF n) ≤ lcm_run (n + 1)
[lcm_lower_bound_by_list_lcm_stirling] Theorem
⊢ Stirling ∧ (∀n c. n DIV SQRT (c * (n − 1)) = SQRT (n DIV c)) ⇒
∀n. ODD n ⇒ SQRT (n DIV TWICE pi) * 2 ** n ≤ lcm_run n
[lcm_prime_product_property] Theorem
⊢ ∀p m n.
prime p ∧ m divides n ∧ ¬(p * m divides n) ⇒
lcm (p * m) n = p * n
[lcm_run_0] Theorem
⊢ lcm_run 0 = 1
[lcm_run_1] Theorem
⊢ lcm_run 1 = 1
[lcm_run_alt] Theorem
⊢ ∀n. lcm_run n = lcm_run (n − 1 + 1)
[lcm_run_beta_divisor] Theorem
⊢ ∀n k. 0 < k ∧ k ≤ n ⇒ beta n k divides lcm_run n
[lcm_run_bound_recurrence] Theorem
⊢ ∀m n. n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n ≤ lcm_run m * binomial n m
[lcm_run_by_FOLDL] Theorem
⊢ ∀n. lcm_run n = FOLDL lcm 1 [1 .. n]
[lcm_run_by_FOLDR] Theorem
⊢ ∀n. lcm_run n = FOLDR lcm 1 [1 .. n]
[lcm_run_by_beta_horizontal] Theorem
⊢ ∀n. 0 < n ⇒ lcm_run n = list_lcm (beta_horizontal n)
[lcm_run_divides_property] Theorem
⊢ ∀m n.
n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n divides lcm_run m * binomial n m
[lcm_run_divides_property_alt] Theorem
⊢ ∀m n.
n ≤ TWICE m ∧ m ≤ n ⇒ lcm_run n divides binomial n m * lcm_run m
[lcm_run_divisors] Theorem
⊢ ∀n. n + 1 divides lcm_run (n + 1) ∧
lcm_run n divides lcm_run (n + 1)
[lcm_run_even_lower] Theorem
⊢ ∀n. EVEN n ⇒ HALF (n − 2) * HALF (HALF (2 ** n)) ≤ lcm_run n
[lcm_run_even_lower_alt] Theorem
⊢ ∀n. EVEN n ∧ 8 ≤ n ⇒ 2 ** n ≤ lcm_run n
[lcm_run_leibniz_divisor] Theorem
⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_run (n + 1)
[lcm_run_lower] Theorem
⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)
[lcm_run_lower_better] Theorem
⊢ ∀n. 7 ≤ n ⇒ 2 ** n ≤ lcm_run n
[lcm_run_lower_better_iff] Theorem
⊢ ∀n. 2 ** n ≤ lcm_run n ⇔ n = 0 ∨ n = 5 ∨ 7 ≤ n
[lcm_run_lower_even] Theorem
⊢ ∀n. n * 4 ** n ≤ lcm_run (TWICE (n + 1))
[lcm_run_lower_even_iff] Theorem
⊢ ∀n. EVEN n ⇒ (2 ** n ≤ lcm_run n ⇔ n = 0 ∨ 8 ≤ n)
[lcm_run_lower_good] Theorem
⊢ ∀n. 2 ** (n − 1) ≤ lcm_run n
[lcm_run_lower_odd] Theorem
⊢ ∀n. n * 4 ** n ≤ lcm_run (TWICE n + 1)
[lcm_run_lower_odd_iff] Theorem
⊢ ∀n. ODD n ⇒ (2 ** n ≤ lcm_run n ⇔ 5 ≤ n)
[lcm_run_lower_simple] Theorem
⊢ ∀n. HALF (n + 1) ≤ lcm_run n
[lcm_run_monotone] Theorem
⊢ ∀n. lcm_run n ≤ lcm_run (n + 1)
[lcm_run_odd_factor] Theorem
⊢ ∀n. 0 < n ⇒ n * leibniz (TWICE n) n divides lcm_run (TWICE n + 1)
[lcm_run_odd_lower] Theorem
⊢ ∀n. ODD n ⇒ HALF n * HALF (2 ** n) ≤ lcm_run n
[lcm_run_odd_lower_alt] Theorem
⊢ ∀n. ODD n ∧ 5 ≤ n ⇒ 2 ** n ≤ lcm_run n
[lcm_run_pos] Theorem
⊢ ∀n. 0 < lcm_run n
[lcm_run_small] Theorem
⊢ lcm_run 2 = 2 ∧ lcm_run 3 = 6 ∧ lcm_run 4 = 12 ∧ lcm_run 5 = 60 ∧
lcm_run 6 = 60 ∧ lcm_run 7 = 420 ∧ lcm_run 8 = 840 ∧
lcm_run 9 = 2520
[lcm_run_suc] Theorem
⊢ ∀n. lcm_run (n + 1) = lcm (n + 1) (lcm_run n)
[lcm_run_upper_bound] Theorem
⊢ ∀n. lcm_run n ≤ 4 ** n
[lcm_upto_0] Theorem
⊢ lcm_upto 0 = 1
[lcm_upto_1] Theorem
⊢ lcm_upto 1 = 1
[lcm_upto_SUC] Theorem
⊢ ∀n. lcm_upto (SUC n) = lcm (SUC n) (lcm_upto n)
[lcm_upto_alt] Theorem
⊢ lcm_upto 0 = 1 ∧ ∀n. lcm_upto (n + 1) = lcm (n + 1) (lcm_upto n)
[lcm_upto_compute] Theorem
⊢ lcm_upto 0 = 1 ∧
(∀n. lcm_upto (NUMERAL (BIT1 n)) =
lcm (NUMERAL (BIT1 n)) (lcm_upto (NUMERAL (BIT1 n) − 1))) ∧
∀n. lcm_upto (NUMERAL (BIT2 n)) =
lcm (NUMERAL (BIT2 n)) (lcm_upto (NUMERAL (BIT1 n)))
[lcm_upto_divisors] Theorem
⊢ ∀n. n + 1 divides lcm_upto (n + 1) ∧
lcm_upto n divides lcm_upto (n + 1)
[lcm_upto_eq_list_lcm] Theorem
⊢ ∀n. lcm_upto n = lcm_run n
[lcm_upto_leibniz_divisor] Theorem
⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_upto (n + 1)
[lcm_upto_lower] Theorem
⊢ ∀n. 2 ** n ≤ lcm_upto (n + 1)
[lcm_upto_lower_better] Theorem
⊢ ∀n. 7 ≤ n ⇒ 2 ** n ≤ lcm_upto n
[lcm_upto_lower_even] Theorem
⊢ ∀n. n * 4 ** n ≤ lcm_upto (TWICE (n + 1))
[lcm_upto_lower_odd] Theorem
⊢ ∀n. n * 4 ** n ≤ lcm_upto (TWICE n + 1)
[lcm_upto_monotone] Theorem
⊢ ∀n. lcm_upto n ≤ lcm_upto (n + 1)
[lcm_upto_pos] Theorem
⊢ ∀n. 0 < lcm_upto (n + 1)
[lcm_upto_small] Theorem
⊢ lcm_upto 2 = 2 ∧ lcm_upto 3 = 6 ∧ lcm_upto 4 = 12 ∧
lcm_upto 5 = 60 ∧ lcm_upto 6 = 60 ∧ lcm_upto 7 = 420 ∧
lcm_upto 8 = 840 ∧ lcm_upto 9 = 2520 ∧ lcm_upto 10 = 2520
[leibniz_0_n] Theorem
⊢ ∀n. leibniz 0 n = if n = 0 then 1 else 0
[leibniz_alt] Theorem
⊢ ∀n. leibniz n = (λj. (n + 1) * j) ∘ binomial n
[leibniz_binomial_identity] Theorem
⊢ ∀m n k.
k ≤ m ∧ m ≤ n ⇒
leibniz n k * binomial (n − k) (m − k) =
leibniz m k * binomial (n + 1) (m + 1)
[leibniz_col_arm_0] Theorem
⊢ ∀a b. leibniz_col_arm a b 0 = []
[leibniz_col_arm_1] Theorem
⊢ ∀a b. leibniz_col_arm a b 1 = [leibniz a b]
[leibniz_col_arm_cons] Theorem
⊢ ∀a b n.
leibniz_col_arm (a + 1) b (n + 1) =
leibniz (a + 1) b::leibniz_col_arm a b n
[leibniz_col_arm_el] Theorem
⊢ ∀n k.
k < n ⇒ ∀a b. EL k (leibniz_col_arm a b n) = leibniz (a − k) b
[leibniz_col_arm_len] Theorem
⊢ ∀a b n. LENGTH (leibniz_col_arm a b n) = n
[leibniz_col_arm_n_0] Theorem
⊢ ∀n. leibniz_col_arm n 0 (n + 1) = leibniz_up n
[leibniz_col_arm_wriggle_row_arm] Theorem
⊢ ∀a b n.
b ≤ a ∧ n ≤ a + 1 − b ⇒
leibniz_col_arm a b n wriggle leibniz_seg_arm a b n
[leibniz_col_def] Theorem
⊢ ∀h. leibniz_col h = {leibniz j 0 | j ∈ count h}
[leibniz_col_eq_natural] Theorem
⊢ ∀n. leibniz_col n = natural n
[leibniz_def_alt] Theorem
⊢ ∀n k. leibniz n k = (λj. (n + 1) * j) (binomial n k)
[leibniz_divides_leibniz_factor] Theorem
⊢ ∀m n k.
k ≤ m ∧ m ≤ n ⇒
leibniz n k divides leibniz m k * binomial (n + 1) (m + 1)
[leibniz_eq_0] Theorem
⊢ ∀n k. leibniz n k = 0 ⇔ n < k
[leibniz_eqn] Theorem
⊢ ∀n k. leibniz n k = (n + 1 − k) * binomial (n + 1) k
[leibniz_formula] Theorem
⊢ ∀n k.
k ≤ n ⇒
leibniz n k = (n + 1) * FACT n DIV (FACT k * FACT (n − k))
[leibniz_horizontal_0] Theorem
⊢ leibniz_horizontal 0 = [1]
[leibniz_horizontal_alt] Theorem
⊢ ∀n. leibniz_horizontal n =
MAP (λj. (n + 1) * j) (binomial_horizontal n)
[leibniz_horizontal_average] Theorem
⊢ ∀n. SUM (leibniz_horizontal n) DIV LENGTH (leibniz_horizontal n) =
SUM (binomial_horizontal n)
[leibniz_horizontal_average_eqn] Theorem
⊢ ∀n. SUM (leibniz_horizontal n) DIV LENGTH (leibniz_horizontal n) =
2 ** n
[leibniz_horizontal_divisor] Theorem
⊢ ∀n k. k ≤ n ⇒ leibniz n k divides list_lcm (leibniz_horizontal n)
[leibniz_horizontal_el] Theorem
⊢ ∀n k. k ≤ n ⇒ EL k (leibniz_horizontal n) = leibniz n k
[leibniz_horizontal_element] Theorem
⊢ ∀n k. k ≤ n ⇒ EL k (leibniz_horizontal n) = leibniz n k
[leibniz_horizontal_head] Theorem
⊢ ∀n. TAKE 1 (leibniz_horizontal (n + 1)) = [n + 2]
[leibniz_horizontal_lcm_alt] Theorem
⊢ ∀n. list_lcm (leibniz_horizontal n) =
(n + 1) * list_lcm (binomial_horizontal n)
[leibniz_horizontal_lcm_lower] Theorem
⊢ ∀n. 2 ** n ≤ list_lcm (leibniz_horizontal n)
[leibniz_horizontal_len] Theorem
⊢ ∀n. LENGTH (leibniz_horizontal n) = n + 1
[leibniz_horizontal_mem] Theorem
⊢ ∀n k. k ≤ n ⇒ MEM (leibniz n k) (leibniz_horizontal n)
[leibniz_horizontal_mem_iff] Theorem
⊢ ∀n k. MEM (leibniz n k) (leibniz_horizontal n) ⇔ k ≤ n
[leibniz_horizontal_member] Theorem
⊢ ∀n x. MEM x (leibniz_horizontal n) ⇔ ∃k. k ≤ n ∧ x = leibniz n k
[leibniz_horizontal_member_divides] Theorem
⊢ ∀m n x.
n ≤ TWICE m + 1 ∧ m ≤ n ∧ MEM x (leibniz_horizontal n) ⇒
x divides
list_lcm (leibniz_horizontal m) * binomial (n + 1) (m + 1)
[leibniz_horizontal_pos] Theorem
⊢ ∀n. EVERY_POSITIVE (leibniz_horizontal n)
[leibniz_horizontal_pos_alt] Theorem
⊢ ∀n x. MEM x (leibniz_horizontal n) ⇒ 0 < x
[leibniz_horizontal_sum] Theorem
⊢ ∀n. SUM (leibniz_horizontal n) =
(n + 1) * SUM (binomial_horizontal n)
[leibniz_horizontal_sum_eqn] Theorem
⊢ ∀n. SUM (leibniz_horizontal n) = (n + 1) * 2 ** n
[leibniz_horizontal_wriggle] Theorem
⊢ ∀n. [leibniz (n + 1) 0] ⧺ leibniz_horizontal n wriggle
leibniz_horizontal (n + 1)
[leibniz_horizontal_wriggle_step] Theorem
⊢ ∀n k.
k ≤ n + 1 ⇒
TAKE (k + 1) (leibniz_horizontal (n + 1)) ⧺
DROP k (leibniz_horizontal n) wriggle leibniz_horizontal (n + 1)
[leibniz_horizontal_zigzag] Theorem
⊢ ∀n k.
k ≤ n ⇒
TAKE (k + 1) (leibniz_horizontal (n + 1)) ⧺
DROP k (leibniz_horizontal n) zigzag
TAKE (k + 2) (leibniz_horizontal (n + 1)) ⧺
DROP (k + 1) (leibniz_horizontal n)
[leibniz_lcm_exchange] Theorem
⊢ ∀n. 0 < n ⇒
∀k. lcm (leibniz n k) (leibniz (n − 1) k) =
lcm (leibniz n k) (leibniz n (k + 1))
[leibniz_lcm_invariance] Theorem
⊢ ∀a b n.
b ≤ a ∧ n ≤ a + 1 − b ⇒
list_lcm (leibniz_col_arm a b n) =
list_lcm (leibniz_seg_arm a b n)
[leibniz_lcm_property] Theorem
⊢ ∀n. lcm_run (n + 1) = list_lcm (leibniz_horizontal n)
[leibniz_less_0] Theorem
⊢ ∀n k. n < k ⇒ leibniz n k = 0
[leibniz_middle_lower] Theorem
⊢ ∀n. 4 ** n ≤ leibniz (TWICE n) n
[leibniz_monotone] Theorem
⊢ ∀n k. k < HALF n ⇒ leibniz n k < leibniz n (k + 1)
[leibniz_n_0] Theorem
⊢ ∀n. leibniz n 0 = n + 1
[leibniz_n_k] Theorem
⊢ ∀n k.
0 < k ∧ k ≤ n ⇒
leibniz n k =
leibniz n (k − 1) * leibniz (n − 1) (k − 1) DIV
(leibniz n (k − 1) − leibniz (n − 1) (k − 1))
[leibniz_n_n] Theorem
⊢ ∀n. leibniz n n = n + 1
[leibniz_pos] Theorem
⊢ ∀n k. k ≤ n ⇒ 0 < leibniz n k
[leibniz_property] Theorem
⊢ ∀n. 0 < n ⇒
∀k. leibniz n k * leibniz (n − 1) k =
leibniz n (k + 1) * (leibniz n k − leibniz (n − 1) k)
[leibniz_recurrence] Theorem
⊢ ∀n. 0 < n ⇒
∀k. k < n ⇒
leibniz n (k + 1) =
leibniz n k * leibniz (n − 1) k DIV
(leibniz n k − leibniz (n − 1) k)
[leibniz_right] Theorem
⊢ ∀n. 0 < n ⇒
∀k. leibniz n (k + 1) = (n − k) * leibniz n k DIV (k + 1)
[leibniz_right_alt] Theorem
⊢ ∀n k. leibniz n (k + 1) = (n − k) * binomial (n + 1) (k + 1)
[leibniz_right_entry] Theorem
⊢ ∀n k. (k + 1) * tc = (n + 1 − k) * tb
[leibniz_right_eqn] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. (k + 1) * leibniz n (k + 1) = (n − k) * leibniz n k
[leibniz_row_def] Theorem
⊢ ∀n h. leibniz_row n h = {leibniz n j | j ∈ count h}
[leibniz_seg_arm_0] Theorem
⊢ ∀a b. leibniz_seg_arm a b 0 = []
[leibniz_seg_arm_1] Theorem
⊢ ∀a b. leibniz_seg_arm a b 1 = [leibniz a b]
[leibniz_seg_arm_el] Theorem
⊢ ∀n k.
k < n ⇒ ∀a b. EL k (leibniz_seg_arm a b n) = leibniz a (b + k)
[leibniz_seg_arm_head] Theorem
⊢ ∀a b n. TAKE 1 (leibniz_seg_arm a b (n + 1)) = [leibniz a b]
[leibniz_seg_arm_len] Theorem
⊢ ∀a b n. LENGTH (leibniz_seg_arm a b n) = n
[leibniz_seg_arm_n_0] Theorem
⊢ ∀n. leibniz_seg_arm n 0 (n + 1) = leibniz_horizontal n
[leibniz_seg_arm_wriggle_row_arm] Theorem
⊢ ∀a b n.
[leibniz (a + 1) b] ⧺ leibniz_seg_arm a b n wriggle
leibniz_seg_arm (a + 1) b (n + 1)
[leibniz_seg_arm_wriggle_step] Theorem
⊢ ∀n k.
k < n + 1 ⇒
∀a b.
TAKE (k + 1) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
DROP k (leibniz_seg_arm a b n) wriggle
leibniz_seg_arm (a + 1) b (n + 1)
[leibniz_seg_arm_zigzag_step] Theorem
⊢ ∀n k.
k < n ⇒
∀a b.
TAKE (k + 1) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
DROP k (leibniz_seg_arm a b n) zigzag
TAKE (k + 2) (leibniz_seg_arm (a + 1) b (n + 1)) ⧺
DROP (k + 1) (leibniz_seg_arm a b n)
[leibniz_seg_def] Theorem
⊢ ∀n k h. leibniz_seg n k h = {leibniz n (k + j) | j ∈ count h}
[leibniz_sym] Theorem
⊢ ∀n k. k ≤ n ⇒ leibniz n k = leibniz n (n − k)
[leibniz_triplet_0] Theorem
⊢ leibniz_up 1 zigzag leibniz_horizontal 1
[leibniz_triplet_lcm] Theorem
⊢ ∀n k. lcm tb ta = lcm tb tc
[leibniz_triplet_member] Theorem
⊢ ∀n k.
ta = leibniz n k ∧ tb = leibniz (n + 1) k ∧
tc = leibniz (n + 1) (k + 1)
[leibniz_triplet_property] Theorem
⊢ ∀n' k. ta * tb = tc * (tb − ta)
[leibniz_up] Theorem
⊢ ∀n. 0 < n ⇒
∀k. leibniz (n − 1) k = (n − k) * leibniz n k DIV (n + 1)
[leibniz_up_0] Theorem
⊢ leibniz_up 0 = [1]
[leibniz_up_alt] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. leibniz (n − 1) k = (n − k) * binomial n k
[leibniz_up_cons] Theorem
⊢ ∀n. leibniz_up (n + 1) = n + 2::leibniz_up n
[leibniz_up_entry] Theorem
⊢ ∀n k. (n + 2) * ta = (n + 1 − k) * tb
[leibniz_up_eqn] Theorem
⊢ ∀n. 0 < n ⇒ ∀k. (n + 1) * leibniz (n − 1) k = (n − k) * leibniz n k
[leibniz_up_lcm_eq_horizontal_lcm] Theorem
⊢ ∀n. list_lcm (leibniz_up n) = list_lcm (leibniz_horizontal n)
[leibniz_up_len] Theorem
⊢ ∀n. LENGTH (leibniz_up n) = n + 1
[leibniz_up_mem] Theorem
⊢ ∀n x. 0 < x ∧ x ≤ n + 1 ⇔ MEM x (leibniz_up n)
[leibniz_up_pos] Theorem
⊢ ∀n. EVERY_POSITIVE (leibniz_up n)
[leibniz_up_wriggle_horizontal] Theorem
⊢ ∀n. leibniz_up n wriggle leibniz_horizontal n
[leibniz_up_wriggle_horizontal_alt] Theorem
⊢ ∀n. leibniz_up n wriggle leibniz_horizontal n
[leibniz_vertical_0] Theorem
⊢ leibniz_vertical 0 = [1]
[leibniz_vertical_alt] Theorem
⊢ ∀n. leibniz_vertical n = GENLIST (λi. 1 + i) (n + 1)
[leibniz_vertical_divisor] Theorem
⊢ ∀n k. k ≤ n ⇒ leibniz n k divides lcm_run (n + 1)
[leibniz_vertical_lcm_lower] Theorem
⊢ ∀n. 2 ** n ≤ lcm_run (n + 1)
[leibniz_vertical_len] Theorem
⊢ ∀n. LENGTH (leibniz_vertical n) = n + 1
[leibniz_vertical_mem] Theorem
⊢ ∀n x. 0 < x ∧ x ≤ n + 1 ⇔ MEM x (leibniz_vertical n)
[leibniz_vertical_not_nil] Theorem
⊢ ∀n. leibniz_vertical n ≠ []
[leibniz_vertical_pos] Theorem
⊢ ∀n. EVERY_POSITIVE (leibniz_vertical n)
[leibniz_vertical_pos_alt] Theorem
⊢ ∀n x. MEM x (leibniz_vertical n) ⇒ 0 < x
[leibniz_vertical_snoc] Theorem
⊢ ∀n. leibniz_vertical (n + 1) = SNOC (n + 2) (leibniz_vertical n)
[leibniz_wriggle_refl] Theorem
⊢ ∀p1. p1 wriggle p1
[leibniz_wriggle_tail] Theorem
⊢ ∀p1 p2. p1 wriggle p2 ⇒ ∀x. [x] ⧺ p1 wriggle [x] ⧺ p2
[leibniz_wriggle_trans] Theorem
⊢ ∀p1 p2 p3. p1 wriggle p2 ∧ p2 wriggle p3 ⇒ p1 wriggle p3
[leibniz_zigzag_tail] Theorem
⊢ ∀p1 p2. p1 zigzag p2 ⇒ ∀x. [x] ⧺ p1 zigzag [x] ⧺ p2
[leibniz_zigzag_wriggle] Theorem
⊢ ∀p1 p2. p1 zigzag p2 ⇒ p1 wriggle p2
[listRangeINC_MONO_INC] Theorem
⊢ ∀m n m' n'.
m' ≤ n' ∧ n' < LENGTH [m .. n] ⇒ EL m' [m .. n] ≤ EL n' [m .. n]
[listRangeINC_PROD] Theorem
⊢ ∀m n.
0 < m ∧ m ≤ n ⇒
PROD [m .. n] = PROD [1 .. n] DIV PROD [1 .. m − 1]
[listRangeINC_PROD_pos] Theorem
⊢ ∀m n. 0 < m ⇒ 0 < PROD [m .. n]
[listRangeLHI_MONO_INC] Theorem
⊢ ∀m n m' n'.
m' ≤ n' ∧ n' < LENGTH [m ..< n] ⇒
EL m' [m ..< n] ≤ EL n' [m ..< n]
[listRangeLHI_PROD] Theorem
⊢ ∀m n.
0 < m ∧ m ≤ n ⇒
PROD [m ..< n] = PROD [1 ..< n] DIV PROD [1 ..< m]
[listRangeLHI_PROD_pos] Theorem
⊢ ∀m n. 0 < m ⇒ 0 < PROD [m ..< n]
[list_count_0_n] Theorem
⊢ ∀n. 0 < n ⇒ list_count 0 n = ∅
[list_count_alt] Theorem
⊢ ∀n k.
list_count n k =
{ls | ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ CARD (set ls) = k}
[list_count_by_image] Theorem
⊢ ∀n k.
0 < k ⇒
list_count n k =
IMAGE (λls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE
[]
[list_count_element] Theorem
⊢ ∀ls n k.
ls ∈ list_count n k ⇔
ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ LENGTH ls = k
[list_count_element_alt] Theorem
⊢ ∀ls n k.
ls ∈ list_count n k ⇔
ALL_DISTINCT ls ∧ set ls ⊆ count n ∧ CARD (set ls) = k
[list_count_element_perm_set_not_empty] Theorem
⊢ ∀ls n k. ls ∈ list_count n k ⇒ perm_set (set ls) ≠ ∅
[list_count_element_set_card] Theorem
⊢ ∀ls n k. ls ∈ list_count n k ⇒ CARD (set ls) = k
[list_count_eq_empty] Theorem
⊢ ∀n k. list_count n k = ∅ ⇔ n < k
[list_count_eqn] Theorem
⊢ ∀n k.
list_count n k =
if k = 0 then {[]}
else
IMAGE (λls. if ALL_DISTINCT ls then ls else []) (necklace k n) DELETE
[]
[list_count_finite] Theorem
⊢ ∀n k. FINITE (list_count n k)
[list_count_n_0] Theorem
⊢ ∀n. list_count n 0 = {[]}
[list_count_n_n] Theorem
⊢ ∀n. list_count n n = perm_count n
[list_count_set_eq_class] Theorem
⊢ ∀ls n k.
ls ∈ list_count n k ⇒
equiv_class (feq set) (list_count n k) ls = perm_set (set ls)
[list_count_set_eq_class_card] Theorem
⊢ ∀ls n k.
ls ∈ list_count n k ⇒
CARD (equiv_class (feq set) (list_count n k) ls) = perm k
[list_count_set_map_bij] Theorem
⊢ ∀n k.
BIJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
(sub_count n k)
[list_count_set_map_element] Theorem
⊢ ∀s n k.
s ∈ partition (feq set) (list_count n k) ⇒
(set ∘ CHOICE) s ∈ sub_count n k
[list_count_set_map_inj] Theorem
⊢ ∀n k.
INJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
(sub_count n k)
[list_count_set_map_surj] Theorem
⊢ ∀n k.
SURJ (set ∘ CHOICE) (partition (feq set) (list_count n k))
(sub_count n k)
[list_count_set_partititon_element_card] Theorem
⊢ ∀n k e. e ∈ partition (feq set) (list_count n k) ⇒ CARD e = perm k
[list_count_subset] Theorem
⊢ ∀n k. list_count n k ⊆ necklace k n
[list_lcm_absorption] Theorem
⊢ ∀x l. MEM x l ⇒ list_lcm (x::l) = list_lcm l
[list_lcm_append] Theorem
⊢ ∀l1 l2. list_lcm (l1 ⧺ l2) = lcm (list_lcm l1) (list_lcm l2)
[list_lcm_append_3] Theorem
⊢ ∀l1 l2 l3.
list_lcm (l1 ⧺ l2 ⧺ l3) =
list_lcm [list_lcm l1; list_lcm l2; list_lcm l3]
[list_lcm_by_FOLDL] Theorem
⊢ ∀ls. list_lcm ls = FOLDL lcm 1 ls
[list_lcm_by_FOLDR] Theorem
⊢ ∀ls. list_lcm ls = FOLDR lcm 1 ls
[list_lcm_cons] Theorem
⊢ ∀h t. list_lcm (h::t) = lcm h (list_lcm t)
[list_lcm_divisor_lcm_pair] Theorem
⊢ ∀l x y. MEM x l ∧ MEM y l ⇒ lcm x y divides list_lcm l
[list_lcm_eq_if_set_eq] Theorem
⊢ ∀l1 l2. set l1 = set l2 ⇒ list_lcm l1 = list_lcm l2
[list_lcm_ge_max] Theorem
⊢ ∀l. POSITIVE l ⇒ MAX_LIST l ≤ list_lcm l
[list_lcm_is_common_multiple] Theorem
⊢ ∀x l. MEM x l ⇒ x divides list_lcm l
[list_lcm_is_least_common_multiple] Theorem
⊢ ∀l m. (∀x. MEM x l ⇒ x divides m) ⇒ list_lcm l divides m
[list_lcm_lower_bound] Theorem
⊢ ∀l. EVERY_POSITIVE l ⇒ SUM l ≤ LENGTH l * list_lcm l
[list_lcm_lower_bound_alt] Theorem
⊢ ∀l. POSITIVE l ⇒ SUM l ≤ LENGTH l * list_lcm l
[list_lcm_lower_by_lcm_pair] Theorem
⊢ ∀l x y. POSITIVE l ∧ MEM x l ∧ MEM y l ⇒ lcm x y ≤ list_lcm l
[list_lcm_map_times] Theorem
⊢ ∀n l.
list_lcm (MAP (λk. n * k) l) =
if l = [] then 1 else n * list_lcm l
[list_lcm_nil] Theorem
⊢ list_lcm [] = 1
[list_lcm_nonempty_lower] Theorem
⊢ ∀l. l ≠ [] ∧ EVERY_POSITIVE l ⇒ SUM l DIV LENGTH l ≤ list_lcm l
[list_lcm_nonempty_lower_alt] Theorem
⊢ ∀l. l ≠ [] ∧ POSITIVE l ⇒ SUM l DIV LENGTH l ≤ list_lcm l
[list_lcm_nub] Theorem
⊢ ∀l. list_lcm (nub l) = list_lcm l
[list_lcm_nub_eq_if_set_eq] Theorem
⊢ ∀l1 l2. set l1 = set l2 ⇒ list_lcm (nub l1) = list_lcm (nub l2)
[list_lcm_pos] Theorem
⊢ ∀l. EVERY_POSITIVE l ⇒ 0 < list_lcm l
[list_lcm_pos_alt] Theorem
⊢ ∀l. POSITIVE l ⇒ 0 < list_lcm l
[list_lcm_prime_factor] Theorem
⊢ ∀p l. prime p ∧ p divides list_lcm l ⇒ p divides PROD_SET (set l)
[list_lcm_prime_factor_member] Theorem
⊢ ∀p l. prime p ∧ p divides list_lcm l ⇒ ∃x. MEM x l ∧ p divides x
[list_lcm_reverse] Theorem
⊢ ∀l. list_lcm (REVERSE l) = list_lcm l
[list_lcm_sing] Theorem
⊢ ∀x. list_lcm [x] = x
[list_lcm_snoc] Theorem
⊢ ∀x l. list_lcm (SNOC x l) = lcm x (list_lcm l)
[list_lcm_suc] Theorem
⊢ ∀n. lcm_run (n + 1) = lcm (n + 1) (lcm_run n)
[list_lcm_upper_by_common_multiple] Theorem
⊢ ∀l m. 0 < m ∧ (∀x. MEM x l ⇒ x divides m) ⇒ list_lcm l ≤ m
[list_lcm_wriggle] Theorem
⊢ ∀p1 p2. p1 wriggle p2 ⇒ list_lcm p1 = list_lcm p2
[list_lcm_zigzag] Theorem
⊢ ∀p1 p2. p1 zigzag p2 ⇒ list_lcm p1 = list_lcm p2
[list_length_eq_sum] Theorem
⊢ ∀ls. EVERY_POSITIVE ls ∧ LENGTH ls = SUM ls ⇒ EVERY (λx. x = 1) ls
[list_length_le_sum] Theorem
⊢ ∀ls. EVERY_POSITIVE ls ⇒ LENGTH ls ≤ SUM ls
[list_product_prime_factor] Theorem
⊢ ∀p l.
prime p ∧ p divides PROD_SET (set l) ⇒ ∃x. MEM x l ∧ p divides x
[monocoloured_0] Theorem
⊢ ∀a. monocoloured 0 a = {[]}
[monocoloured_0_card] Theorem
⊢ ∀a. CARD (monocoloured 0 a) = 1
[monocoloured_1] Theorem
⊢ ∀a. monocoloured 1 a = necklace 1 a
[monocoloured_card] Theorem
⊢ ∀n a. 0 < n ⇒ CARD (monocoloured n a) = a
[monocoloured_card_eqn] Theorem
⊢ ∀n a. CARD (monocoloured n a) = if n = 0 then 1 else a
[monocoloured_element] Theorem
⊢ ∀n a ls.
ls ∈ monocoloured n a ⇔
ls ∈ necklace n a ∧ (ls ≠ [] ⇒ SING (set ls))
[monocoloured_empty] Theorem
⊢ ∀n. 0 < n ⇒ monocoloured n 0 = ∅
[monocoloured_eqn] Theorem
⊢ ∀n a.
monocoloured n a =
if n = 0 then {[]} else IMAGE (λc. GENLIST (K c) n) (count a)
[monocoloured_finite] Theorem
⊢ ∀n a. FINITE (monocoloured n a)
[monocoloured_mono] Theorem
⊢ ∀n. monocoloured n 1 = necklace n 1
[monocoloured_necklace] Theorem
⊢ ∀n a ls. ls ∈ monocoloured n a ⇒ ls ∈ necklace n a
[monocoloured_subset] Theorem
⊢ ∀n a. monocoloured n a ⊆ necklace n a
[monocoloured_suc] Theorem
⊢ ∀n a.
0 < n ⇒
monocoloured (SUC n) a =
IMAGE (λls. HD ls::ls) (monocoloured n a)
[multi_mono_disjoint] Theorem
⊢ ∀n a. DISJOINT (multicoloured n a) (monocoloured n a)
[multi_mono_exhaust] Theorem
⊢ ∀n a. necklace n a = multicoloured n a ∪ monocoloured n a
[multicoloured_0] Theorem
⊢ ∀a. multicoloured 0 a = ∅
[multicoloured_1] Theorem
⊢ ∀a. multicoloured 1 a = ∅
[multicoloured_card] Theorem
⊢ ∀n a. 0 < n ⇒ CARD (multicoloured n a) = a ** n − a
[multicoloured_card_eqn] Theorem
⊢ ∀n a. CARD (multicoloured n a) = if n = 0 then 0 else a ** n − a
[multicoloured_element] Theorem
⊢ ∀n a ls.
ls ∈ multicoloured n a ⇔
ls ∈ necklace n a ∧ ls ≠ [] ∧ ¬SING (set ls)
[multicoloured_empty] Theorem
⊢ ∀n. multicoloured n 0 = ∅ ∧ multicoloured n 1 = ∅
[multicoloured_finite] Theorem
⊢ ∀n a. FINITE (multicoloured n a)
[multicoloured_n_0] Theorem
⊢ ∀n. multicoloured n 0 = ∅
[multicoloured_n_1] Theorem
⊢ ∀n. multicoloured n 1 = ∅
[multicoloured_necklace] Theorem
⊢ ∀n a ls. ls ∈ multicoloured n a ⇒ ls ∈ necklace n a
[multicoloured_nonempty] Theorem
⊢ ∀n a. 1 < n ∧ 1 < a ⇒ multicoloured n a ≠ ∅
[multicoloured_not_monocoloured] Theorem
⊢ ∀n a ls. ls ∈ multicoloured n a ⇒ ls ∉ monocoloured n a
[multicoloured_not_monocoloured_iff] Theorem
⊢ ∀n a ls.
ls ∈ necklace n a ⇒
(ls ∈ multicoloured n a ⇔ ls ∉ monocoloured n a)
[multicoloured_or_monocoloured] Theorem
⊢ ∀n a ls.
ls ∈ necklace n a ⇒
ls ∈ multicoloured n a ∨ ls ∈ monocoloured n a
[multicoloured_subset] Theorem
⊢ ∀n a. multicoloured n a ⊆ necklace n a
[necklace_0] Theorem
⊢ ∀a. necklace 0 a = {[]}
[necklace_1] Theorem
⊢ ∀a. necklace 1 a = {[e] | e ∈ count a}
[necklace_1_monocoloured] Theorem
⊢ ∀a. necklace 1 a = monocoloured 1 a
[necklace_card] Theorem
⊢ ∀n a. CARD (necklace n a) = a ** n
[necklace_colors] Theorem
⊢ ∀n a ls. ls ∈ necklace n a ⇒ set ls ⊆ count a
[necklace_element] Theorem
⊢ ∀n a ls. ls ∈ necklace n a ⇔ LENGTH ls = n ∧ set ls ⊆ count a
[necklace_empty] Theorem
⊢ ∀n. 0 < n ⇒ necklace n 0 = ∅
[necklace_eqn] Theorem
⊢ ∀n a.
necklace n a =
if n = 0 then {[]}
else IMAGE (λ(c,ls). c::ls) (count a × necklace (n − 1) a)
[necklace_finite] Theorem
⊢ ∀n a. FINITE (necklace n a)
[necklace_length] Theorem
⊢ ∀n a ls. ls ∈ necklace n a ⇒ LENGTH ls = n
[necklace_not_nil] Theorem
⊢ ∀n a ls. 0 < n ∧ ls ∈ necklace n a ⇒ ls ≠ []
[necklace_property] Theorem
⊢ ∀n a ls. ls ∈ necklace n a ⇒ LENGTH ls = n ∧ set ls ⊆ count a
[necklace_suc] Theorem
⊢ ∀n a.
necklace (SUC n) a =
IMAGE (λ(c,ls). c::ls) (count a × necklace n a)
[nub_all_distinct] Theorem
⊢ ∀l. ALL_DISTINCT (nub l)
[nub_cons] Theorem
⊢ ∀x l. nub (x::l) = if MEM x l then nub l else x::nub l
[nub_nil] Theorem
⊢ nub [] = []
[nub_sing] Theorem
⊢ ∀x. nub [x] = [x]
[over_bij] Theorem
⊢ ∀f s t. BIJ f s t ⇒ over f s t
[over_inj] Theorem
⊢ ∀f s t. INJ f s t ⇒ over f s t
[over_surj] Theorem
⊢ ∀f s t. SURJ f s t ⇒ over f s t
[pairwise_coprime_prod_set_divides] Theorem
⊢ ∀s m.
FINITE s ∧ PAIRWISE_COPRIME s ∧ (∀x. x ∈ s ⇒ x divides m) ⇒
PROD_SET s divides m
[pairwise_coprime_prod_set_eq_set_lcm] Theorem
⊢ ∀s. FINITE s ∧ PAIRWISE_COPRIME s ⇒ set_lcm s = PROD_SET s
[perm_0] Theorem
⊢ perm 0 = 1
[perm_1] Theorem
⊢ perm 1 = 1
[perm_alt] Theorem
⊢ perm 0 = 1 ∧ ∀n. perm (n + 1) = (n + 1) * perm n
[perm_count_0] Theorem
⊢ perm_count 0 = {[]}
[perm_count_1] Theorem
⊢ perm_count 1 = {[0]}
[perm_count_element] Theorem
⊢ ∀ls n. ls ∈ perm_count n ⇔ ALL_DISTINCT ls ∧ set ls = count n
[perm_count_element_length] Theorem
⊢ ∀ls n. ls ∈ perm_count n ⇒ LENGTH ls = n
[perm_count_element_no_self] Theorem
⊢ ∀ls n. ls ∈ perm_count n ⇒ ¬MEM n ls
[perm_count_eqn] Theorem
⊢ ∀n. perm_count n =
if n = 0 then {[]}
else
BIGUNION (IMAGE ($interleave (n − 1)) (perm_count (n − 1)))
[perm_count_finite] Theorem
⊢ ∀n. FINITE (perm_count n)
[perm_count_interleave_card] Theorem
⊢ ∀n e. e ∈ IMAGE ($interleave n) (perm_count n) ⇒ CARD e = n + 1
[perm_count_interleave_disjoint] Theorem
⊢ ∀n e s t.
s ∈ IMAGE ($interleave n) (perm_count n) ∧
t ∈ IMAGE ($interleave n) (perm_count n) ∧ s ≠ t ⇒
DISJOINT s t
[perm_count_interleave_finite] Theorem
⊢ ∀n e. e ∈ IMAGE ($interleave n) (perm_count n) ⇒ FINITE e
[perm_count_interleave_inj] Theorem
⊢ ∀n. INJ ($interleave n) (perm_count n) 𝕌(:num list -> bool)
[perm_count_subset] Theorem
⊢ ∀n. perm_count n ⊆ necklace n n
[perm_count_suc] Theorem
⊢ ∀n. perm_count (SUC n) =
BIGUNION (IMAGE ($interleave n) (perm_count n))
[perm_count_suc_alt] Theorem
⊢ ∀n. perm_count (n + 1) =
BIGUNION (IMAGE ($interleave n) (perm_count n))
[perm_eq_fact] Theorem
⊢ ∀n. perm n = FACT n
[perm_set_bij_eq_perm_count] Theorem
⊢ ∀s. FINITE s ⇒ perm_set s =b= perm_count (CARD s)
[perm_set_card] Theorem
⊢ ∀s. FINITE s ⇒ CARD (perm_set s) = perm (CARD s)
[perm_set_card_alt] Theorem
⊢ ∀s. FINITE s ⇒ CARD (perm_set s) = FACT (CARD s)
[perm_set_element] Theorem
⊢ ∀ls s. ls ∈ perm_set s ⇔ ALL_DISTINCT ls ∧ set ls = s
[perm_set_empty] Theorem
⊢ perm_set ∅ = {[]}
[perm_set_eq_empty_sing] Theorem
⊢ ∀s. perm_set s = {[]} ⇔ s = ∅
[perm_set_finite] Theorem
⊢ ∀s. FINITE s ⇒ FINITE (perm_set s)
[perm_set_has_self_list] Theorem
⊢ ∀s. FINITE s ⇒ SET_TO_LIST s ∈ perm_set s
[perm_set_list_not_empty] Theorem
⊢ ∀ls. perm_set (set ls) ≠ ∅
[perm_set_map_bij] Theorem
⊢ ∀f s n. BIJ f s (count n) ⇒ BIJ (MAP f) (perm_set s) (perm_count n)
[perm_set_map_element] Theorem
⊢ ∀ls f s n.
ls ∈ perm_set s ∧ BIJ f s (count n) ⇒ MAP f ls ∈ perm_count n
[perm_set_map_inj] Theorem
⊢ ∀f s n. BIJ f s (count n) ⇒ INJ (MAP f) (perm_set s) (perm_count n)
[perm_set_map_surj] Theorem
⊢ ∀f s n.
BIJ f s (count n) ⇒ SURJ (MAP f) (perm_set s) (perm_count n)
[perm_set_not_empty] Theorem
⊢ ∀s. FINITE s ⇒ perm_set s ≠ ∅
[perm_set_perm_count] Theorem
⊢ ∀n. perm_set (count n) = perm_count n
[perm_set_sing] Theorem
⊢ ∀x. perm_set {x} = {[x]}
[perm_suc] Theorem
⊢ ∀n. perm (SUC n) = SUC n * perm n
[perm_suc_alt] Theorem
⊢ ∀n. perm (n + 1) = (n + 1) * perm n
[power_predecessor_eqn] Theorem
⊢ ∀t n. tops t n = (t − 1) * SUM (MAP (λj. t ** j) [0 ..< n])
[prime_divides_binomials] Theorem
⊢ ∀n. prime n ⇒ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ n divides binomial n k
[prime_divides_binomials_alt] Theorem
⊢ ∀n k. prime n ∧ 0 < k ∧ k < n ⇒ n divides binomial n k
[prime_divisor_property] Theorem
⊢ ∀n p.
1 < n ∧ p < n ∧ prime p ∧ p divides n ⇒
¬(p divides FACT (n − 1) DIV FACT (n − p))
[prime_iff_divides_binomials] Theorem
⊢ ∀n. prime n ⇔ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ n divides binomial n k
[prime_iff_divides_binomials_alt] Theorem
⊢ ∀n. prime n ⇔ 1 < n ∧ ∀k. 0 < k ∧ k < n ⇒ binomial n k MOD n = 0
[prod_1_to_n_eq_fact_n] Theorem
⊢ ∀n. PROD [1 .. n] = FACT n
[rotate_0] Theorem
⊢ ∀l. rotate 0 l = l
[rotate_add] Theorem
⊢ ∀n m l. n + m ≤ LENGTH l ⇒ rotate n (rotate m l) = rotate (n + m) l
[rotate_full] Theorem
⊢ ∀l. rotate (LENGTH l) l = l
[rotate_lcancel] Theorem
⊢ ∀k l. k < LENGTH l ⇒ rotate (LENGTH l − k) (rotate k l) = l
[rotate_nil] Theorem
⊢ ∀n. rotate n [] = []
[rotate_rcancel] Theorem
⊢ ∀k l. k < LENGTH l ⇒ rotate k (rotate (LENGTH l − k) l) = l
[rotate_same_length] Theorem
⊢ ∀l n. LENGTH (rotate n l) = LENGTH l
[rotate_same_set] Theorem
⊢ ∀l n. set (rotate n l) = set l
[rotate_shift_element] Theorem
⊢ ∀l n.
n < LENGTH l ⇒ rotate n l = EL n l::(DROP (SUC n) l ⧺ TAKE n l)
[rotate_suc] Theorem
⊢ ∀l n. n < LENGTH l ⇒ rotate (SUC n) l = rotate 1 (rotate n l)
[set_lcm_empty] Theorem
⊢ set_lcm ∅ = 1
[set_lcm_eq_big_lcm] Theorem
⊢ ∀s. FINITE s ⇒ big_lcm s = set_lcm s
[set_lcm_eq_list_lcm] Theorem
⊢ ∀l. set_lcm (set l) = list_lcm l
[set_lcm_insert] Theorem
⊢ ∀s. FINITE s ⇒ ∀x. set_lcm (x INSERT s) = lcm x (set_lcm s)
[set_lcm_is_common_multiple] Theorem
⊢ ∀x s. FINITE s ∧ x ∈ s ⇒ x divides set_lcm s
[set_lcm_is_least_common_multiple] Theorem
⊢ ∀s m. FINITE s ∧ (∀x. x ∈ s ⇒ x divides m) ⇒ set_lcm s divides m
[set_lcm_nonempty] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒
set_lcm s = lcm (CHOICE s) (set_lcm (REST s))
[set_lcm_sing] Theorem
⊢ ∀x. set_lcm {x} = x
[sub_count_0_n] Theorem
⊢ ∀n. sub_count 0 n = if n = 0 then {∅} else ∅
[sub_count_alt] Theorem
⊢ ∀n k.
sub_count n 0 = {∅} ∧ sub_count 0 (k + 1) = ∅ ∧
sub_count (n + 1) (k + 1) =
IMAGE (λs. n INSERT s) (sub_count n k) ∪ sub_count n (k + 1)
[sub_count_count_inj] Theorem
⊢ ∀n m. INJ (sub_count n) (upto n) 𝕌(:(num -> bool) -> bool)
[sub_count_disjoint] Theorem
⊢ ∀n k.
DISJOINT (IMAGE (λs. n INSERT s) (sub_count n k))
(sub_count n (k + 1))
[sub_count_element] Theorem
⊢ ∀n k s. s ∈ sub_count n k ⇔ s ⊆ count n ∧ CARD s = k
[sub_count_element_finite] Theorem
⊢ ∀n k s. s ∈ sub_count n k ⇒ FINITE s
[sub_count_element_no_self] Theorem
⊢ ∀n k s. s ∈ sub_count n k ⇒ n ∉ s
[sub_count_eq_empty] Theorem
⊢ ∀n k. sub_count n k = ∅ ⇔ n < k
[sub_count_eqn] Theorem
⊢ ∀n k.
sub_count n k =
if k = 0 then {∅}
else if n = 0 then ∅
else
IMAGE (λs. n − 1 INSERT s) (sub_count (n − 1) (k − 1)) ∪
sub_count (n − 1) k
[sub_count_equiv_class] Theorem
⊢ ∀n s.
s ⊆ count n ⇒
sub_count n (CARD s) =
equiv_class (λs t. s =b= t) (POW (count n)) s
[sub_count_finite] Theorem
⊢ ∀n k. FINITE (sub_count n k)
[sub_count_insert] Theorem
⊢ ∀n k s. s ∈ sub_count n k ⇒ n INSERT s ∈ sub_count (n + 1) (k + 1)
[sub_count_insert_card] Theorem
⊢ ∀n k. CARD (IMAGE (λs. n INSERT s) (sub_count n k)) = n choose k
[sub_count_n_0] Theorem
⊢ ∀n. sub_count n 0 = {∅}
[sub_count_n_1] Theorem
⊢ ∀n. sub_count n 1 = {{j} | j < n}
[sub_count_n_n] Theorem
⊢ ∀n. sub_count n n = {count n}
[sub_count_subset] Theorem
⊢ ∀n k. sub_count n k ⊆ POW (count n)
[sub_count_union] Theorem
⊢ ∀n k.
sub_count (n + 1) (k + 1) =
IMAGE (λs. n INSERT s) (sub_count n k) ∪ sub_count n (k + 1)
[sub_sets_element] Theorem
⊢ ∀P k s. s ∈ sub_sets P k ⇔ s ⊆ P ∧ CARD s = k
[sub_sets_equiv_class] Theorem
⊢ ∀s t.
FINITE t ∧ s ⊆ t ⇒
sub_sets t (CARD s) = equiv_class (λs t. s =b= t) (POW t) s
[sub_sets_sub_count] Theorem
⊢ ∀n k. sub_sets (count n) k = sub_count n k
[sum_1_to_n_double] Theorem
⊢ ∀n. TWICE (SUM [1 .. n]) = n * (n + 1)
[sum_1_to_n_eq_tri_n] Theorem
⊢ ∀n. SUM [1 .. n] = tri n
[sum_1_to_n_eqn] Theorem
⊢ ∀n. SUM [1 .. n] = HALF (n * (n + 1))
[surj_iff_preimage_card_not_0] Theorem
⊢ ∀f s t.
FINITE s ∧ over f s t ⇒
(SURJ f s t ⇔ ∀y. y ∈ t ⇒ CARD (preimage f s y) ≠ 0)
[surj_preimage_not_empty] Theorem
⊢ ∀f s t. SURJ f s t ⇔ over f s t ∧ ∀y. y ∈ t ⇒ preimage f s y ≠ ∅
[tail_turn] Theorem
⊢ ∀ls. ls ≠ [] ⇒ TL (turn ls) = FRONT ls
[triple_11] Theorem
⊢ ∀a0 a1 a2 a0' a1' a2'.
triple a0 a1 a2 = triple a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
[triple_Axiom] Theorem
⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (triple a0 a1 a2) = f a0 a1 a2
[triple_accessors] Theorem
⊢ (∀n n0 n1. (triple n n0 n1).a = n) ∧
(∀n n0 n1. (triple n n0 n1).b = n0) ∧
∀n n0 n1. (triple n n0 n1).c = n1
[triple_accfupds] Theorem
⊢ (∀t f. (t with b updated_by f).a = t.a) ∧
(∀t f. (t with c updated_by f).a = t.a) ∧
(∀t f. (t with a updated_by f).b = t.b) ∧
(∀t f. (t with c updated_by f).b = t.b) ∧
(∀t f. (t with a updated_by f).c = t.c) ∧
(∀t f. (t with b updated_by f).c = t.c) ∧
(∀t f. (t with a updated_by f).a = f t.a) ∧
(∀t f. (t with b updated_by f).b = f t.b) ∧
∀t f. (t with c updated_by f).c = f t.c
[triple_case_cong] Theorem
⊢ ∀M M' f.
M = M' ∧
(∀a0 a1 a2. M' = triple a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
triple_CASE M f = triple_CASE M' f'
[triple_case_eq] Theorem
⊢ triple_CASE x f = v ⇔ ∃n n0 n1. x = triple n n0 n1 ∧ f n n0 n1 = v
[triple_component_equality] Theorem
⊢ ∀t1 t2. t1 = t2 ⇔ t1.a = t2.a ∧ t1.b = t2.b ∧ t1.c = t2.c
[triple_fn_updates] Theorem
⊢ (∀f n n0 n1.
triple n n0 n1 with a updated_by f = triple (f n) n0 n1) ∧
(∀f n n0 n1.
triple n n0 n1 with b updated_by f = triple n (f n0) n1) ∧
∀f n n0 n1. triple n n0 n1 with c updated_by f = triple n n0 (f n1)
[triple_fupdcanon] Theorem
⊢ (∀t g f.
t with <|b updated_by f; a updated_by g|> =
t with <|a updated_by g; b updated_by f|>) ∧
(∀t g f.
t with <|c updated_by f; a updated_by g|> =
t with <|a updated_by g; c updated_by f|>) ∧
∀t g f.
t with <|c updated_by f; b updated_by g|> =
t with <|b updated_by g; c updated_by f|>
[triple_fupdcanon_comp] Theorem
⊢ ((∀g f. b_fupd f ∘ a_fupd g = a_fupd g ∘ b_fupd f) ∧
∀h g f. b_fupd f ∘ a_fupd g ∘ h = a_fupd g ∘ b_fupd f ∘ h) ∧
((∀g f. c_fupd f ∘ a_fupd g = a_fupd g ∘ c_fupd f) ∧
∀h g f. c_fupd f ∘ a_fupd g ∘ h = a_fupd g ∘ c_fupd f ∘ h) ∧
(∀g f. c_fupd f ∘ b_fupd g = b_fupd g ∘ c_fupd f) ∧
∀h g f. c_fupd f ∘ b_fupd g ∘ h = b_fupd g ∘ c_fupd f ∘ h
[triple_fupdfupds] Theorem
⊢ (∀t g f.
t with <|a updated_by f; a updated_by g|> =
t with a updated_by f ∘ g) ∧
(∀t g f.
t with <|b updated_by f; b updated_by g|> =
t with b updated_by f ∘ g) ∧
∀t g f.
t with <|c updated_by f; c updated_by g|> =
t with c updated_by f ∘ g
[triple_fupdfupds_comp] Theorem
⊢ ((∀g f. a_fupd f ∘ a_fupd g = a_fupd (f ∘ g)) ∧
∀h g f. a_fupd f ∘ a_fupd g ∘ h = a_fupd (f ∘ g) ∘ h) ∧
((∀g f. b_fupd f ∘ b_fupd g = b_fupd (f ∘ g)) ∧
∀h g f. b_fupd f ∘ b_fupd g ∘ h = b_fupd (f ∘ g) ∘ h) ∧
(∀g f. c_fupd f ∘ c_fupd g = c_fupd (f ∘ g)) ∧
∀h g f. c_fupd f ∘ c_fupd g ∘ h = c_fupd (f ∘ g) ∘ h
[triple_induction] Theorem
⊢ ∀P. (∀n n0 n1. P (triple n n0 n1)) ⇒ ∀t. P t
[triple_literal_11] Theorem
⊢ ∀n11 n01 n1 n12 n02 n2.
<|a := n11; b := n01; c := n1|> = <|a := n12; b := n02; c := n2|> ⇔
n11 = n12 ∧ n01 = n02 ∧ n1 = n2
[triple_literal_nchotomy] Theorem
⊢ ∀t. ∃n1 n0 n. t = <|a := n1; b := n0; c := n|>
[triple_nchotomy] Theorem
⊢ ∀tt. ∃n n0 n1. tt = triple n n0 n1
[triple_updates_eq_literal] Theorem
⊢ ∀t n1 n0 n.
t with <|a := n1; b := n0; c := n|> =
<|a := n1; b := n0; c := n|>
[turn_eq_nil] Theorem
⊢ ∀p. turn p = [] ⇔ p = []
[turn_exp_0] Theorem
⊢ ∀l. turn_exp l 0 = l
[turn_exp_1] Theorem
⊢ ∀l. turn_exp l 1 = turn l
[turn_exp_2] Theorem
⊢ ∀l. turn_exp l 2 = turn (turn l)
[turn_exp_SUC] Theorem
⊢ ∀l n. turn_exp l (SUC n) = turn_exp (turn l) n
[turn_exp_length] Theorem
⊢ ∀l n. LENGTH (turn_exp l n) = LENGTH l
[turn_exp_suc] Theorem
⊢ ∀l n. turn_exp l (SUC n) = turn (turn_exp l n)
[turn_length] Theorem
⊢ ∀l. LENGTH (turn l) = LENGTH l
[turn_nil] Theorem
⊢ turn [] = []
[turn_not_nil] Theorem
⊢ ∀l. l ≠ [] ⇒ turn l = LAST l::FRONT l
[turn_snoc] Theorem
⊢ ∀ls x. turn (SNOC x ls) = x::ls
*)
end
HOL 4, Trindemossen-2