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
∀ n. ∀ m. ∃ z. ∃ x. ∃ y. (∀ k. Lt(k,m) → ∃ i. BetaAt(x,y,k,i) ∧ (Prime(S k) ∧ (∃ j. PowerValuation(S k,n,j) ∧ Pow(S k,j,i)) ∨ ¬Prime(S k) ∧ i = 1)) ∧ Product(x,y,m,z)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
7 occurrences
In local proof propositions
7 occurrences
Exact expanded native-PA statement
forall n m. exists z. (exists bpr_product_code_bpc_product_exists bpr_product_scale_bpc_product_exists. ((forall bpr_prefix_index_bpc_product_exists_prefix. (exists bpr_gap_bpc_product_exists_prefix_bound. bpr_gap_bpc_product_exists_prefix_bound + S (bpr_prefix_index_bpc_product_exists_prefix) = m) -> exists bpr_prefix_value_bpc_product_exists_prefix. ((((exists bpr_height_bpc_product_exists_prefix_decoded. bpr_height_bpc_product_exists_prefix_decoded + S (bpr_prefix_value_bpc_product_exists_prefix) = S ((S (bpr_prefix_index_bpc_product_exists_prefix)) * bpr_product_scale_bpc_product_exists)) /\ exists bpr_quotient_bpc_product_exists_prefix_decoded. bpr_product_code_bpc_product_exists = bpr_quotient_bpc_product_exists_prefix_decoded * S ((S (bpr_prefix_index_bpc_product_exists_prefix)) * bpr_product_scale_bpc_product_exists) + (bpr_prefix_value_bpc_product_exists_prefix))) /\ (((((~(S (bpr_prefix_index_bpc_product_exists_prefix) = 1) /\ forall bpr_left_bpc_product_exists_prefix_choice_prime bpr_right_bpc_product_exists_prefix_choice_prime. S (bpr_prefix_index_bpc_product_exists_prefix) = bpr_left_bpc_product_exists_prefix_choice_prime * bpr_right_bpc_product_exists_prefix_choice_prime -> bpr_left_bpc_product_exists_prefix_choice_prime = 1 \/ bpr_right_bpc_product_exists_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpc_product_exists_prefix_choice. ((((exists bpr_le_gap_bpc_product_exists_prefix_choice_valuation_selected_bound. bpr_le_gap_bpc_product_exists_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpc_product_exists_prefix_choice) = (n)) /\ (exists bpr_power_value_bpc_product_exists_prefix_choice_valuation_selected. ((exists bpr_power_code_bpc_product_exists_prefix_choice_valuation_selected_power bpr_power_scale_bpc_product_exists_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpc_product_exists_prefix_choice_valuation_selected_power. (exists bpr_gap_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpc_product_exists_prefix_choice) -> (((exists bpr_height_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpc_product_exists_prefix)) = S ((S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpc_product_exists_prefix_choice_valuation_selected_power = bpr_quotient_bpc_product_exists_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpc_product_exists_prefix))))) /\ (exists ff_u_bpc_product_exists_prefix_choice_valuation_selected_power_product ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_start. ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_start. ff_u_bpc_product_exists_prefix_choice_valuation_selected_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpc_product_exists_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpc_product_exists_prefix_choice)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpc_product_exists_prefix_choice_valuation_selected_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpc_product_exists_prefix_choice)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpc_product_exists_prefix_choice_valuation_selected))) /\ forall ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpc_product_exists_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpc_product_exists_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpc_product_exists_prefix_choice) -> exists ff_p_bpc_product_exists_prefix_choice_valuation_selected_power_product ff_r_bpc_product_exists_prefix_choice_valuation_selected_power_product ff_s_bpc_product_exists_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_factor. ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpc_product_exists_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpc_product_exists_prefix_choice_valuation_selected_power = ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_selected_power) + (ff_p_bpc_product_exists_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_partial. ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpc_product_exists_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_partial. ff_u_bpc_product_exists_prefix_choice_valuation_selected_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product) + (ff_r_bpc_product_exists_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_successor. ff_h_bpc_product_exists_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpc_product_exists_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_successor. ff_u_bpc_product_exists_prefix_choice_valuation_selected_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpc_product_exists_prefix_choice_valuation_selected_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_selected_power_product) + (ff_s_bpc_product_exists_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpc_product_exists_prefix_choice_valuation_selected_power_product = ff_r_bpc_product_exists_prefix_choice_valuation_selected_power_product * ff_p_bpc_product_exists_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpc_product_exists_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpc_product_exists_prefix_choice_valuation_selected) * bpr_divides_quotient_bpc_product_exists_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation. (exists bpr_le_gap_bpc_product_exists_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpc_product_exists_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpc_product_exists_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpc_product_exists_prefix_choice_valuation_candidate_power bpr_power_scale_bpc_product_exists_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpc_product_exists_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation) -> (((exists bpr_height_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpc_product_exists_prefix)) = S ((S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpc_product_exists_prefix_choice_valuation_candidate_power = bpr_quotient_bpc_product_exists_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpc_product_exists_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpc_product_exists_prefix))))) /\ (exists ff_u_bpc_product_exists_prefix_choice_valuation_candidate_power_product ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_start. ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_start. ff_u_bpc_product_exists_prefix_choice_valuation_candidate_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpc_product_exists_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpc_product_exists_prefix_choice_valuation_candidate_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpc_product_exists_prefix_choice_valuation_candidate))) /\ forall ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpc_product_exists_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpc_product_exists_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation) -> exists ff_p_bpc_product_exists_prefix_choice_valuation_candidate_power_product ff_r_bpc_product_exists_prefix_choice_valuation_candidate_power_product ff_s_bpc_product_exists_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpc_product_exists_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpc_product_exists_prefix_choice_valuation_candidate_power = ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_valuation_candidate_power) + (ff_p_bpc_product_exists_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpc_product_exists_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpc_product_exists_prefix_choice_valuation_candidate_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product) + (ff_r_bpc_product_exists_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpc_product_exists_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpc_product_exists_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpc_product_exists_prefix_choice_valuation_candidate_power_product = ff_q_bpc_product_exists_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpc_product_exists_prefix_choice_valuation_candidate_power_product)) * ff_v_bpc_product_exists_prefix_choice_valuation_candidate_power_product) + (ff_s_bpc_product_exists_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpc_product_exists_prefix_choice_valuation_candidate_power_product = ff_r_bpc_product_exists_prefix_choice_valuation_candidate_power_product * ff_p_bpc_product_exists_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpc_product_exists_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpc_product_exists_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpc_product_exists_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpc_product_exists_prefix_choice_valuation_candidate_below. bpr_le_gap_bpc_product_exists_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpc_product_exists_prefix_choice_valuation) = (bpr_choice_exponent_bpc_product_exists_prefix_choice))) /\ (exists bpr_power_code_bpc_product_exists_prefix_choice_power bpr_power_scale_bpc_product_exists_prefix_choice_power. ((forall bpr_power_index_bpc_product_exists_prefix_choice_power. (exists bpr_gap_bpc_product_exists_prefix_choice_power_repeat_bound. bpr_gap_bpc_product_exists_prefix_choice_power_repeat_bound + S (bpr_power_index_bpc_product_exists_prefix_choice_power) = bpr_choice_exponent_bpc_product_exists_prefix_choice) -> (((exists bpr_height_bpc_product_exists_prefix_choice_power_repeat_entry. bpr_height_bpc_product_exists_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpc_product_exists_prefix)) = S ((S (bpr_power_index_bpc_product_exists_prefix_choice_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_power)) /\ exists bpr_quotient_bpc_product_exists_prefix_choice_power_repeat_entry. bpr_power_code_bpc_product_exists_prefix_choice_power = bpr_quotient_bpc_product_exists_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpc_product_exists_prefix_choice_power)) * bpr_power_scale_bpc_product_exists_prefix_choice_power) + (S (bpr_prefix_index_bpc_product_exists_prefix))))) /\ (exists ff_u_bpc_product_exists_prefix_choice_power_product ff_v_bpc_product_exists_prefix_choice_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_power_product_start. ff_h_bpc_product_exists_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_power_product_start. ff_u_bpc_product_exists_prefix_choice_power_product = ff_q_bpc_product_exists_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpc_product_exists_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_power_product_terminal. ff_h_bpc_product_exists_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpc_product_exists_prefix) = S ((S (bpr_choice_exponent_bpc_product_exists_prefix_choice)) * ff_v_bpc_product_exists_prefix_choice_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_power_product_terminal. ff_u_bpc_product_exists_prefix_choice_power_product = ff_q_bpc_product_exists_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpc_product_exists_prefix_choice)) * ff_v_bpc_product_exists_prefix_choice_power_product) + (bpr_prefix_value_bpc_product_exists_prefix))) /\ forall ff_i_bpc_product_exists_prefix_choice_power_product. (exists ff_lt_bpc_product_exists_prefix_choice_power_product_bound. ff_lt_bpc_product_exists_prefix_choice_power_product_bound + S ff_i_bpc_product_exists_prefix_choice_power_product = bpr_choice_exponent_bpc_product_exists_prefix_choice) -> exists ff_p_bpc_product_exists_prefix_choice_power_product ff_r_bpc_product_exists_prefix_choice_power_product ff_s_bpc_product_exists_prefix_choice_power_product. ((((exists ff_h_bpc_product_exists_prefix_choice_power_product_factor. ff_h_bpc_product_exists_prefix_choice_power_product_factor + S (ff_p_bpc_product_exists_prefix_choice_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_power)) /\ exists ff_q_bpc_product_exists_prefix_choice_power_product_factor. bpr_power_code_bpc_product_exists_prefix_choice_power = ff_q_bpc_product_exists_prefix_choice_power_product_factor * S ((S (ff_i_bpc_product_exists_prefix_choice_power_product)) * bpr_power_scale_bpc_product_exists_prefix_choice_power) + (ff_p_bpc_product_exists_prefix_choice_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_power_product_partial. ff_h_bpc_product_exists_prefix_choice_power_product_partial + S (ff_r_bpc_product_exists_prefix_choice_power_product) = S ((S (ff_i_bpc_product_exists_prefix_choice_power_product)) * ff_v_bpc_product_exists_prefix_choice_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_power_product_partial. ff_u_bpc_product_exists_prefix_choice_power_product = ff_q_bpc_product_exists_prefix_choice_power_product_partial * S ((S (ff_i_bpc_product_exists_prefix_choice_power_product)) * ff_v_bpc_product_exists_prefix_choice_power_product) + (ff_r_bpc_product_exists_prefix_choice_power_product))) /\ ((((exists ff_h_bpc_product_exists_prefix_choice_power_product_successor. ff_h_bpc_product_exists_prefix_choice_power_product_successor + S (ff_s_bpc_product_exists_prefix_choice_power_product) = S ((S (S ff_i_bpc_product_exists_prefix_choice_power_product)) * ff_v_bpc_product_exists_prefix_choice_power_product)) /\ exists ff_q_bpc_product_exists_prefix_choice_power_product_successor. ff_u_bpc_product_exists_prefix_choice_power_product = ff_q_bpc_product_exists_prefix_choice_power_product_successor * S ((S (S ff_i_bpc_product_exists_prefix_choice_power_product)) * ff_v_bpc_product_exists_prefix_choice_power_product) + (ff_s_bpc_product_exists_prefix_choice_power_product))) /\ ff_s_bpc_product_exists_prefix_choice_power_product = ff_r_bpc_product_exists_prefix_choice_power_product * ff_p_bpc_product_exists_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpc_product_exists_prefix) = 1) /\ forall bpr_left_bpc_product_exists_prefix_choice_prime bpr_right_bpc_product_exists_prefix_choice_prime. S (bpr_prefix_index_bpc_product_exists_prefix) = bpr_left_bpc_product_exists_prefix_choice_prime * bpr_right_bpc_product_exists_prefix_choice_prime -> bpr_left_bpc_product_exists_prefix_choice_prime = 1 \/ bpr_right_bpc_product_exists_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpc_product_exists_prefix = 1))))) /\ (exists ff_u_bpc_product_exists_product ff_v_bpc_product_exists_product. ((((exists ff_h_bpc_product_exists_product_start. ff_h_bpc_product_exists_product_start + S (1) = S ((S (0)) * ff_v_bpc_product_exists_product)) /\ exists ff_q_bpc_product_exists_product_start. ff_u_bpc_product_exists_product = ff_q_bpc_product_exists_product_start * S ((S (0)) * ff_v_bpc_product_exists_product) + (1))) /\ ((((exists ff_h_bpc_product_exists_product_terminal. ff_h_bpc_product_exists_product_terminal + S (z) = S ((S (m)) * ff_v_bpc_product_exists_product)) /\ exists ff_q_bpc_product_exists_product_terminal. ff_u_bpc_product_exists_product = ff_q_bpc_product_exists_product_terminal * S ((S (m)) * ff_v_bpc_product_exists_product) + (z))) /\ forall ff_i_bpc_product_exists_product. (exists ff_lt_bpc_product_exists_product_bound. ff_lt_bpc_product_exists_product_bound + S ff_i_bpc_product_exists_product = m) -> exists ff_p_bpc_product_exists_product ff_r_bpc_product_exists_product ff_s_bpc_product_exists_product. ((((exists ff_h_bpc_product_exists_product_factor. ff_h_bpc_product_exists_product_factor + S (ff_p_bpc_product_exists_product) = S ((S (ff_i_bpc_product_exists_product)) * bpr_product_scale_bpc_product_exists)) /\ exists ff_q_bpc_product_exists_product_factor. bpr_product_code_bpc_product_exists = ff_q_bpc_product_exists_product_factor * S ((S (ff_i_bpc_product_exists_product)) * bpr_product_scale_bpc_product_exists) + (ff_p_bpc_product_exists_product))) /\ ((((exists ff_h_bpc_product_exists_product_partial. ff_h_bpc_product_exists_product_partial + S (ff_r_bpc_product_exists_product) = S ((S (ff_i_bpc_product_exists_product)) * ff_v_bpc_product_exists_product)) /\ exists ff_q_bpc_product_exists_product_partial. ff_u_bpc_product_exists_product = ff_q_bpc_product_exists_product_partial * S ((S (ff_i_bpc_product_exists_product)) * ff_v_bpc_product_exists_product) + (ff_r_bpc_product_exists_product))) /\ ((((exists ff_h_bpc_product_exists_product_successor. ff_h_bpc_product_exists_product_successor + S (ff_s_bpc_product_exists_product) = S ((S (S ff_i_bpc_product_exists_product)) * ff_v_bpc_product_exists_product)) /\ exists ff_q_bpc_product_exists_product_successor. ff_u_bpc_product_exists_product = ff_q_bpc_product_exists_product_successor * S ((S (S ff_i_bpc_product_exists_product)) * ff_v_bpc_product_exists_product) + (ff_s_bpc_product_exists_product))) /\ ff_s_bpc_product_exists_product = ff_r_bpc_product_exists_product * ff_p_bpc_product_exists_product))))))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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.
Named ingredients (2)
01Fix variables and assumptionsL1–2
02Establish hprefixL3–4
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution prefix exists.
- L3
have hprefix : ∃ b. ∃ c. ∀ x. Lt(x,m) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ (∃ z. PowerValuation(S x,n,z) ∧ Pow(S x,z,y)) ∨ ¬Prime(S x) ∧ y = 1)Definitions: Lt(x,m)BetaAt(b,c,x,y)Prime(S x)PowerValuation(S x,n,z)Pow(S x,z,y)Original native command in the exact edition - L4
apply prime_contribution_prefix_exists
03Separate the logical casesL5–6
04Establish hproductL7–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product exists.
- L7
have hproduct : ∃ z. Product(x,x1,m,z)Definitions: Product(x,x1,m,z)Original native command in the exact edition - L8
apply beta_product_exists
05Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
cases hproduct
06Construct an explicit witnessL10–12
07Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
split
Original defined command ledger · 15 lines
- 0001
intro n - 0002
intro m - 0003
have hprefix : ∃ b. ∃ c. ∀ x. Lt(x,m) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ (∃ z. PowerValuation(S x,n,z) ∧ Pow(S x,z,y)) ∨ ¬Prime(S x) ∧ y = 1)Exact native replay line
have hprefix : exists b c. (forall bpr_prefix_index_bpcpx_result. (exists bpr_gap_bpcpx_result_bound. bpr_gap_bpcpx_result_bound + S (bpr_prefix_index_bpcpx_result) = m) -> exists bpr_prefix_value_bpcpx_result. ((((exists bpr_height_bpcpx_result_decoded. bpr_height_bpcpx_result_decoded + S (bpr_prefix_value_bpcpx_result) = S ((S (bpr_prefix_index_bpcpx_result)) * c)) /\ exists bpr_quotient_bpcpx_result_decoded. b = bpr_quotient_bpcpx_result_decoded * S ((S (bpr_prefix_index_bpcpx_result)) * c) + (bpr_prefix_value_bpcpx_result))) /\ (((((~(S (bpr_prefix_index_bpcpx_result) = 1) /\ forall bpr_left_bpcpx_result_choice_prime bpr_right_bpcpx_result_choice_prime. S (bpr_prefix_index_bpcpx_result) = bpr_left_bpcpx_result_choice_prime * bpr_right_bpcpx_result_choice_prime -> bpr_left_bpcpx_result_choice_prime = 1 \/ bpr_right_bpcpx_result_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpx_result_choice. ((((exists bpr_le_gap_bpcpx_result_choice_valuation_selected_bound. bpr_le_gap_bpcpx_result_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpx_result_choice) = (n)) /\ (exists bpr_power_value_bpcpx_result_choice_valuation_selected. ((exists bpr_power_code_bpcpx_result_choice_valuation_selected_power bpr_power_scale_bpcpx_result_choice_valuation_selected_power. ((forall bpr_power_index_bpcpx_result_choice_valuation_selected_power. (exists bpr_gap_bpcpx_result_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpx_result_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_valuation_selected_power) = bpr_choice_exponent_bpcpx_result_choice) -> (((exists bpr_height_bpcpx_result_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpx_result_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpx_result_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpx_result_choice_valuation_selected_power = bpr_quotient_bpcpx_result_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_valuation_selected_power_product ff_v_bpcpx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_start. ff_h_bpcpx_result_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_start. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_terminal. ff_h_bpcpx_result_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpx_result_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_terminal. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (bpr_power_value_bpcpx_result_choice_valuation_selected))) /\ forall ff_i_bpcpx_result_choice_valuation_selected_power_product. (exists ff_lt_bpcpx_result_choice_valuation_selected_power_product_bound. ff_lt_bpcpx_result_choice_valuation_selected_power_product_bound + S ff_i_bpcpx_result_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpx_result_choice) -> exists ff_p_bpcpx_result_choice_valuation_selected_power_product ff_r_bpcpx_result_choice_valuation_selected_power_product ff_s_bpcpx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_factor. ff_h_bpcpx_result_choice_valuation_selected_power_product_factor + S (ff_p_bpcpx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpx_result_choice_valuation_selected_power = ff_q_bpcpx_result_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power) + (ff_p_bpcpx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_partial. ff_h_bpcpx_result_choice_valuation_selected_power_product_partial + S (ff_r_bpcpx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_partial. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (ff_r_bpcpx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_successor. ff_h_bpcpx_result_choice_valuation_selected_power_product_successor + S (ff_s_bpcpx_result_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_successor. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (ff_s_bpcpx_result_choice_valuation_selected_power_product))) /\ ff_s_bpcpx_result_choice_valuation_selected_power_product = ff_r_bpcpx_result_choice_valuation_selected_power_product * ff_p_bpcpx_result_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_result_choice_valuation_selected_divides. n = (bpr_power_value_bpcpx_result_choice_valuation_selected) * bpr_divides_quotient_bpcpx_result_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpx_result_choice_valuation. (exists bpr_le_gap_bpcpx_result_choice_valuation_candidate_bound. bpr_le_gap_bpcpx_result_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpx_result_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpx_result_choice_valuation_candidate. ((exists bpr_power_code_bpcpx_result_choice_valuation_candidate_power bpr_power_scale_bpcpx_result_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpx_result_choice_valuation_candidate_power. (exists bpr_gap_bpcpx_result_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpx_result_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpx_result_choice_valuation) -> (((exists bpr_height_bpcpx_result_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpx_result_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpx_result_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpx_result_choice_valuation_candidate_power = bpr_quotient_bpcpx_result_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_valuation_candidate_power_product ff_v_bpcpx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_start. ff_h_bpcpx_result_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_start. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_terminal. ff_h_bpcpx_result_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpx_result_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpx_result_choice_valuation)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_terminal. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpx_result_choice_valuation)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpx_result_choice_valuation_candidate))) /\ forall ff_i_bpcpx_result_choice_valuation_candidate_power_product. (exists ff_lt_bpcpx_result_choice_valuation_candidate_power_product_bound. ff_lt_bpcpx_result_choice_valuation_candidate_power_product_bound + S ff_i_bpcpx_result_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpx_result_choice_valuation) -> exists ff_p_bpcpx_result_choice_valuation_candidate_power_product ff_r_bpcpx_result_choice_valuation_candidate_power_product ff_s_bpcpx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_factor. ff_h_bpcpx_result_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpx_result_choice_valuation_candidate_power = ff_q_bpcpx_result_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power) + (ff_p_bpcpx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_partial. ff_h_bpcpx_result_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_partial. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (ff_r_bpcpx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_successor. ff_h_bpcpx_result_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_successor. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (ff_s_bpcpx_result_choice_valuation_candidate_power_product))) /\ ff_s_bpcpx_result_choice_valuation_candidate_power_product = ff_r_bpcpx_result_choice_valuation_candidate_power_product * ff_p_bpcpx_result_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_result_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpx_result_choice_valuation_candidate) * bpr_divides_quotient_bpcpx_result_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpx_result_choice_valuation_candidate_below. bpr_le_gap_bpcpx_result_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpx_result_choice_valuation) = (bpr_choice_exponent_bpcpx_result_choice))) /\ (exists bpr_power_code_bpcpx_result_choice_power bpr_power_scale_bpcpx_result_choice_power. ((forall bpr_power_index_bpcpx_result_choice_power. (exists bpr_gap_bpcpx_result_choice_power_repeat_bound. bpr_gap_bpcpx_result_choice_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_power) = bpr_choice_exponent_bpcpx_result_choice) -> (((exists bpr_height_bpcpx_result_choice_power_repeat_entry. bpr_height_bpcpx_result_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_power)) * bpr_power_scale_bpcpx_result_choice_power)) /\ exists bpr_quotient_bpcpx_result_choice_power_repeat_entry. bpr_power_code_bpcpx_result_choice_power = bpr_quotient_bpcpx_result_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_power)) * bpr_power_scale_bpcpx_result_choice_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_power_product ff_v_bpcpx_result_choice_power_product. ((((exists ff_h_bpcpx_result_choice_power_product_start. ff_h_bpcpx_result_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_start. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_terminal. ff_h_bpcpx_result_choice_power_product_terminal + S (bpr_prefix_value_bpcpx_result) = S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_terminal. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_power_product) + (bpr_prefix_value_bpcpx_result))) /\ forall ff_i_bpcpx_result_choice_power_product. (exists ff_lt_bpcpx_result_choice_power_product_bound. ff_lt_bpcpx_result_choice_power_product_bound + S ff_i_bpcpx_result_choice_power_product = bpr_choice_exponent_bpcpx_result_choice) -> exists ff_p_bpcpx_result_choice_power_product ff_r_bpcpx_result_choice_power_product ff_s_bpcpx_result_choice_power_product. ((((exists ff_h_bpcpx_result_choice_power_product_factor. ff_h_bpcpx_result_choice_power_product_factor + S (ff_p_bpcpx_result_choice_power_product) = S ((S (ff_i_bpcpx_result_choice_power_product)) * bpr_power_scale_bpcpx_result_choice_power)) /\ exists ff_q_bpcpx_result_choice_power_product_factor. bpr_power_code_bpcpx_result_choice_power = ff_q_bpcpx_result_choice_power_product_factor * S ((S (ff_i_bpcpx_result_choice_power_product)) * bpr_power_scale_bpcpx_result_choice_power) + (ff_p_bpcpx_result_choice_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_partial. ff_h_bpcpx_result_choice_power_product_partial + S (ff_r_bpcpx_result_choice_power_product) = S ((S (ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_partial. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_partial * S ((S (ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product) + (ff_r_bpcpx_result_choice_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_successor. ff_h_bpcpx_result_choice_power_product_successor + S (ff_s_bpcpx_result_choice_power_product) = S ((S (S ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_successor. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product) + (ff_s_bpcpx_result_choice_power_product))) /\ ff_s_bpcpx_result_choice_power_product = ff_r_bpcpx_result_choice_power_product * ff_p_bpcpx_result_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpx_result) = 1) /\ forall bpr_left_bpcpx_result_choice_prime bpr_right_bpcpx_result_choice_prime. S (bpr_prefix_index_bpcpx_result) = bpr_left_bpcpx_result_choice_prime * bpr_right_bpcpx_result_choice_prime -> bpr_left_bpcpx_result_choice_prime = 1 \/ bpr_right_bpcpx_result_choice_prime = 1)) /\ bpr_prefix_value_bpcpx_result = 1))))) - 0004
apply prime_contribution_prefix_exists - 0005
cases hprefix - 0006
cases hprefix_witness - 0007
have hproduct : ∃ z. Product(x,x1,m,z)Exact native replay line
have hproduct : exists z. (exists ff_u_bpc_product_exists_witness ff_v_bpc_product_exists_witness. ((((exists ff_h_bpc_product_exists_witness_start. ff_h_bpc_product_exists_witness_start + S (1) = S ((S (0)) * ff_v_bpc_product_exists_witness)) /\ exists ff_q_bpc_product_exists_witness_start. ff_u_bpc_product_exists_witness = ff_q_bpc_product_exists_witness_start * S ((S (0)) * ff_v_bpc_product_exists_witness) + (1))) /\ ((((exists ff_h_bpc_product_exists_witness_terminal. ff_h_bpc_product_exists_witness_terminal + S (z) = S ((S (m)) * ff_v_bpc_product_exists_witness)) /\ exists ff_q_bpc_product_exists_witness_terminal. ff_u_bpc_product_exists_witness = ff_q_bpc_product_exists_witness_terminal * S ((S (m)) * ff_v_bpc_product_exists_witness) + (z))) /\ forall ff_i_bpc_product_exists_witness. (exists ff_lt_bpc_product_exists_witness_bound. ff_lt_bpc_product_exists_witness_bound + S ff_i_bpc_product_exists_witness = m) -> exists ff_p_bpc_product_exists_witness ff_r_bpc_product_exists_witness ff_s_bpc_product_exists_witness. ((((exists ff_h_bpc_product_exists_witness_factor. ff_h_bpc_product_exists_witness_factor + S (ff_p_bpc_product_exists_witness) = S ((S (ff_i_bpc_product_exists_witness)) * x1)) /\ exists ff_q_bpc_product_exists_witness_factor. x = ff_q_bpc_product_exists_witness_factor * S ((S (ff_i_bpc_product_exists_witness)) * x1) + (ff_p_bpc_product_exists_witness))) /\ ((((exists ff_h_bpc_product_exists_witness_partial. ff_h_bpc_product_exists_witness_partial + S (ff_r_bpc_product_exists_witness) = S ((S (ff_i_bpc_product_exists_witness)) * ff_v_bpc_product_exists_witness)) /\ exists ff_q_bpc_product_exists_witness_partial. ff_u_bpc_product_exists_witness = ff_q_bpc_product_exists_witness_partial * S ((S (ff_i_bpc_product_exists_witness)) * ff_v_bpc_product_exists_witness) + (ff_r_bpc_product_exists_witness))) /\ ((((exists ff_h_bpc_product_exists_witness_successor. ff_h_bpc_product_exists_witness_successor + S (ff_s_bpc_product_exists_witness) = S ((S (S ff_i_bpc_product_exists_witness)) * ff_v_bpc_product_exists_witness)) /\ exists ff_q_bpc_product_exists_witness_successor. ff_u_bpc_product_exists_witness = ff_q_bpc_product_exists_witness_successor * S ((S (S ff_i_bpc_product_exists_witness)) * ff_v_bpc_product_exists_witness) + (ff_s_bpc_product_exists_witness))) /\ ff_s_bpc_product_exists_witness = ff_r_bpc_product_exists_witness * ff_p_bpc_product_exists_witness)))))) - 0008
apply beta_product_exists - 0009
cases hproduct - 0010
exists x2 - 0011
exists x - 0012
exists x1 - 0013
split - 0014
exact hprefix_witness_witness - 0015
exact hproduct_witness