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.
Definition in prerequisite notation
∀ ff_i_defined_all_bits. Lt(ff_i_defined_all_bits,l) → ∃ x. BetaAt(b,c,ff_i_defined_all_bits,x) ∧ (x = 0 ∨ x = 1)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
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))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
CD0001 · finite_bit_entry_casesCD0002 · finite_bit_membership_decidableCD0004 · finite_bit_subset_pointwise_leCD0012 · finite_bit_intersection_existsCD0013 · finite_bit_complement_existsCD0015 · finite_bit_union_of_complementsCD0019 · finite_bit_nonmember_zeroCD0020 · finite_modular_composition_all_bitsCD0022 · finite_modular_set_pullback_existsCD002F · finite_modular_sumset_prefix_existsCD0034 · finite_modular_orbit_member_or_boundaryCD0035 · prime_modular_set_translation_boundary_exists