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
BetaAt(b,c,0,2) ∧ (∀ x. Lt(x,k) → ∃ y. ∃ z. BetaAt(b,c,x,y) ∧ (BetaAt(b,c,S x,z) ∧ NextPrime(y,z)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(((exists fs_h_pen_lowerlayer_initial. fs_h_pen_lowerlayer_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_lowerlayer_initial. b = fs_q_pen_lowerlayer_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_lowerlayer. (exists pc_lt_pen_lowerlayer_bound. pc_lt_pen_lowerlayer_bound + S (pen_index_lowerlayer) = (k)) -> exists pen_previous_lowerlayer pen_following_lowerlayer. (((exists fs_h_pen_lowerlayer_previous. fs_h_pen_lowerlayer_previous + S (pen_previous_lowerlayer) = S ((S (pen_index_lowerlayer)) * c)) /\ exists fs_q_pen_lowerlayer_previous. b = fs_q_pen_lowerlayer_previous * S ((S (pen_index_lowerlayer)) * c) + (pen_previous_lowerlayer))) /\ ((((exists fs_h_pen_lowerlayer_following. fs_h_pen_lowerlayer_following + S (pen_following_lowerlayer) = S ((S (S pen_index_lowerlayer)) * c)) /\ exists fs_q_pen_lowerlayer_following. b = fs_q_pen_lowerlayer_following * S ((S (S pen_index_lowerlayer)) * c) + (pen_following_lowerlayer))) /\ (((~(pen_following_lowerlayer = 1) /\ forall bpr_left_pc_pen_lowerlayer_next_prime bpr_right_pc_pen_lowerlayer_next_prime. pen_following_lowerlayer = bpr_left_pc_pen_lowerlayer_next_prime * bpr_right_pc_pen_lowerlayer_next_prime -> bpr_left_pc_pen_lowerlayer_next_prime = 1 \/ bpr_right_pc_pen_lowerlayer_next_prime = 1)) /\ ((exists pc_lt_pen_lowerlayer_next_greater. pc_lt_pen_lowerlayer_next_greater + S (pen_previous_lowerlayer) = (pen_following_lowerlayer)) /\ forall pen_comparison_lowerlayer_next. ((~(pen_comparison_lowerlayer_next = 1) /\ forall bpr_left_pc_pen_lowerlayer_next_comparison bpr_right_pc_pen_lowerlayer_next_comparison. pen_comparison_lowerlayer_next = bpr_left_pc_pen_lowerlayer_next_comparison * bpr_right_pc_pen_lowerlayer_next_comparison -> bpr_left_pc_pen_lowerlayer_next_comparison = 1 \/ bpr_right_pc_pen_lowerlayer_next_comparison = 1)) -> (exists pc_lt_pen_lowerlayer_next_above. pc_lt_pen_lowerlayer_next_above + S (pen_previous_lowerlayer) = (pen_comparison_lowerlayer_next)) -> (exists pc_le_pen_lowerlayer_next_minimal. pc_le_pen_lowerlayer_next_minimal + (pen_following_lowerlayer) = (pen_comparison_lowerlayer_next)))))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
PE0007 · initial_prime_chain_singleton_existsPE0008 · initial_prime_chain_prefix_extendPE0009 · initial_prime_chain_prefix_restrictPE000A · initial_prime_chain_terminal_is_primePE000B · initial_prime_chain_bounded_existsPE000C · first_primes_double_exponential_boundPE000D · initial_prime_chain_strict_orderPE000E · initial_prime_chain_exhausts_primesPE000F · prime_list_nonempty_chain