Readable signature
CentralBinom(n,z)Exact expansion
((exists bcf_lt_gap_bertrand_defined_central_binom_out_of_range. bcf_lt_gap_bertrand_defined_central_binom_out_of_range + S (n + n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bertrand_defined_central_binom_in_range. bcf_le_gap_bertrand_defined_central_binom_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bertrand_defined_central_binom bcf_row_code_scale_bertrand_defined_central_binom bcf_row_scale_code_bertrand_defined_central_binom bcf_row_scale_scale_bertrand_defined_central_binom bcf_row_code_bertrand_defined_central_binom bcf_row_scale_bertrand_defined_central_binom. ((forall bcf_row_index_bertrand_defined_central_binom_table. (exists bcf_lt_gap_bertrand_defined_central_binom_table_row_bound. bcf_lt_gap_bertrand_defined_central_binom_table_row_bound + S (bcf_row_index_bertrand_defined_central_binom_table) = S (n + n)) -> exists bcf_row_code_bertrand_defined_central_binom_table bcf_row_scale_bertrand_defined_central_binom_table. ((((exists bcf_height_bertrand_defined_central_binom_table_decoded_row_code. bcf_height_bertrand_defined_central_binom_table_decoded_row_code + S (bcf_row_code_bertrand_defined_central_binom_table) = S ((S (bcf_row_index_bertrand_defined_central_binom_table)) * bcf_row_code_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_decoded_row_code. bcf_row_code_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_table_decoded_row_code * S ((S (bcf_row_index_bertrand_defined_central_binom_table)) * bcf_row_code_scale_bertrand_defined_central_binom) + (bcf_row_code_bertrand_defined_central_binom_table))) /\ ((((exists bcf_height_bertrand_defined_central_binom_table_decoded_row_scale. bcf_height_bertrand_defined_central_binom_table_decoded_row_scale + S (bcf_row_scale_bertrand_defined_central_binom_table) = S ((S (bcf_row_index_bertrand_defined_central_binom_table)) * bcf_row_scale_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_decoded_row_scale. bcf_row_scale_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_table_decoded_row_scale * S ((S (bcf_row_index_bertrand_defined_central_binom_table)) * bcf_row_scale_scale_bertrand_defined_central_binom) + (bcf_row_scale_bertrand_defined_central_binom_table))) /\ ((bcf_row_index_bertrand_defined_central_binom_table = 0 /\ (forall bcf_index_bertrand_defined_central_binom_table_zero_row. (exists bcf_lt_gap_bertrand_defined_central_binom_table_zero_row_bound. bcf_lt_gap_bertrand_defined_central_binom_table_zero_row_bound + S (bcf_index_bertrand_defined_central_binom_table_zero_row) = S (n + n)) -> exists bcf_value_bertrand_defined_central_binom_table_zero_row. ((((exists bcf_height_bertrand_defined_central_binom_table_zero_row_entry. bcf_height_bertrand_defined_central_binom_table_zero_row_entry + S (bcf_value_bertrand_defined_central_binom_table_zero_row) = S ((S (bcf_index_bertrand_defined_central_binom_table_zero_row)) * bcf_row_scale_bertrand_defined_central_binom_table)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_zero_row_entry. bcf_row_code_bertrand_defined_central_binom_table = bcf_quotient_bertrand_defined_central_binom_table_zero_row_entry * S ((S (bcf_index_bertrand_defined_central_binom_table_zero_row)) * bcf_row_scale_bertrand_defined_central_binom_table) + (bcf_value_bertrand_defined_central_binom_table_zero_row))) /\ ((bcf_index_bertrand_defined_central_binom_table_zero_row = 0 /\ bcf_value_bertrand_defined_central_binom_table_zero_row = 1) \/ exists bcf_predecessor_bertrand_defined_central_binom_table_zero_row. bcf_index_bertrand_defined_central_binom_table_zero_row = S bcf_predecessor_bertrand_defined_central_binom_table_zero_row /\ bcf_value_bertrand_defined_central_binom_table_zero_row = 0)))) \/ exists bcf_predecessor_bertrand_defined_central_binom_table bcf_previous_code_bertrand_defined_central_binom_table bcf_previous_scale_bertrand_defined_central_binom_table. bcf_row_index_bertrand_defined_central_binom_table = S bcf_predecessor_bertrand_defined_central_binom_table /\ ((((exists bcf_height_bertrand_defined_central_binom_table_decoded_previous_code. bcf_height_bertrand_defined_central_binom_table_decoded_previous_code + S (bcf_previous_code_bertrand_defined_central_binom_table) = S ((S (bcf_predecessor_bertrand_defined_central_binom_table)) * bcf_row_code_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_decoded_previous_code. bcf_row_code_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_table_decoded_previous_code * S ((S (bcf_predecessor_bertrand_defined_central_binom_table)) * bcf_row_code_scale_bertrand_defined_central_binom) + (bcf_previous_code_bertrand_defined_central_binom_table))) /\ ((((exists bcf_height_bertrand_defined_central_binom_table_decoded_previous_scale. bcf_height_bertrand_defined_central_binom_table_decoded_previous_scale + S (bcf_previous_scale_bertrand_defined_central_binom_table) = S ((S (bcf_predecessor_bertrand_defined_central_binom_table)) * bcf_row_scale_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_decoded_previous_scale. bcf_row_scale_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_table_decoded_previous_scale * S ((S (bcf_predecessor_bertrand_defined_central_binom_table)) * bcf_row_scale_scale_bertrand_defined_central_binom) + (bcf_previous_scale_bertrand_defined_central_binom_table))) /\ (forall bcf_index_bertrand_defined_central_binom_table_row_step. (exists bcf_lt_gap_bertrand_defined_central_binom_table_row_step_bound. bcf_lt_gap_bertrand_defined_central_binom_table_row_step_bound + S (bcf_index_bertrand_defined_central_binom_table_row_step) = S (n + n)) -> exists bcf_value_bertrand_defined_central_binom_table_row_step. ((((exists bcf_height_bertrand_defined_central_binom_table_row_step_entry. bcf_height_bertrand_defined_central_binom_table_row_step_entry + S (bcf_value_bertrand_defined_central_binom_table_row_step) = S ((S (bcf_index_bertrand_defined_central_binom_table_row_step)) * bcf_row_scale_bertrand_defined_central_binom_table)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_row_step_entry. bcf_row_code_bertrand_defined_central_binom_table = bcf_quotient_bertrand_defined_central_binom_table_row_step_entry * S ((S (bcf_index_bertrand_defined_central_binom_table_row_step)) * bcf_row_scale_bertrand_defined_central_binom_table) + (bcf_value_bertrand_defined_central_binom_table_row_step))) /\ ((bcf_index_bertrand_defined_central_binom_table_row_step = 0 /\ bcf_value_bertrand_defined_central_binom_table_row_step = 1) \/ exists bcf_predecessor_bertrand_defined_central_binom_table_row_step bcf_left_bertrand_defined_central_binom_table_row_step bcf_right_bertrand_defined_central_binom_table_row_step. bcf_index_bertrand_defined_central_binom_table_row_step = S bcf_predecessor_bertrand_defined_central_binom_table_row_step /\ ((((exists bcf_height_bertrand_defined_central_binom_table_row_step_previous_left. bcf_height_bertrand_defined_central_binom_table_row_step_previous_left + S (bcf_left_bertrand_defined_central_binom_table_row_step) = S ((S (bcf_predecessor_bertrand_defined_central_binom_table_row_step)) * bcf_previous_scale_bertrand_defined_central_binom_table)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_row_step_previous_left. bcf_previous_code_bertrand_defined_central_binom_table = bcf_quotient_bertrand_defined_central_binom_table_row_step_previous_left * S ((S (bcf_predecessor_bertrand_defined_central_binom_table_row_step)) * bcf_previous_scale_bertrand_defined_central_binom_table) + (bcf_left_bertrand_defined_central_binom_table_row_step))) /\ ((((exists bcf_height_bertrand_defined_central_binom_table_row_step_previous_right. bcf_height_bertrand_defined_central_binom_table_row_step_previous_right + S (bcf_right_bertrand_defined_central_binom_table_row_step) = S ((S (S (bcf_predecessor_bertrand_defined_central_binom_table_row_step))) * bcf_previous_scale_bertrand_defined_central_binom_table)) /\ exists bcf_quotient_bertrand_defined_central_binom_table_row_step_previous_right. bcf_previous_code_bertrand_defined_central_binom_table = bcf_quotient_bertrand_defined_central_binom_table_row_step_previous_right * S ((S (S (bcf_predecessor_bertrand_defined_central_binom_table_row_step))) * bcf_previous_scale_bertrand_defined_central_binom_table) + (bcf_right_bertrand_defined_central_binom_table_row_step))) /\ bcf_value_bertrand_defined_central_binom_table_row_step = bcf_left_bertrand_defined_central_binom_table_row_step + bcf_right_bertrand_defined_central_binom_table_row_step))))))))))) /\ ((((exists bcf_height_bertrand_defined_central_binom_decoded_row_code. bcf_height_bertrand_defined_central_binom_decoded_row_code + S (bcf_row_code_bertrand_defined_central_binom) = S ((S (n + n)) * bcf_row_code_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_decoded_row_code. bcf_row_code_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bertrand_defined_central_binom) + (bcf_row_code_bertrand_defined_central_binom))) /\ ((((exists bcf_height_bertrand_defined_central_binom_decoded_row_scale. bcf_height_bertrand_defined_central_binom_decoded_row_scale + S (bcf_row_scale_bertrand_defined_central_binom) = S ((S (n + n)) * bcf_row_scale_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_decoded_row_scale. bcf_row_scale_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bertrand_defined_central_binom) + (bcf_row_scale_bertrand_defined_central_binom))) /\ (((exists bcf_height_bertrand_defined_central_binom_decoded_value. bcf_height_bertrand_defined_central_binom_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bertrand_defined_central_binom)) /\ exists bcf_quotient_bertrand_defined_central_binom_decoded_value. bcf_row_code_bertrand_defined_central_binom = bcf_quotient_bertrand_defined_central_binom_decoded_value * S ((S (n)) * bcf_row_scale_bertrand_defined_central_binom) + (z))))))))This node is conservative notation, not a theorem, new axiom, predicate constant, or kernel rule. Its expansion is checked for exact first-order AST equivalence.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
BT00TN central_binom_exists BT00TP central_binom_positive BT00TQ central_binom_zero BT00TS central_binom_succ_double_middle BT00TU central_binom_succ_recurrence BT00U2 central_binom_four_weighted_of_recurrence BT00U3 four_pow_central_seed_package BT00U4 four_pow_lt_mul_central_binom BT00VG primorial_even_interval_divides_central BT00VI primorial_even_interval_le_central BT00VL central_binom_recurrence_double_bundle BT00VM central_binom_strong_upper_of_laws BT00VN central_binom_upper_support_package BT00VO central_binom_strong_upper BT00VP central_binom_odd_middle_le_four_pow BT00VT central_binom_nonzero_strong_upper BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00VX central_binom_prime_divisor_le_double BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT00XM central_binom_factorial_valuation_balance BT00XN central_binom_legendre_valuation_balance BT00Y4 central_binom_carry_bit_count BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00Y7 central_binom_prime_square_tail_valuation_le_one BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients BT00YE central_binom_prime_valuation_zero_two_thirds_range BT00YG central_binom_prime_valuation_zero_above_third_quotient BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one BT00YJ no_bertrand_central_nonzero_valuation_live_ranges BT00YK no_bertrand_central_nonzero_valuation_factor_ranges BT00YL no_bertrand_central_nonzero_contribution_factor_ranges BT00YM no_bertrand_central_prime_contribution_ranges BT0107 central_binom_prime_contribution_product_exists BT0108 no_bertrand_central_contribution_choice_ranges BT010V no_bertrand_small_contribution_choice_le_double BT010W no_bertrand_middle_contribution_choice_le_selector BT010X no_bertrand_high_contribution_choice_eq_one BT010Y no_bertrand_small_contribution_product_le_power BT0110 no_bertrand_middle_contribution_interval_le_primorial_interval BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0112 no_bertrand_high_contribution_interval_eq_one BT0113 central_binom_factorization_small BT0114 central_binom_le_of_no_bertrand_prime BT0115 bertrand_eventually_closed_upper