Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Readable signature
BitCount(b,c,l,z)Exact expansion
((exists ff_u_defined_bit_count_sum ff_v_defined_bit_count_sum. ((((exists ff_h_defined_bit_count_sum_start. ff_h_defined_bit_count_sum_start + S (0) = S ((S (0)) * ff_v_defined_bit_count_sum)) /\ exists ff_q_defined_bit_count_sum_start. ff_u_defined_bit_count_sum = ff_q_defined_bit_count_sum_start * S ((S (0)) * ff_v_defined_bit_count_sum) + (0))) /\ ((((exists ff_h_defined_bit_count_sum_terminal. ff_h_defined_bit_count_sum_terminal + S (z) = S ((S (l)) * ff_v_defined_bit_count_sum)) /\ exists ff_q_defined_bit_count_sum_terminal. ff_u_defined_bit_count_sum = ff_q_defined_bit_count_sum_terminal * S ((S (l)) * ff_v_defined_bit_count_sum) + (z))) /\ forall ff_i_defined_bit_count_sum. (exists ff_lt_defined_bit_count_sum_bound. ff_lt_defined_bit_count_sum_bound + S ff_i_defined_bit_count_sum = l) -> exists ff_a_defined_bit_count_sum ff_r_defined_bit_count_sum ff_s_defined_bit_count_sum. ((((exists ff_h_defined_bit_count_sum_summand. ff_h_defined_bit_count_sum_summand + S (ff_a_defined_bit_count_sum) = S ((S (ff_i_defined_bit_count_sum)) * c)) /\ exists ff_q_defined_bit_count_sum_summand. b = ff_q_defined_bit_count_sum_summand * S ((S (ff_i_defined_bit_count_sum)) * c) + (ff_a_defined_bit_count_sum))) /\ ((((exists ff_h_defined_bit_count_sum_partial. ff_h_defined_bit_count_sum_partial + S (ff_r_defined_bit_count_sum) = S ((S (ff_i_defined_bit_count_sum)) * ff_v_defined_bit_count_sum)) /\ exists ff_q_defined_bit_count_sum_partial. ff_u_defined_bit_count_sum = ff_q_defined_bit_count_sum_partial * S ((S (ff_i_defined_bit_count_sum)) * ff_v_defined_bit_count_sum) + (ff_r_defined_bit_count_sum))) /\ ((((exists ff_h_defined_bit_count_sum_successor. ff_h_defined_bit_count_sum_successor + S (ff_s_defined_bit_count_sum) = S ((S (S ff_i_defined_bit_count_sum)) * ff_v_defined_bit_count_sum)) /\ exists ff_q_defined_bit_count_sum_successor. ff_u_defined_bit_count_sum = ff_q_defined_bit_count_sum_successor * S ((S (S ff_i_defined_bit_count_sum)) * ff_v_defined_bit_count_sum) + (ff_s_defined_bit_count_sum))) /\ ff_s_defined_bit_count_sum = ff_r_defined_bit_count_sum + ff_a_defined_bit_count_sum)))))) /\ (forall ff_i_defined_bit_count_bits. (exists ff_lt_defined_bit_count_bits_bound. ff_lt_defined_bit_count_bits_bound + S ff_i_defined_bit_count_bits = l) -> exists ff_bit_defined_bit_count_bits. ((((exists ff_h_defined_bit_count_bits_decoded. ff_h_defined_bit_count_bits_decoded + S (ff_bit_defined_bit_count_bits) = S ((S (ff_i_defined_bit_count_bits)) * c)) /\ exists ff_q_defined_bit_count_bits_decoded. b = ff_q_defined_bit_count_bits_decoded * S ((S (ff_i_defined_bit_count_bits)) * c) + (ff_bit_defined_bit_count_bits))) /\ (ff_bit_defined_bit_count_bits = 0 \/ ff_bit_defined_bit_count_bits = 1))))This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
PA003I bit_count_exists PA0042 bit_count_succ_decompose PA0048 bit_count_zero PA006Q bit_count_functional PA0077 gauss_signed_half_bit_count_exists PA007G beta_sign_factor_prefix_exists PA007I beta_sign_factor_product_power PA007J beta_sign_factor_product_power_exists PA0080 gauss_signed_products_balance_mod PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA00BV arbitrary_gauss_lemma_complete PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00DF distinct_odd_prime_half_row_count_exists PA00DG distinct_odd_prime_half_row_count_choice PA00DH distinct_odd_prime_half_row_count_choices_bounded PA00DI eisenstein_rectangle_row_count_prefix_extend PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DK distinct_odd_prime_half_row_count_prefix_exists_bounded PA00DL distinct_odd_prime_half_row_count_prefix_exists PA00DM distinct_odd_prime_half_rectangle_total_exists PA00DW beta_all_one_bit_count_exact PA00DX eisenstein_initial_segment_bit_count_functional PA00DY eisenstein_initial_segment_bit_count_exact PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient PA00E2 distinct_odd_prime_semantic_row_equals_decoded_quotient PA00E3 distinct_odd_prime_quotient_entry_matches_rectangle PA00E4 distinct_odd_prime_quotient_sum_transports_to_rectangle PA00E5 distinct_odd_prime_quotient_sum_equals_rectangle_total PA00E6 eisenstein_rectangle_decoded_row_count PA00E7 eisenstein_transposed_outer_column_choices PA00E8 eisenstein_transposed_column_prefix_extend PA00E9 eisenstein_transposed_column_prefix_exists PA00EB eisenstein_transposed_column_prefix_all_bits PA00ED eisenstein_transposed_column_pointwise_complement PA00EE complementary_bit_counts_add_length PA00EF eisenstein_row_transposed_column_count_partition PA00EG eisenstein_transposed_column_count_choices PA00EH eisenstein_transposed_column_count_prefix_extend PA00EI eisenstein_transposed_column_count_prefix_exists PA00EJ eisenstein_transposed_column_count_total_exists PA00EM eisenstein_transposed_column_count_decoded_witness PA00EN eisenstein_transposed_column_count_decoded_partition PA00EO eisenstein_transposed_column_count_matches_decoded_constant PA00EQ eisenstein_rectangle_plus_column_count_total PA00ER eisenstein_transposed_column_count_prefix_forget PA00ES eisenstein_zero_width_rectangle_sum_zero PA00EU eisenstein_successor_row_count_decompose PA00EV eisenstein_successor_row_split_choices PA00EW eisenstein_successor_row_split_prefix_extend PA00EX eisenstein_successor_row_split_prefix_exists PA00EY eisenstein_successor_rectangle_row_split_prefix_exists PA00F0 eisenstein_successor_row_split_reduced_rectangle_prefix PA00F1 eisenstein_successor_row_split_decoded_add PA00F2 eisenstein_successor_row_split_sum_add PA00F3 eisenstein_fubini_column_count_prefix_succ_restrict PA00F4 eisenstein_transposed_column_decoded_choice PA00F6 eisenstein_transposed_column_counts_extensional PA00F7 eisenstein_fubini_column_count_witness_retarget PA00F8 eisenstein_fubini_column_count_prefix_retarget_predecessor PA00F9 eisenstein_successor_terminal_bit_matches_last_column PA00FA eisenstein_successor_terminal_prefix_to_last_column PA00FB eisenstein_successor_terminal_sum_matches_last_column PA00FC eisenstein_fubini_universal PA00FD eisenstein_constructed_column_total_equals_swapped_total PA00FE eisenstein_rectangle_floor_sum_identity PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity PA00FG distinct_odd_primes_gauss_eisenstein_data_exists