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
Product(b,c,l,z)Exact expansion
exists ff_u_defined_product ff_v_defined_product. ((((exists ff_h_defined_product_start. ff_h_defined_product_start + S (1) = S ((S (0)) * ff_v_defined_product)) /\ exists ff_q_defined_product_start. ff_u_defined_product = ff_q_defined_product_start * S ((S (0)) * ff_v_defined_product) + (1))) /\ ((((exists ff_h_defined_product_terminal. ff_h_defined_product_terminal + S (z) = S ((S (l)) * ff_v_defined_product)) /\ exists ff_q_defined_product_terminal. ff_u_defined_product = ff_q_defined_product_terminal * S ((S (l)) * ff_v_defined_product) + (z))) /\ forall ff_i_defined_product. (exists ff_lt_defined_product_bound. ff_lt_defined_product_bound + S ff_i_defined_product = l) -> exists ff_p_defined_product ff_r_defined_product ff_s_defined_product. ((((exists ff_h_defined_product_factor. ff_h_defined_product_factor + S (ff_p_defined_product) = S ((S (ff_i_defined_product)) * c)) /\ exists ff_q_defined_product_factor. b = ff_q_defined_product_factor * S ((S (ff_i_defined_product)) * c) + (ff_p_defined_product))) /\ ((((exists ff_h_defined_product_partial. ff_h_defined_product_partial + S (ff_r_defined_product) = S ((S (ff_i_defined_product)) * ff_v_defined_product)) /\ exists ff_q_defined_product_partial. ff_u_defined_product = ff_q_defined_product_partial * S ((S (ff_i_defined_product)) * ff_v_defined_product) + (ff_r_defined_product))) /\ ((((exists ff_h_defined_product_successor. ff_h_defined_product_successor + S (ff_s_defined_product) = S ((S (S ff_i_defined_product)) * ff_v_defined_product)) /\ exists ff_q_defined_product_successor. ff_u_defined_product = ff_q_defined_product_successor * S ((S (S ff_i_defined_product)) * ff_v_defined_product) + (ff_s_defined_product))) /\ ff_s_defined_product = ff_r_defined_product * ff_p_defined_product)))))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
PA003X beta_product_exists PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004D pow_successor_decompose PA004Y beta_product_transport_prefix PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA005G pow_functional PA0065 factorial_succ_decompose PA006B factorial_functional PA007I beta_sign_factor_product_power PA007J beta_sign_factor_product_power_exists PA007N beta_product_pointwise_mul_exact PA007O beta_pointwise_mul_product_exists PA007Q beta_product_pointwise_scale_mod PA007R gauss_signed_pointwise_mul_product_mod PA007W beta_product_reindex_fixed_last PA007X beta_product_permutation_invariant PA007Y gauss_magnitude_product_eq_half_range PA0080 gauss_signed_products_balance_mod PA0081 beta_product_pointwise_coprime PA0082 prime_positive_bounded_product_coprime PA0083 prime_half_range_product_coprime PA0084 gauss_signed_products_cancel_mod PA0085 gauss_lemma_power_congruence_exists PA008J prime_mul_residue_product_balance PA008K prime_range_product_coprime PA009Y beta_product_double_succ_decompose PA00A0 beta_adjacent_target_pairs_product_power PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00B9 beta_adjacent_unit_pairs_product_one PA00BA paired_pair_order_product_one_exists PA00BD pair_order_terminal_successor_product_eq_range_two PA00BE prime_wilson_terminal_product_package_exists PA00BF prime_terminal_range_two_product_mod_one_exists PA00BG beta_range_two_product_is_factorial_succ PA00BH beta_range_two_product_restore_last PA00BJ prime_factorial_wilson_congruence PA00BK scaled_pair_order_terminal_power_mod_predecessor