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.
Statement with defined notation
forall n. ~(S n = 0)Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. ~(S n = 0)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA0006 beta_range_empty PA000I bounded_common_multiple_step PA000K bounded_common_multiple_exists PA000U beta_modulus_nonzero PA002I bounded_beta_exclusive_recode_invariant PA0031 prime_nonzero PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0043 beta_repeat_empty PA004F finite_surjective_zero PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA0052 beta_product_replace_balance PA0063 prime_bounded_nonzero_mod_inverse PA006S mul_left_cancel_nonzero PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007G beta_sign_factor_prefix_exists PA007L beta_pointwise_mul_prefix_exists PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008K prime_range_product_coprime PA008R prime_scaled_inverse_prefix_extend PA008S prime_scaled_inverse_prefix_exists_bounded PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA00A4 prime_inverse_index_exists PA00A6 prime_inverse_prefix_exists_bounded PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AB paired_inverse_witness_zero PA00AG prime_bounded_square_one_cases PA00BY beta_division_prefix_exists PA00CU beta_sum_replace_balance PA00D8 distinct_odd_prime_half_products_ne PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00E9 eisenstein_transposed_column_prefix_exists PA00EI eisenstein_transposed_column_count_prefix_exists PA00EX eisenstein_successor_row_split_prefix_existsDefinition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
01Use earlier factsL1–1
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L1
apply PA1