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 k. (n + m) + k = n + (m + k)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 k. (n + m) + k = n + (m + k)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA000A mul_add PA000G mul_succ_left PA000R le_trans PA0013 factor_difference PA001I add_permute_outer PA001J balanced_bezout_euclid_step PA001W bezout_mod_left PA001X bezout_mod_right PA0024 mod_eq_trans PA0025 mod_eq_predecessor_cancel PA002D positive_quotient_gap_impossible PA0033 lt_of_le_of_lt PA0034 beta_half_range_entry_bounds PA003J add_le_add_right PA003K add_le_add_left PA003P coprime_balanced_mod_inverse PA005D predecessor_square_mod_one PA005N square_decomp PA005O add_residue PA0068 antisymm_from_witnesses PA006D odd_mul_odd PA006F even_add_odd PA006I odd_add_odd PA006N division_block_upper PA006O lt_trans PA006Y odd_upper_remainder_reflection PA0070 gauss_pointwise_signed_half_representative PA0090 euler_pair_iteration_previous_balance PA00A2 prime_two_or_terminal_odd_shape PA00AC pair_order_iteration_previous_balance PA00AD pair_order_iteration_step_room PA00AG prime_bounded_square_one_cases PA00C2 odd_half_strictly_below_modulus PA00C3 odd_half_positive_complement_exists PA00C4 predecessor_multiple_mod_complement PA00CL odd_reflected_remainder_mod_two PA00CM signed_remainder_sum_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00CU beta_sum_replace_balance PA00D1 mod_eq_add_cancel_left PA00D2 mod_two_cancel_middle PA00DQ odd_half_cross_product_gap PA00EP beta_sum_pointwise_addDefinition-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.