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 m. S n + m = S (n + m)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 m. S n + m = S (n + m)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA000F add_comm PA000Q le_succ_self PA000W le_eq_or_lt PA000X lt_to_le PA0010 lt_irrefl_expanded PA0017 common_divisor_beta_moduli_divides_gap_times_c PA001C division_remainder_succ PA002C lt_not_eq_add_middle PA002O le_succ PA0034 beta_half_range_entry_bounds PA005D predecessor_square_mod_one PA005L quadratic_residue_search_up_to PA0065 factorial_succ_decompose PA0067 drop_add_prefix_from_fixed PA006D odd_mul_odd PA006G odd_add_even PA006I odd_add_odd PA006O lt_trans PA007C gauss_signed_half_magnitude_injective PA007V gauss_predecessor_half_range_aligned PA008F beta_range_one_entry_eq_succ PA0090 euler_pair_iteration_previous_balance PA0091 euler_pair_iteration_step_short PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA009U pair_order_double_succ_length PA00A0 beta_adjacent_target_pairs_product_power PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00A2 prime_two_or_terminal_odd_shape PA00AC pair_order_iteration_previous_balance PA00AD pair_order_iteration_step_room PA00B9 beta_adjacent_unit_pairs_product_one PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BG beta_range_two_product_is_factorial_succ PA00BN bounded_euler_criterion_dichotomy PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00CL odd_reflected_remainder_mod_two PA00CS beta_magnitude_predecessor_recode_aligned_half_range PA00E1 distinct_odd_prime_row_bit_count_equals_decoded_quotient PA00EE complementary_bit_counts_add_lengthDefinition-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.