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
k = 0 ∨ (∃ x. k = S x ∧ InitialPrimeChain(b,c,x))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
(k = 0 \/ exists pen_last_index_lowerlayer. k = S pen_last_index_lowerlayer /\ ((((exists fs_h_pen_lowerlayer_chain_initial. fs_h_pen_lowerlayer_chain_initial + S (2) = S ((S (0)) * c)) /\ exists fs_q_pen_lowerlayer_chain_initial. b = fs_q_pen_lowerlayer_chain_initial * S ((S (0)) * c) + (2))) /\ forall pen_index_lowerlayer_chain. (exists pc_lt_pen_lowerlayer_chain_bound. pc_lt_pen_lowerlayer_chain_bound + S (pen_index_lowerlayer_chain) = (pen_last_index_lowerlayer)) -> exists pen_previous_lowerlayer_chain pen_following_lowerlayer_chain. (((exists fs_h_pen_lowerlayer_chain_previous. fs_h_pen_lowerlayer_chain_previous + S (pen_previous_lowerlayer_chain) = S ((S (pen_index_lowerlayer_chain)) * c)) /\ exists fs_q_pen_lowerlayer_chain_previous. b = fs_q_pen_lowerlayer_chain_previous * S ((S (pen_index_lowerlayer_chain)) * c) + (pen_previous_lowerlayer_chain))) /\ ((((exists fs_h_pen_lowerlayer_chain_following. fs_h_pen_lowerlayer_chain_following + S (pen_following_lowerlayer_chain) = S ((S (S pen_index_lowerlayer_chain)) * c)) /\ exists fs_q_pen_lowerlayer_chain_following. b = fs_q_pen_lowerlayer_chain_following * S ((S (S pen_index_lowerlayer_chain)) * c) + (pen_following_lowerlayer_chain))) /\ (((~(pen_following_lowerlayer_chain = 1) /\ forall bpr_left_pc_pen_lowerlayer_chain_next_prime bpr_right_pc_pen_lowerlayer_chain_next_prime. pen_following_lowerlayer_chain = bpr_left_pc_pen_lowerlayer_chain_next_prime * bpr_right_pc_pen_lowerlayer_chain_next_prime -> bpr_left_pc_pen_lowerlayer_chain_next_prime = 1 \/ bpr_right_pc_pen_lowerlayer_chain_next_prime = 1)) /\ ((exists pc_lt_pen_lowerlayer_chain_next_greater. pc_lt_pen_lowerlayer_chain_next_greater + S (pen_previous_lowerlayer_chain) = (pen_following_lowerlayer_chain)) /\ forall pen_comparison_lowerlayer_chain_next. ((~(pen_comparison_lowerlayer_chain_next = 1) /\ forall bpr_left_pc_pen_lowerlayer_chain_next_comparison bpr_right_pc_pen_lowerlayer_chain_next_comparison. pen_comparison_lowerlayer_chain_next = bpr_left_pc_pen_lowerlayer_chain_next_comparison * bpr_right_pc_pen_lowerlayer_chain_next_comparison -> bpr_left_pc_pen_lowerlayer_chain_next_comparison = 1 \/ bpr_right_pc_pen_lowerlayer_chain_next_comparison = 1)) -> (exists pc_lt_pen_lowerlayer_chain_next_above. pc_lt_pen_lowerlayer_chain_next_above + S (pen_previous_lowerlayer_chain) = (pen_comparison_lowerlayer_chain_next)) -> (exists pc_le_pen_lowerlayer_chain_next_minimal. pc_le_pen_lowerlayer_chain_next_minimal + (pen_following_lowerlayer_chain) = (pen_comparison_lowerlayer_chain_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
none