lte_valuation_product_exact

Exact expanded first-order arithmetic statement

forall p a b e f. (~((p) = 1) /\ forall pvs_left_product_prime pvs_right_product_prime. (p) = pvs_left_product_prime * pvs_right_product_prime -> pvs_left_product_prime = 1 \/ pvs_right_product_prime = 1) -> ~(a = 0) -> ~(b = 0) -> (((exists bpd_gap_pvs_product_left_selected_bound. bpd_gap_pvs_product_left_selected_bound + (e) = (a)) /\ (exists bpvi_result_pvs_product_left_selected. ((exists bpvi_b_pvs_product_left_selected_power bpvi_c_pvs_product_left_selected_power. ((forall bpvi_i_pvs_product_left_selected_power. (exists bpvi_repeat_gap_pvs_product_left_selected_power. bpvi_repeat_gap_pvs_product_left_selected_power + S bpvi_i_pvs_product_left_selected_power = e) -> (((exists bpvi_h_pvs_product_left_selected_power_repeat. bpvi_h_pvs_product_left_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_left_selected_power)) * bpvi_c_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_repeat. bpvi_b_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_repeat * S ((S (bpvi_i_pvs_product_left_selected_power)) * bpvi_c_pvs_product_left_selected_power) + (p)))) /\ (exists bpvi_u_pvs_product_left_selected_power bpvi_v_pvs_product_left_selected_power. ((((exists bpvi_h_pvs_product_left_selected_power_start. bpvi_h_pvs_product_left_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_start. bpvi_u_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_start * S ((S (0)) * bpvi_v_pvs_product_left_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_product_left_selected_power_terminal. bpvi_h_pvs_product_left_selected_power_terminal + S (bpvi_result_pvs_product_left_selected) = S ((S (e)) * bpvi_v_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_terminal. bpvi_u_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_product_left_selected_power) + (bpvi_result_pvs_product_left_selected))) /\ forall bpvi_j_pvs_product_left_selected_power. (exists bpvi_product_gap_pvs_product_left_selected_power. bpvi_product_gap_pvs_product_left_selected_power + S bpvi_j_pvs_product_left_selected_power = e) -> exists bpvi_factor_pvs_product_left_selected_power bpvi_partial_pvs_product_left_selected_power bpvi_successor_pvs_product_left_selected_power. ((((exists bpvi_h_pvs_product_left_selected_power_factor. bpvi_h_pvs_product_left_selected_power_factor + S (bpvi_factor_pvs_product_left_selected_power) = S ((S (bpvi_j_pvs_product_left_selected_power)) * bpvi_c_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_factor. bpvi_b_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_factor * S ((S (bpvi_j_pvs_product_left_selected_power)) * bpvi_c_pvs_product_left_selected_power) + (bpvi_factor_pvs_product_left_selected_power))) /\ ((((exists bpvi_h_pvs_product_left_selected_power_partial. bpvi_h_pvs_product_left_selected_power_partial + S (bpvi_partial_pvs_product_left_selected_power) = S ((S (bpvi_j_pvs_product_left_selected_power)) * bpvi_v_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_partial. bpvi_u_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_partial * S ((S (bpvi_j_pvs_product_left_selected_power)) * bpvi_v_pvs_product_left_selected_power) + (bpvi_partial_pvs_product_left_selected_power))) /\ ((((exists bpvi_h_pvs_product_left_selected_power_successor. bpvi_h_pvs_product_left_selected_power_successor + S (bpvi_successor_pvs_product_left_selected_power) = S ((S (S bpvi_j_pvs_product_left_selected_power)) * bpvi_v_pvs_product_left_selected_power)) /\ exists bpvi_q_pvs_product_left_selected_power_successor. bpvi_u_pvs_product_left_selected_power = bpvi_q_pvs_product_left_selected_power_successor * S ((S (S bpvi_j_pvs_product_left_selected_power)) * bpvi_v_pvs_product_left_selected_power) + (bpvi_successor_pvs_product_left_selected_power))) /\ bpvi_successor_pvs_product_left_selected_power = bpvi_partial_pvs_product_left_selected_power * bpvi_factor_pvs_product_left_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_left_selected. a = bpvi_result_pvs_product_left_selected * bpvi_divisor_factor_pvs_product_left_selected))) /\ forall bpd_candidate_pvs_product_left. (exists bpd_gap_pvs_product_left_candidate_bound. bpd_gap_pvs_product_left_candidate_bound + (bpd_candidate_pvs_product_left) = (a)) -> (exists bpvi_result_pvs_product_left_candidate. ((exists bpvi_b_pvs_product_left_candidate_power bpvi_c_pvs_product_left_candidate_power. ((forall bpvi_i_pvs_product_left_candidate_power. (exists bpvi_repeat_gap_pvs_product_left_candidate_power. bpvi_repeat_gap_pvs_product_left_candidate_power + S bpvi_i_pvs_product_left_candidate_power = bpd_candidate_pvs_product_left) -> (((exists bpvi_h_pvs_product_left_candidate_power_repeat. bpvi_h_pvs_product_left_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_left_candidate_power)) * bpvi_c_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_repeat. bpvi_b_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_repeat * S ((S (bpvi_i_pvs_product_left_candidate_power)) * bpvi_c_pvs_product_left_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_product_left_candidate_power bpvi_v_pvs_product_left_candidate_power. ((((exists bpvi_h_pvs_product_left_candidate_power_start. bpvi_h_pvs_product_left_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_start. bpvi_u_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_start * S ((S (0)) * bpvi_v_pvs_product_left_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_product_left_candidate_power_terminal. bpvi_h_pvs_product_left_candidate_power_terminal + S (bpvi_result_pvs_product_left_candidate) = S ((S (bpd_candidate_pvs_product_left)) * bpvi_v_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_terminal. bpvi_u_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_terminal * S ((S (bpd_candidate_pvs_product_left)) * bpvi_v_pvs_product_left_candidate_power) + (bpvi_result_pvs_product_left_candidate))) /\ forall bpvi_j_pvs_product_left_candidate_power. (exists bpvi_product_gap_pvs_product_left_candidate_power. bpvi_product_gap_pvs_product_left_candidate_power + S bpvi_j_pvs_product_left_candidate_power = bpd_candidate_pvs_product_left) -> exists bpvi_factor_pvs_product_left_candidate_power bpvi_partial_pvs_product_left_candidate_power bpvi_successor_pvs_product_left_candidate_power. ((((exists bpvi_h_pvs_product_left_candidate_power_factor. bpvi_h_pvs_product_left_candidate_power_factor + S (bpvi_factor_pvs_product_left_candidate_power) = S ((S (bpvi_j_pvs_product_left_candidate_power)) * bpvi_c_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_factor. bpvi_b_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_factor * S ((S (bpvi_j_pvs_product_left_candidate_power)) * bpvi_c_pvs_product_left_candidate_power) + (bpvi_factor_pvs_product_left_candidate_power))) /\ ((((exists bpvi_h_pvs_product_left_candidate_power_partial. bpvi_h_pvs_product_left_candidate_power_partial + S (bpvi_partial_pvs_product_left_candidate_power) = S ((S (bpvi_j_pvs_product_left_candidate_power)) * bpvi_v_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_partial. bpvi_u_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_partial * S ((S (bpvi_j_pvs_product_left_candidate_power)) * bpvi_v_pvs_product_left_candidate_power) + (bpvi_partial_pvs_product_left_candidate_power))) /\ ((((exists bpvi_h_pvs_product_left_candidate_power_successor. bpvi_h_pvs_product_left_candidate_power_successor + S (bpvi_successor_pvs_product_left_candidate_power) = S ((S (S bpvi_j_pvs_product_left_candidate_power)) * bpvi_v_pvs_product_left_candidate_power)) /\ exists bpvi_q_pvs_product_left_candidate_power_successor. bpvi_u_pvs_product_left_candidate_power = bpvi_q_pvs_product_left_candidate_power_successor * S ((S (S bpvi_j_pvs_product_left_candidate_power)) * bpvi_v_pvs_product_left_candidate_power) + (bpvi_successor_pvs_product_left_candidate_power))) /\ bpvi_successor_pvs_product_left_candidate_power = bpvi_partial_pvs_product_left_candidate_power * bpvi_factor_pvs_product_left_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_left_candidate. a = bpvi_result_pvs_product_left_candidate * bpvi_divisor_factor_pvs_product_left_candidate)) -> (exists bpd_gap_pvs_product_left_maximal. bpd_gap_pvs_product_left_maximal + (bpd_candidate_pvs_product_left) = (e))) -> (((exists bpd_gap_pvs_product_right_selected_bound. bpd_gap_pvs_product_right_selected_bound + (f) = (b)) /\ (exists bpvi_result_pvs_product_right_selected. ((exists bpvi_b_pvs_product_right_selected_power bpvi_c_pvs_product_right_selected_power. ((forall bpvi_i_pvs_product_right_selected_power. (exists bpvi_repeat_gap_pvs_product_right_selected_power. bpvi_repeat_gap_pvs_product_right_selected_power + S bpvi_i_pvs_product_right_selected_power = f) -> (((exists bpvi_h_pvs_product_right_selected_power_repeat. bpvi_h_pvs_product_right_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_right_selected_power)) * bpvi_c_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_repeat. bpvi_b_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_repeat * S ((S (bpvi_i_pvs_product_right_selected_power)) * bpvi_c_pvs_product_right_selected_power) + (p)))) /\ (exists bpvi_u_pvs_product_right_selected_power bpvi_v_pvs_product_right_selected_power. ((((exists bpvi_h_pvs_product_right_selected_power_start. bpvi_h_pvs_product_right_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_start. bpvi_u_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_start * S ((S (0)) * bpvi_v_pvs_product_right_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_product_right_selected_power_terminal. bpvi_h_pvs_product_right_selected_power_terminal + S (bpvi_result_pvs_product_right_selected) = S ((S (f)) * bpvi_v_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_terminal. bpvi_u_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_product_right_selected_power) + (bpvi_result_pvs_product_right_selected))) /\ forall bpvi_j_pvs_product_right_selected_power. (exists bpvi_product_gap_pvs_product_right_selected_power. bpvi_product_gap_pvs_product_right_selected_power + S bpvi_j_pvs_product_right_selected_power = f) -> exists bpvi_factor_pvs_product_right_selected_power bpvi_partial_pvs_product_right_selected_power bpvi_successor_pvs_product_right_selected_power. ((((exists bpvi_h_pvs_product_right_selected_power_factor. bpvi_h_pvs_product_right_selected_power_factor + S (bpvi_factor_pvs_product_right_selected_power) = S ((S (bpvi_j_pvs_product_right_selected_power)) * bpvi_c_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_factor. bpvi_b_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_factor * S ((S (bpvi_j_pvs_product_right_selected_power)) * bpvi_c_pvs_product_right_selected_power) + (bpvi_factor_pvs_product_right_selected_power))) /\ ((((exists bpvi_h_pvs_product_right_selected_power_partial. bpvi_h_pvs_product_right_selected_power_partial + S (bpvi_partial_pvs_product_right_selected_power) = S ((S (bpvi_j_pvs_product_right_selected_power)) * bpvi_v_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_partial. bpvi_u_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_partial * S ((S (bpvi_j_pvs_product_right_selected_power)) * bpvi_v_pvs_product_right_selected_power) + (bpvi_partial_pvs_product_right_selected_power))) /\ ((((exists bpvi_h_pvs_product_right_selected_power_successor. bpvi_h_pvs_product_right_selected_power_successor + S (bpvi_successor_pvs_product_right_selected_power) = S ((S (S bpvi_j_pvs_product_right_selected_power)) * bpvi_v_pvs_product_right_selected_power)) /\ exists bpvi_q_pvs_product_right_selected_power_successor. bpvi_u_pvs_product_right_selected_power = bpvi_q_pvs_product_right_selected_power_successor * S ((S (S bpvi_j_pvs_product_right_selected_power)) * bpvi_v_pvs_product_right_selected_power) + (bpvi_successor_pvs_product_right_selected_power))) /\ bpvi_successor_pvs_product_right_selected_power = bpvi_partial_pvs_product_right_selected_power * bpvi_factor_pvs_product_right_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_right_selected. b = bpvi_result_pvs_product_right_selected * bpvi_divisor_factor_pvs_product_right_selected))) /\ forall bpd_candidate_pvs_product_right. (exists bpd_gap_pvs_product_right_candidate_bound. bpd_gap_pvs_product_right_candidate_bound + (bpd_candidate_pvs_product_right) = (b)) -> (exists bpvi_result_pvs_product_right_candidate. ((exists bpvi_b_pvs_product_right_candidate_power bpvi_c_pvs_product_right_candidate_power. ((forall bpvi_i_pvs_product_right_candidate_power. (exists bpvi_repeat_gap_pvs_product_right_candidate_power. bpvi_repeat_gap_pvs_product_right_candidate_power + S bpvi_i_pvs_product_right_candidate_power = bpd_candidate_pvs_product_right) -> (((exists bpvi_h_pvs_product_right_candidate_power_repeat. bpvi_h_pvs_product_right_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_right_candidate_power)) * bpvi_c_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_repeat. bpvi_b_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_repeat * S ((S (bpvi_i_pvs_product_right_candidate_power)) * bpvi_c_pvs_product_right_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_product_right_candidate_power bpvi_v_pvs_product_right_candidate_power. ((((exists bpvi_h_pvs_product_right_candidate_power_start. bpvi_h_pvs_product_right_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_start. bpvi_u_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_start * S ((S (0)) * bpvi_v_pvs_product_right_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_product_right_candidate_power_terminal. bpvi_h_pvs_product_right_candidate_power_terminal + S (bpvi_result_pvs_product_right_candidate) = S ((S (bpd_candidate_pvs_product_right)) * bpvi_v_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_terminal. bpvi_u_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_terminal * S ((S (bpd_candidate_pvs_product_right)) * bpvi_v_pvs_product_right_candidate_power) + (bpvi_result_pvs_product_right_candidate))) /\ forall bpvi_j_pvs_product_right_candidate_power. (exists bpvi_product_gap_pvs_product_right_candidate_power. bpvi_product_gap_pvs_product_right_candidate_power + S bpvi_j_pvs_product_right_candidate_power = bpd_candidate_pvs_product_right) -> exists bpvi_factor_pvs_product_right_candidate_power bpvi_partial_pvs_product_right_candidate_power bpvi_successor_pvs_product_right_candidate_power. ((((exists bpvi_h_pvs_product_right_candidate_power_factor. bpvi_h_pvs_product_right_candidate_power_factor + S (bpvi_factor_pvs_product_right_candidate_power) = S ((S (bpvi_j_pvs_product_right_candidate_power)) * bpvi_c_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_factor. bpvi_b_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_factor * S ((S (bpvi_j_pvs_product_right_candidate_power)) * bpvi_c_pvs_product_right_candidate_power) + (bpvi_factor_pvs_product_right_candidate_power))) /\ ((((exists bpvi_h_pvs_product_right_candidate_power_partial. bpvi_h_pvs_product_right_candidate_power_partial + S (bpvi_partial_pvs_product_right_candidate_power) = S ((S (bpvi_j_pvs_product_right_candidate_power)) * bpvi_v_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_partial. bpvi_u_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_partial * S ((S (bpvi_j_pvs_product_right_candidate_power)) * bpvi_v_pvs_product_right_candidate_power) + (bpvi_partial_pvs_product_right_candidate_power))) /\ ((((exists bpvi_h_pvs_product_right_candidate_power_successor. bpvi_h_pvs_product_right_candidate_power_successor + S (bpvi_successor_pvs_product_right_candidate_power) = S ((S (S bpvi_j_pvs_product_right_candidate_power)) * bpvi_v_pvs_product_right_candidate_power)) /\ exists bpvi_q_pvs_product_right_candidate_power_successor. bpvi_u_pvs_product_right_candidate_power = bpvi_q_pvs_product_right_candidate_power_successor * S ((S (S bpvi_j_pvs_product_right_candidate_power)) * bpvi_v_pvs_product_right_candidate_power) + (bpvi_successor_pvs_product_right_candidate_power))) /\ bpvi_successor_pvs_product_right_candidate_power = bpvi_partial_pvs_product_right_candidate_power * bpvi_factor_pvs_product_right_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_right_candidate. b = bpvi_result_pvs_product_right_candidate * bpvi_divisor_factor_pvs_product_right_candidate)) -> (exists bpd_gap_pvs_product_right_maximal. bpd_gap_pvs_product_right_maximal + (bpd_candidate_pvs_product_right) = (f))) -> (((exists bpd_gap_pvs_product_result_selected_bound. bpd_gap_pvs_product_result_selected_bound + (e + f) = (a * b)) /\ (exists bpvi_result_pvs_product_result_selected. ((exists bpvi_b_pvs_product_result_selected_power bpvi_c_pvs_product_result_selected_power. ((forall bpvi_i_pvs_product_result_selected_power. (exists bpvi_repeat_gap_pvs_product_result_selected_power. bpvi_repeat_gap_pvs_product_result_selected_power + S bpvi_i_pvs_product_result_selected_power = e + f) -> (((exists bpvi_h_pvs_product_result_selected_power_repeat. bpvi_h_pvs_product_result_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_result_selected_power)) * bpvi_c_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_repeat. bpvi_b_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_repeat * S ((S (bpvi_i_pvs_product_result_selected_power)) * bpvi_c_pvs_product_result_selected_power) + (p)))) /\ (exists bpvi_u_pvs_product_result_selected_power bpvi_v_pvs_product_result_selected_power. ((((exists bpvi_h_pvs_product_result_selected_power_start. bpvi_h_pvs_product_result_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_start. bpvi_u_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_start * S ((S (0)) * bpvi_v_pvs_product_result_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_product_result_selected_power_terminal. bpvi_h_pvs_product_result_selected_power_terminal + S (bpvi_result_pvs_product_result_selected) = S ((S (e + f)) * bpvi_v_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_terminal. bpvi_u_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_terminal * S ((S (e + f)) * bpvi_v_pvs_product_result_selected_power) + (bpvi_result_pvs_product_result_selected))) /\ forall bpvi_j_pvs_product_result_selected_power. (exists bpvi_product_gap_pvs_product_result_selected_power. bpvi_product_gap_pvs_product_result_selected_power + S bpvi_j_pvs_product_result_selected_power = e + f) -> exists bpvi_factor_pvs_product_result_selected_power bpvi_partial_pvs_product_result_selected_power bpvi_successor_pvs_product_result_selected_power. ((((exists bpvi_h_pvs_product_result_selected_power_factor. bpvi_h_pvs_product_result_selected_power_factor + S (bpvi_factor_pvs_product_result_selected_power) = S ((S (bpvi_j_pvs_product_result_selected_power)) * bpvi_c_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_factor. bpvi_b_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_factor * S ((S (bpvi_j_pvs_product_result_selected_power)) * bpvi_c_pvs_product_result_selected_power) + (bpvi_factor_pvs_product_result_selected_power))) /\ ((((exists bpvi_h_pvs_product_result_selected_power_partial. bpvi_h_pvs_product_result_selected_power_partial + S (bpvi_partial_pvs_product_result_selected_power) = S ((S (bpvi_j_pvs_product_result_selected_power)) * bpvi_v_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_partial. bpvi_u_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_partial * S ((S (bpvi_j_pvs_product_result_selected_power)) * bpvi_v_pvs_product_result_selected_power) + (bpvi_partial_pvs_product_result_selected_power))) /\ ((((exists bpvi_h_pvs_product_result_selected_power_successor. bpvi_h_pvs_product_result_selected_power_successor + S (bpvi_successor_pvs_product_result_selected_power) = S ((S (S bpvi_j_pvs_product_result_selected_power)) * bpvi_v_pvs_product_result_selected_power)) /\ exists bpvi_q_pvs_product_result_selected_power_successor. bpvi_u_pvs_product_result_selected_power = bpvi_q_pvs_product_result_selected_power_successor * S ((S (S bpvi_j_pvs_product_result_selected_power)) * bpvi_v_pvs_product_result_selected_power) + (bpvi_successor_pvs_product_result_selected_power))) /\ bpvi_successor_pvs_product_result_selected_power = bpvi_partial_pvs_product_result_selected_power * bpvi_factor_pvs_product_result_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_result_selected. a * b = bpvi_result_pvs_product_result_selected * bpvi_divisor_factor_pvs_product_result_selected))) /\ forall bpd_candidate_pvs_product_result. (exists bpd_gap_pvs_product_result_candidate_bound. bpd_gap_pvs_product_result_candidate_bound + (bpd_candidate_pvs_product_result) = (a * b)) -> (exists bpvi_result_pvs_product_result_candidate. ((exists bpvi_b_pvs_product_result_candidate_power bpvi_c_pvs_product_result_candidate_power. ((forall bpvi_i_pvs_product_result_candidate_power. (exists bpvi_repeat_gap_pvs_product_result_candidate_power. bpvi_repeat_gap_pvs_product_result_candidate_power + S bpvi_i_pvs_product_result_candidate_power = bpd_candidate_pvs_product_result) -> (((exists bpvi_h_pvs_product_result_candidate_power_repeat. bpvi_h_pvs_product_result_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_product_result_candidate_power)) * bpvi_c_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_repeat. bpvi_b_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_repeat * S ((S (bpvi_i_pvs_product_result_candidate_power)) * bpvi_c_pvs_product_result_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_product_result_candidate_power bpvi_v_pvs_product_result_candidate_power. ((((exists bpvi_h_pvs_product_result_candidate_power_start. bpvi_h_pvs_product_result_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_start. bpvi_u_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_start * S ((S (0)) * bpvi_v_pvs_product_result_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_product_result_candidate_power_terminal. bpvi_h_pvs_product_result_candidate_power_terminal + S (bpvi_result_pvs_product_result_candidate) = S ((S (bpd_candidate_pvs_product_result)) * bpvi_v_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_terminal. bpvi_u_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_terminal * S ((S (bpd_candidate_pvs_product_result)) * bpvi_v_pvs_product_result_candidate_power) + (bpvi_result_pvs_product_result_candidate))) /\ forall bpvi_j_pvs_product_result_candidate_power. (exists bpvi_product_gap_pvs_product_result_candidate_power. bpvi_product_gap_pvs_product_result_candidate_power + S bpvi_j_pvs_product_result_candidate_power = bpd_candidate_pvs_product_result) -> exists bpvi_factor_pvs_product_result_candidate_power bpvi_partial_pvs_product_result_candidate_power bpvi_successor_pvs_product_result_candidate_power. ((((exists bpvi_h_pvs_product_result_candidate_power_factor. bpvi_h_pvs_product_result_candidate_power_factor + S (bpvi_factor_pvs_product_result_candidate_power) = S ((S (bpvi_j_pvs_product_result_candidate_power)) * bpvi_c_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_factor. bpvi_b_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_factor * S ((S (bpvi_j_pvs_product_result_candidate_power)) * bpvi_c_pvs_product_result_candidate_power) + (bpvi_factor_pvs_product_result_candidate_power))) /\ ((((exists bpvi_h_pvs_product_result_candidate_power_partial. bpvi_h_pvs_product_result_candidate_power_partial + S (bpvi_partial_pvs_product_result_candidate_power) = S ((S (bpvi_j_pvs_product_result_candidate_power)) * bpvi_v_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_partial. bpvi_u_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_partial * S ((S (bpvi_j_pvs_product_result_candidate_power)) * bpvi_v_pvs_product_result_candidate_power) + (bpvi_partial_pvs_product_result_candidate_power))) /\ ((((exists bpvi_h_pvs_product_result_candidate_power_successor. bpvi_h_pvs_product_result_candidate_power_successor + S (bpvi_successor_pvs_product_result_candidate_power) = S ((S (S bpvi_j_pvs_product_result_candidate_power)) * bpvi_v_pvs_product_result_candidate_power)) /\ exists bpvi_q_pvs_product_result_candidate_power_successor. bpvi_u_pvs_product_result_candidate_power = bpvi_q_pvs_product_result_candidate_power_successor * S ((S (S bpvi_j_pvs_product_result_candidate_power)) * bpvi_v_pvs_product_result_candidate_power) + (bpvi_successor_pvs_product_result_candidate_power))) /\ bpvi_successor_pvs_product_result_candidate_power = bpvi_partial_pvs_product_result_candidate_power * bpvi_factor_pvs_product_result_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_product_result_candidate. a * b = bpvi_result_pvs_product_result_candidate * bpvi_divisor_factor_pvs_product_result_candidate)) -> (exists bpd_gap_pvs_product_result_maximal. bpd_gap_pvs_product_result_maximal + (bpd_candidate_pvs_product_result) = (e + f)))