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
AllBits(b,c,l)Exact expansion
forall ff_i_defined_all_bits. (exists ff_lt_defined_all_bits_bound. ff_lt_defined_all_bits_bound + S ff_i_defined_all_bits = l) -> exists ff_bit_defined_all_bits. ((((exists ff_h_defined_all_bits_decoded. ff_h_defined_all_bits_decoded + S (ff_bit_defined_all_bits) = S ((S (ff_i_defined_all_bits)) * c)) /\ exists ff_q_defined_all_bits_decoded. b = ff_q_defined_all_bits_decoded * S ((S (ff_i_defined_all_bits)) * c) + (ff_bit_defined_all_bits))) /\ (ff_bit_defined_all_bits = 0 \/ ff_bit_defined_all_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
Used by theorem statements or local proof propositions
PA003I bit_count_exists PA0040 all_bits_prefix_succ PA0041 all_bits_last_succ PA0042 bit_count_succ_decompose PA0076 gauss_signed_half_prefix_all_bits PA0077 gauss_signed_half_bit_count_exists PA00DE eisenstein_row_indicator_prefix_all_bits PA00DF distinct_odd_prime_half_row_count_exists PA00DU eisenstein_initial_segment_prefix_all_bits PA00DY eisenstein_initial_segment_bit_count_exact PA00EB eisenstein_transposed_column_prefix_all_bits PA00EF eisenstein_row_transposed_column_count_partition PA00F7 eisenstein_fubini_column_count_witness_retarget