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
∀ pc_index_secondwave. Lt(pc_index_secondwave,l) → ∃ x. BetaAt(d,f,pc_index_secondwave,x) ∧ (Lt(pc_index_secondwave,u) ∧ x = 0 ∨ Le(u,pc_index_secondwave) ∧ BetaAt(b,c,pc_index_secondwave,x))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pc_index_secondwave. (exists pc_lt_secondwave_bound. pc_lt_secondwave_bound + S (pc_index_secondwave) = (l)) -> exists pc_bit_secondwave. (((exists fs_h_pc_secondwave_entry. fs_h_pc_secondwave_entry + S (pc_bit_secondwave) = S ((S (pc_index_secondwave)) * f)) /\ exists fs_q_pc_secondwave_entry. d = fs_q_pc_secondwave_entry * S ((S (pc_index_secondwave)) * f) + (pc_bit_secondwave))) /\ ((((exists pc_lt_secondwave_choice_below. pc_lt_secondwave_choice_below + S (pc_index_secondwave) = (u)) /\ pc_bit_secondwave = 0) \/ ((exists pc_le_secondwave_choice_above. pc_le_secondwave_choice_above + (u) = (pc_index_secondwave)) /\ (((exists fs_h_pc_secondwave_choice_source. fs_h_pc_secondwave_choice_source + S (pc_bit_secondwave) = S ((S (pc_index_secondwave)) * c)) /\ exists fs_q_pc_secondwave_choice_source. b = fs_q_pc_secondwave_choice_source * S ((S (pc_index_secondwave)) * c) + (pc_bit_secondwave))))))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
none
Checked theorems using this definition
PC000F · beta_cutoff_prefix_emptyPC0010 · beta_cutoff_prefix_drop_lastPC0011 · beta_cutoff_prefix_entryPC0012 · beta_cutoff_prefix_extendPC0013 · beta_cutoff_prefix_existsPC0014 · beta_cutoff_count_comparisonPC001E · primorial_cutoff_weighted_lowerPC0020 · primorial_cutoff_count_power_boundPC0028 · prime_cutoff_exponent_boundPC002A · prime_count_chebyshev_upper