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.
Readable signature
Sum(b,c,l,z)Exact expansion
exists ff_u_defined_sum ff_v_defined_sum. ((((exists ff_h_defined_sum_start. ff_h_defined_sum_start + S (0) = S ((S (0)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_start. ff_u_defined_sum = ff_q_defined_sum_start * S ((S (0)) * ff_v_defined_sum) + (0))) /\ ((((exists ff_h_defined_sum_terminal. ff_h_defined_sum_terminal + S (z) = S ((S (l)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_terminal. ff_u_defined_sum = ff_q_defined_sum_terminal * S ((S (l)) * ff_v_defined_sum) + (z))) /\ forall ff_i_defined_sum. (exists ff_lt_defined_sum_bound. ff_lt_defined_sum_bound + S ff_i_defined_sum = l) -> exists ff_a_defined_sum ff_r_defined_sum ff_s_defined_sum. ((((exists ff_h_defined_sum_summand. ff_h_defined_sum_summand + S (ff_a_defined_sum) = S ((S (ff_i_defined_sum)) * c)) /\ exists ff_q_defined_sum_summand. b = ff_q_defined_sum_summand * S ((S (ff_i_defined_sum)) * c) + (ff_a_defined_sum))) /\ ((((exists ff_h_defined_sum_partial. ff_h_defined_sum_partial + S (ff_r_defined_sum) = S ((S (ff_i_defined_sum)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_partial. ff_u_defined_sum = ff_q_defined_sum_partial * S ((S (ff_i_defined_sum)) * ff_v_defined_sum) + (ff_r_defined_sum))) /\ ((((exists ff_h_defined_sum_successor. ff_h_defined_sum_successor + S (ff_s_defined_sum) = S ((S (S ff_i_defined_sum)) * ff_v_defined_sum)) /\ exists ff_q_defined_sum_successor. ff_u_defined_sum = ff_q_defined_sum_successor * S ((S (S ff_i_defined_sum)) * ff_v_defined_sum) + (ff_s_defined_sum))) /\ ff_s_defined_sum = ff_r_defined_sum + ff_a_defined_sum)))))This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
Used by theorem statements or local proof propositions
PA003H beta_sum_exists PA003Y beta_sum_succ_decompose PA0042 bit_count_succ_decompose PA0047 beta_sum_zero PA006P beta_sum_functional PA00C1 prime_scaled_half_quotient_sum_exists PA00CQ beta_sum_pointwise_mod_three_add PA00CR gauss_eisenstein_terminal_sums_mod_two PA00CT beta_sum_transport_prefix PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant PA00CW beta_sum_reindex_fixed_last PA00CX beta_sum_permutation_invariant PA00CY beta_magnitude_sum_permutation_exact PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two PA00D6 gauss_eisenstein_sign_count_mod_quotient_sum PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00DM distinct_odd_prime_half_rectangle_total_exists PA00E4 distinct_odd_prime_quotient_sum_transports_to_rectangle PA00E5 distinct_odd_prime_quotient_sum_equals_rectangle_total PA00EJ eisenstein_transposed_column_count_total_exists PA00EK beta_repeat_sum_exact PA00EL beta_repeat_sum_exists_exact PA00EP beta_sum_pointwise_add PA00EQ eisenstein_rectangle_plus_column_count_total PA00ES eisenstein_zero_width_rectangle_sum_zero PA00F2 eisenstein_successor_row_split_sum_add PA00F6 eisenstein_transposed_column_counts_extensional PA00FB eisenstein_successor_terminal_sum_matches_last_column PA00FC eisenstein_fubini_universal PA00FD eisenstein_constructed_column_total_equals_swapped_total PA00FE eisenstein_rectangle_floor_sum_identity PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity PA00FG distinct_odd_primes_gauss_eisenstein_data_exists