Readable signature
BetaAt(b,c,i,x)Exact expansion
((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))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
none
Used by definitions
PD0014 Product PD0015 Sum PD0016 AllBits PD0018 Range PD0019 Repeat PD0041 Choose PD0043 Primorial PD0049 PowerQuotPrefixUsed by theorem statements or local proof propositions
BT0040 beta_at_self_of_bound BT0041 beta_at_exists BT0042 beta_at_unique BT0045 beta_at_of_mod_eq_bound BT0053 beta_value_le_code BT0057 beta_value_lt_scaled_base BT005A beta_exclusive_recode_congruence_step BT005B beta_exclusive_recode_invariant_step BT005C bounded_beta_exclusive_recode_invariant BT005D beta_prefix_extend BT005E beta_prefix_product_trace_exists BT005F beta_product_exists BT005G beta_product_functional BT005J beta_product_succ_decompose BT005K beta_product_succ_append BT005L beta_product_transport_prefix BT0069 beta_factor_divides_product BT007X beta_repeat_entry_eq BT007Y beta_repeat_transport_entry BT0082 pow_functional BT0083 pow_successor_decompose BT0087 beta_range_entry_eq BT0088 beta_range_transport_entry BT0089 beta_prefix_sum_trace_exists BT008A beta_sum_exists BT008B beta_sum_trace_functional BT008F beta_sum_succ_decompose BT008K all_bits_last_succ BT008O bit_count_succ_decompose BT008P bit_count_bounded BT0090 factorial_functional BT0092 factorial_succ_decompose BT00DH beta_product_pointwise_coprime BT00I9 beta_sum_transport_prefix BT00JA eisenstein_initial_segment_prefix_all_bits BT00JB eisenstein_initial_segment_decoded_choice BT00JC beta_all_one_bit_count_exact BT00JD eisenstein_initial_segment_bit_count_functional BT00JE eisenstein_initial_segment_bit_count_exact BT00K5 beta_sum_pointwise_add BT00S0 prime_power_quotient_prefix_exists BT00S1 power_quotient_prefix_transport BT00S3 legendre_sum_functional BT00SE eisenstein_initial_segment_prefix_extend BT00SF eisenstein_initial_segment_prefix_exists BT00SJ power_quotient_prefix_decoded_divrem BT00SK power_quotient_successor_pointwise_add BT00SR beta_sum_succ_last_zero BT00SS prime_power_quotient_prefix_last_zero BT00ST legendre_sum_zero_extended_prefix BT00SU initial_segment_prefix_sum_exists BT00SV prime_legendre_sum_succ BT00T2 beta_pascal_zero_row_extend BT00T3 beta_pascal_zero_row_exists BT00T4 beta_pascal_row_step_extend BT00T5 beta_pascal_row_step_exists BT00T6 beta_pascal_table_prefix_extend BT00T7 beta_pascal_table_prefix_exists BT00T8 choose_exists BT00T9 beta_pascal_zero_row_pointwise_functional BT00TA beta_pascal_row_step_pointwise_functional BT00TB beta_pascal_table_row_pointwise_functional BT00TC choose_functional BT00TE choose_zero BT00TF beta_pascal_table_diagonal_boundary BT00TG choose_self BT00TH beta_pascal_table_successor_cell_recurrence BT00TI choose_succ_succ_of_lt BT00U7 primorial_factor_prefix_extend BT00U8 primorial_factor_prefix_exists BT00UA primorial_exists BT00UD primorial_succ_decompose BT00UQ beta_product_prefix_suffix_split BT00UR primorial_interval_factor_prefix_extend BT00US primorial_interval_factor_prefix_exists BT00UW primorial_interval_factor_prefix_shift BT00UX primorial_factor_prefix_restrict_add BT00UY primorial_prefix_interval_split BT00VA factorial_prime_divides_of_le BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00VE primorial_interval_pairwise_coprime BT00VF primorial_interval_divides_choose_between BT00VG primorial_even_interval_divides_central BT00VH primorial_odd_interval_divides_middle BT00VI primorial_even_interval_le_central BT00VJ primorial_odd_interval_le_middle BT00VU primorial_four_power_support_package BT00VV primorial_le_four_pow_bounded BT00X9 beta_product_pointwise_le BT00XA beta_product_uniform_le_pow BT00XP power_quotient_prefix_tail_entry_zero BT00XQ power_quotient_prefix_sum_extend_zero BT00XV double_quotient_carry_choice BT00XW double_quotient_carry_prefix_extend BT00XX double_quotient_carry_prefix_exists BT00XY double_quotient_carry_prefix_all_bits BT00Y0 double_quotient_carry_prefix_restrict BT00Y1 bit_count_positive_last_one BT00Y3 beta_sum_double_carry_exact BT00Y4 central_binom_carry_bit_count BT00Y5 central_binom_prime_power_contribution_le_double BT00YC double_quotient_carry_prefix_entries_zero BT00YD central_binom_prime_valuation_zero_of_exact_double_quotients BT00YP prime_contribution_prefix_extend BT00YQ prime_contribution_prefix_exists BT00YS prime_contribution_product_exists BT00YW prime_contribution_prefix_pairwise_coprime BT00YY prime_contribution_product_divides BT0100 prime_contribution_selected_entry BT0102 prime_contribution_cofactor_prime_contradiction BT0103 prime_contribution_cofactor_eq_one BT0104 prime_contribution_reverse_divides BT0105 prime_contribution_product_eq BT0106 prime_contribution_complete_exists BT0107 central_binom_prime_contribution_product_exists BT010K prime_contribution_interval_prefix_extend BT010L prime_contribution_interval_prefix_exists BT010P prime_contribution_interval_prefix_shift BT010Q prime_contribution_prefix_restrict_add BT010R prime_contribution_prefix_interval_split BT010S prime_contribution_product_length_eq_transport BT010U beta_product_all_one_exact 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