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.
Exact expanded PA statement
forall n m. S n + m = S (n + m)Structural proof guide
Generated structural guide
A successor can move through addition on the left.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct 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_lengthFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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.