odd_prime_lifting_the_exponent_value

Exact expanded first-order arithmetic statement

forall p x y d n a b X Y D. (~((p) = 1) /\ forall pvs_left_supplied_prime pvs_right_supplied_prime. (p) = pvs_left_supplied_prime * pvs_right_supplied_prime -> pvs_left_supplied_prime = 1 \/ pvs_right_supplied_prime = 1) -> (exists olte_gap_supplied_odd. olte_gap_supplied_odd + S (2) = (p)) -> (exists olte_gap_supplied_order. olte_gap_supplied_order + S (y) = (x)) -> ~(y = 0) -> ~(n = 0) -> x = y + d -> (exists olte_factor_supplied_divisor. (d) = (p) * olte_factor_supplied_divisor) -> ~(exists olte_factor_supplied_units. (x * y) = (p) * olte_factor_supplied_units) -> (((exists bpd_gap_pvs_supplied_difference_valuation_selected_bound. bpd_gap_pvs_supplied_difference_valuation_selected_bound + (a) = (d)) /\ (exists bpvi_result_pvs_supplied_difference_valuation_selected. ((exists bpvi_b_pvs_supplied_difference_valuation_selected_power bpvi_c_pvs_supplied_difference_valuation_selected_power. ((forall bpvi_i_pvs_supplied_difference_valuation_selected_power. (exists bpvi_repeat_gap_pvs_supplied_difference_valuation_selected_power. bpvi_repeat_gap_pvs_supplied_difference_valuation_selected_power + S bpvi_i_pvs_supplied_difference_valuation_selected_power = a) -> (((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_repeat. bpvi_h_pvs_supplied_difference_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_difference_valuation_selected_power)) * bpvi_c_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_repeat. bpvi_b_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_repeat * S ((S (bpvi_i_pvs_supplied_difference_valuation_selected_power)) * bpvi_c_pvs_supplied_difference_valuation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_difference_valuation_selected_power bpvi_v_pvs_supplied_difference_valuation_selected_power. ((((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_start. bpvi_h_pvs_supplied_difference_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_start. bpvi_u_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_start * S ((S (0)) * bpvi_v_pvs_supplied_difference_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_terminal. bpvi_h_pvs_supplied_difference_valuation_selected_power_terminal + S (bpvi_result_pvs_supplied_difference_valuation_selected) = S ((S (a)) * bpvi_v_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_terminal. bpvi_u_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_terminal * S ((S (a)) * bpvi_v_pvs_supplied_difference_valuation_selected_power) + (bpvi_result_pvs_supplied_difference_valuation_selected))) /\ forall bpvi_j_pvs_supplied_difference_valuation_selected_power. (exists bpvi_product_gap_pvs_supplied_difference_valuation_selected_power. bpvi_product_gap_pvs_supplied_difference_valuation_selected_power + S bpvi_j_pvs_supplied_difference_valuation_selected_power = a) -> exists bpvi_factor_pvs_supplied_difference_valuation_selected_power bpvi_partial_pvs_supplied_difference_valuation_selected_power bpvi_successor_pvs_supplied_difference_valuation_selected_power. ((((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_factor. bpvi_h_pvs_supplied_difference_valuation_selected_power_factor + S (bpvi_factor_pvs_supplied_difference_valuation_selected_power) = S ((S (bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_c_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_factor. bpvi_b_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_factor * S ((S (bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_c_pvs_supplied_difference_valuation_selected_power) + (bpvi_factor_pvs_supplied_difference_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_partial. bpvi_h_pvs_supplied_difference_valuation_selected_power_partial + S (bpvi_partial_pvs_supplied_difference_valuation_selected_power) = S ((S (bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_v_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_partial. bpvi_u_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_partial * S ((S (bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_v_pvs_supplied_difference_valuation_selected_power) + (bpvi_partial_pvs_supplied_difference_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_selected_power_successor. bpvi_h_pvs_supplied_difference_valuation_selected_power_successor + S (bpvi_successor_pvs_supplied_difference_valuation_selected_power) = S ((S (S bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_v_pvs_supplied_difference_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_selected_power_successor. bpvi_u_pvs_supplied_difference_valuation_selected_power = bpvi_q_pvs_supplied_difference_valuation_selected_power_successor * S ((S (S bpvi_j_pvs_supplied_difference_valuation_selected_power)) * bpvi_v_pvs_supplied_difference_valuation_selected_power) + (bpvi_successor_pvs_supplied_difference_valuation_selected_power))) /\ bpvi_successor_pvs_supplied_difference_valuation_selected_power = bpvi_partial_pvs_supplied_difference_valuation_selected_power * bpvi_factor_pvs_supplied_difference_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_difference_valuation_selected. d = bpvi_result_pvs_supplied_difference_valuation_selected * bpvi_divisor_factor_pvs_supplied_difference_valuation_selected))) /\ forall bpd_candidate_pvs_supplied_difference_valuation. (exists bpd_gap_pvs_supplied_difference_valuation_candidate_bound. bpd_gap_pvs_supplied_difference_valuation_candidate_bound + (bpd_candidate_pvs_supplied_difference_valuation) = (d)) -> (exists bpvi_result_pvs_supplied_difference_valuation_candidate. ((exists bpvi_b_pvs_supplied_difference_valuation_candidate_power bpvi_c_pvs_supplied_difference_valuation_candidate_power. ((forall bpvi_i_pvs_supplied_difference_valuation_candidate_power. (exists bpvi_repeat_gap_pvs_supplied_difference_valuation_candidate_power. bpvi_repeat_gap_pvs_supplied_difference_valuation_candidate_power + S bpvi_i_pvs_supplied_difference_valuation_candidate_power = bpd_candidate_pvs_supplied_difference_valuation) -> (((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_repeat. bpvi_h_pvs_supplied_difference_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_difference_valuation_candidate_power)) * bpvi_c_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_repeat. bpvi_b_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_repeat * S ((S (bpvi_i_pvs_supplied_difference_valuation_candidate_power)) * bpvi_c_pvs_supplied_difference_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_difference_valuation_candidate_power bpvi_v_pvs_supplied_difference_valuation_candidate_power. ((((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_start. bpvi_h_pvs_supplied_difference_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_start. bpvi_u_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_terminal. bpvi_h_pvs_supplied_difference_valuation_candidate_power_terminal + S (bpvi_result_pvs_supplied_difference_valuation_candidate) = S ((S (bpd_candidate_pvs_supplied_difference_valuation)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_terminal. bpvi_u_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_terminal * S ((S (bpd_candidate_pvs_supplied_difference_valuation)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power) + (bpvi_result_pvs_supplied_difference_valuation_candidate))) /\ forall bpvi_j_pvs_supplied_difference_valuation_candidate_power. (exists bpvi_product_gap_pvs_supplied_difference_valuation_candidate_power. bpvi_product_gap_pvs_supplied_difference_valuation_candidate_power + S bpvi_j_pvs_supplied_difference_valuation_candidate_power = bpd_candidate_pvs_supplied_difference_valuation) -> exists bpvi_factor_pvs_supplied_difference_valuation_candidate_power bpvi_partial_pvs_supplied_difference_valuation_candidate_power bpvi_successor_pvs_supplied_difference_valuation_candidate_power. ((((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_factor. bpvi_h_pvs_supplied_difference_valuation_candidate_power_factor + S (bpvi_factor_pvs_supplied_difference_valuation_candidate_power) = S ((S (bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_c_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_factor. bpvi_b_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_factor * S ((S (bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_c_pvs_supplied_difference_valuation_candidate_power) + (bpvi_factor_pvs_supplied_difference_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_partial. bpvi_h_pvs_supplied_difference_valuation_candidate_power_partial + S (bpvi_partial_pvs_supplied_difference_valuation_candidate_power) = S ((S (bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_partial. bpvi_u_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_partial * S ((S (bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power) + (bpvi_partial_pvs_supplied_difference_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_difference_valuation_candidate_power_successor. bpvi_h_pvs_supplied_difference_valuation_candidate_power_successor + S (bpvi_successor_pvs_supplied_difference_valuation_candidate_power) = S ((S (S bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_difference_valuation_candidate_power_successor. bpvi_u_pvs_supplied_difference_valuation_candidate_power = bpvi_q_pvs_supplied_difference_valuation_candidate_power_successor * S ((S (S bpvi_j_pvs_supplied_difference_valuation_candidate_power)) * bpvi_v_pvs_supplied_difference_valuation_candidate_power) + (bpvi_successor_pvs_supplied_difference_valuation_candidate_power))) /\ bpvi_successor_pvs_supplied_difference_valuation_candidate_power = bpvi_partial_pvs_supplied_difference_valuation_candidate_power * bpvi_factor_pvs_supplied_difference_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_difference_valuation_candidate. d = bpvi_result_pvs_supplied_difference_valuation_candidate * bpvi_divisor_factor_pvs_supplied_difference_valuation_candidate)) -> (exists bpd_gap_pvs_supplied_difference_valuation_maximal. bpd_gap_pvs_supplied_difference_valuation_maximal + (bpd_candidate_pvs_supplied_difference_valuation) = (a))) -> (((exists bpd_gap_pvs_supplied_exponent_valuation_selected_bound. bpd_gap_pvs_supplied_exponent_valuation_selected_bound + (b) = (n)) /\ (exists bpvi_result_pvs_supplied_exponent_valuation_selected. ((exists bpvi_b_pvs_supplied_exponent_valuation_selected_power bpvi_c_pvs_supplied_exponent_valuation_selected_power. ((forall bpvi_i_pvs_supplied_exponent_valuation_selected_power. (exists bpvi_repeat_gap_pvs_supplied_exponent_valuation_selected_power. bpvi_repeat_gap_pvs_supplied_exponent_valuation_selected_power + S bpvi_i_pvs_supplied_exponent_valuation_selected_power = b) -> (((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_repeat. bpvi_h_pvs_supplied_exponent_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_exponent_valuation_selected_power)) * bpvi_c_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_repeat. bpvi_b_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_repeat * S ((S (bpvi_i_pvs_supplied_exponent_valuation_selected_power)) * bpvi_c_pvs_supplied_exponent_valuation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_exponent_valuation_selected_power bpvi_v_pvs_supplied_exponent_valuation_selected_power. ((((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_start. bpvi_h_pvs_supplied_exponent_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_start. bpvi_u_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_start * S ((S (0)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_terminal. bpvi_h_pvs_supplied_exponent_valuation_selected_power_terminal + S (bpvi_result_pvs_supplied_exponent_valuation_selected) = S ((S (b)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_terminal. bpvi_u_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_terminal * S ((S (b)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power) + (bpvi_result_pvs_supplied_exponent_valuation_selected))) /\ forall bpvi_j_pvs_supplied_exponent_valuation_selected_power. (exists bpvi_product_gap_pvs_supplied_exponent_valuation_selected_power. bpvi_product_gap_pvs_supplied_exponent_valuation_selected_power + S bpvi_j_pvs_supplied_exponent_valuation_selected_power = b) -> exists bpvi_factor_pvs_supplied_exponent_valuation_selected_power bpvi_partial_pvs_supplied_exponent_valuation_selected_power bpvi_successor_pvs_supplied_exponent_valuation_selected_power. ((((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_factor. bpvi_h_pvs_supplied_exponent_valuation_selected_power_factor + S (bpvi_factor_pvs_supplied_exponent_valuation_selected_power) = S ((S (bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_c_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_factor. bpvi_b_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_factor * S ((S (bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_c_pvs_supplied_exponent_valuation_selected_power) + (bpvi_factor_pvs_supplied_exponent_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_partial. bpvi_h_pvs_supplied_exponent_valuation_selected_power_partial + S (bpvi_partial_pvs_supplied_exponent_valuation_selected_power) = S ((S (bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_partial. bpvi_u_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_partial * S ((S (bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power) + (bpvi_partial_pvs_supplied_exponent_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_selected_power_successor. bpvi_h_pvs_supplied_exponent_valuation_selected_power_successor + S (bpvi_successor_pvs_supplied_exponent_valuation_selected_power) = S ((S (S bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_selected_power_successor. bpvi_u_pvs_supplied_exponent_valuation_selected_power = bpvi_q_pvs_supplied_exponent_valuation_selected_power_successor * S ((S (S bpvi_j_pvs_supplied_exponent_valuation_selected_power)) * bpvi_v_pvs_supplied_exponent_valuation_selected_power) + (bpvi_successor_pvs_supplied_exponent_valuation_selected_power))) /\ bpvi_successor_pvs_supplied_exponent_valuation_selected_power = bpvi_partial_pvs_supplied_exponent_valuation_selected_power * bpvi_factor_pvs_supplied_exponent_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_exponent_valuation_selected. n = bpvi_result_pvs_supplied_exponent_valuation_selected * bpvi_divisor_factor_pvs_supplied_exponent_valuation_selected))) /\ forall bpd_candidate_pvs_supplied_exponent_valuation. (exists bpd_gap_pvs_supplied_exponent_valuation_candidate_bound. bpd_gap_pvs_supplied_exponent_valuation_candidate_bound + (bpd_candidate_pvs_supplied_exponent_valuation) = (n)) -> (exists bpvi_result_pvs_supplied_exponent_valuation_candidate. ((exists bpvi_b_pvs_supplied_exponent_valuation_candidate_power bpvi_c_pvs_supplied_exponent_valuation_candidate_power. ((forall bpvi_i_pvs_supplied_exponent_valuation_candidate_power. (exists bpvi_repeat_gap_pvs_supplied_exponent_valuation_candidate_power. bpvi_repeat_gap_pvs_supplied_exponent_valuation_candidate_power + S bpvi_i_pvs_supplied_exponent_valuation_candidate_power = bpd_candidate_pvs_supplied_exponent_valuation) -> (((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_repeat. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_c_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_repeat. bpvi_b_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_repeat * S ((S (bpvi_i_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_c_pvs_supplied_exponent_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_exponent_valuation_candidate_power bpvi_v_pvs_supplied_exponent_valuation_candidate_power. ((((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_start. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_start. bpvi_u_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_terminal. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_terminal + S (bpvi_result_pvs_supplied_exponent_valuation_candidate) = S ((S (bpd_candidate_pvs_supplied_exponent_valuation)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_terminal. bpvi_u_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_terminal * S ((S (bpd_candidate_pvs_supplied_exponent_valuation)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power) + (bpvi_result_pvs_supplied_exponent_valuation_candidate))) /\ forall bpvi_j_pvs_supplied_exponent_valuation_candidate_power. (exists bpvi_product_gap_pvs_supplied_exponent_valuation_candidate_power. bpvi_product_gap_pvs_supplied_exponent_valuation_candidate_power + S bpvi_j_pvs_supplied_exponent_valuation_candidate_power = bpd_candidate_pvs_supplied_exponent_valuation) -> exists bpvi_factor_pvs_supplied_exponent_valuation_candidate_power bpvi_partial_pvs_supplied_exponent_valuation_candidate_power bpvi_successor_pvs_supplied_exponent_valuation_candidate_power. ((((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_factor. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_factor + S (bpvi_factor_pvs_supplied_exponent_valuation_candidate_power) = S ((S (bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_c_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_factor. bpvi_b_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_factor * S ((S (bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_c_pvs_supplied_exponent_valuation_candidate_power) + (bpvi_factor_pvs_supplied_exponent_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_partial. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_partial + S (bpvi_partial_pvs_supplied_exponent_valuation_candidate_power) = S ((S (bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_partial. bpvi_u_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_partial * S ((S (bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power) + (bpvi_partial_pvs_supplied_exponent_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_exponent_valuation_candidate_power_successor. bpvi_h_pvs_supplied_exponent_valuation_candidate_power_successor + S (bpvi_successor_pvs_supplied_exponent_valuation_candidate_power) = S ((S (S bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power)) /\ exists bpvi_q_pvs_supplied_exponent_valuation_candidate_power_successor. bpvi_u_pvs_supplied_exponent_valuation_candidate_power = bpvi_q_pvs_supplied_exponent_valuation_candidate_power_successor * S ((S (S bpvi_j_pvs_supplied_exponent_valuation_candidate_power)) * bpvi_v_pvs_supplied_exponent_valuation_candidate_power) + (bpvi_successor_pvs_supplied_exponent_valuation_candidate_power))) /\ bpvi_successor_pvs_supplied_exponent_valuation_candidate_power = bpvi_partial_pvs_supplied_exponent_valuation_candidate_power * bpvi_factor_pvs_supplied_exponent_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_exponent_valuation_candidate. n = bpvi_result_pvs_supplied_exponent_valuation_candidate * bpvi_divisor_factor_pvs_supplied_exponent_valuation_candidate)) -> (exists bpd_gap_pvs_supplied_exponent_valuation_maximal. bpd_gap_pvs_supplied_exponent_valuation_maximal + (bpd_candidate_pvs_supplied_exponent_valuation) = (b))) -> (exists pa_b_olte_supplied_X pa_c_olte_supplied_X. ((forall pa_i_olte_supplied_X_repeat. (exists pa_lt_olte_supplied_X_repeat_bound. pa_lt_olte_supplied_X_repeat_bound + S pa_i_olte_supplied_X_repeat = n) -> (((exists pa_h_olte_supplied_X_repeat_decoded. pa_h_olte_supplied_X_repeat_decoded + S (x) = S ((S (pa_i_olte_supplied_X_repeat)) * pa_c_olte_supplied_X)) /\ exists pa_q_olte_supplied_X_repeat_decoded. pa_b_olte_supplied_X = pa_q_olte_supplied_X_repeat_decoded * S ((S (pa_i_olte_supplied_X_repeat)) * pa_c_olte_supplied_X) + (x)))) /\ (exists pa_u_olte_supplied_X_product pa_v_olte_supplied_X_product. ((((exists pa_h_olte_supplied_X_product_start. pa_h_olte_supplied_X_product_start + S (1) = S ((S (0)) * pa_v_olte_supplied_X_product)) /\ exists pa_q_olte_supplied_X_product_start. pa_u_olte_supplied_X_product = pa_q_olte_supplied_X_product_start * S ((S (0)) * pa_v_olte_supplied_X_product) + (1))) /\ ((((exists pa_h_olte_supplied_X_product_terminal. pa_h_olte_supplied_X_product_terminal + S (X) = S ((S (n)) * pa_v_olte_supplied_X_product)) /\ exists pa_q_olte_supplied_X_product_terminal. pa_u_olte_supplied_X_product = pa_q_olte_supplied_X_product_terminal * S ((S (n)) * pa_v_olte_supplied_X_product) + (X))) /\ forall pa_i_olte_supplied_X_product. (exists pa_lt_olte_supplied_X_product_bound. pa_lt_olte_supplied_X_product_bound + S pa_i_olte_supplied_X_product = n) -> exists pa_p_olte_supplied_X_product pa_r_olte_supplied_X_product pa_s_olte_supplied_X_product. ((((exists pa_h_olte_supplied_X_product_factor. pa_h_olte_supplied_X_product_factor + S (pa_p_olte_supplied_X_product) = S ((S (pa_i_olte_supplied_X_product)) * pa_c_olte_supplied_X)) /\ exists pa_q_olte_supplied_X_product_factor. pa_b_olte_supplied_X = pa_q_olte_supplied_X_product_factor * S ((S (pa_i_olte_supplied_X_product)) * pa_c_olte_supplied_X) + (pa_p_olte_supplied_X_product))) /\ ((((exists pa_h_olte_supplied_X_product_partial. pa_h_olte_supplied_X_product_partial + S (pa_r_olte_supplied_X_product) = S ((S (pa_i_olte_supplied_X_product)) * pa_v_olte_supplied_X_product)) /\ exists pa_q_olte_supplied_X_product_partial. pa_u_olte_supplied_X_product = pa_q_olte_supplied_X_product_partial * S ((S (pa_i_olte_supplied_X_product)) * pa_v_olte_supplied_X_product) + (pa_r_olte_supplied_X_product))) /\ ((((exists pa_h_olte_supplied_X_product_successor. pa_h_olte_supplied_X_product_successor + S (pa_s_olte_supplied_X_product) = S ((S (S pa_i_olte_supplied_X_product)) * pa_v_olte_supplied_X_product)) /\ exists pa_q_olte_supplied_X_product_successor. pa_u_olte_supplied_X_product = pa_q_olte_supplied_X_product_successor * S ((S (S pa_i_olte_supplied_X_product)) * pa_v_olte_supplied_X_product) + (pa_s_olte_supplied_X_product))) /\ pa_s_olte_supplied_X_product = pa_r_olte_supplied_X_product * pa_p_olte_supplied_X_product)))))))) -> (exists pa_b_olte_supplied_Y pa_c_olte_supplied_Y. ((forall pa_i_olte_supplied_Y_repeat. (exists pa_lt_olte_supplied_Y_repeat_bound. pa_lt_olte_supplied_Y_repeat_bound + S pa_i_olte_supplied_Y_repeat = n) -> (((exists pa_h_olte_supplied_Y_repeat_decoded. pa_h_olte_supplied_Y_repeat_decoded + S (y) = S ((S (pa_i_olte_supplied_Y_repeat)) * pa_c_olte_supplied_Y)) /\ exists pa_q_olte_supplied_Y_repeat_decoded. pa_b_olte_supplied_Y = pa_q_olte_supplied_Y_repeat_decoded * S ((S (pa_i_olte_supplied_Y_repeat)) * pa_c_olte_supplied_Y) + (y)))) /\ (exists pa_u_olte_supplied_Y_product pa_v_olte_supplied_Y_product. ((((exists pa_h_olte_supplied_Y_product_start. pa_h_olte_supplied_Y_product_start + S (1) = S ((S (0)) * pa_v_olte_supplied_Y_product)) /\ exists pa_q_olte_supplied_Y_product_start. pa_u_olte_supplied_Y_product = pa_q_olte_supplied_Y_product_start * S ((S (0)) * pa_v_olte_supplied_Y_product) + (1))) /\ ((((exists pa_h_olte_supplied_Y_product_terminal. pa_h_olte_supplied_Y_product_terminal + S (Y) = S ((S (n)) * pa_v_olte_supplied_Y_product)) /\ exists pa_q_olte_supplied_Y_product_terminal. pa_u_olte_supplied_Y_product = pa_q_olte_supplied_Y_product_terminal * S ((S (n)) * pa_v_olte_supplied_Y_product) + (Y))) /\ forall pa_i_olte_supplied_Y_product. (exists pa_lt_olte_supplied_Y_product_bound. pa_lt_olte_supplied_Y_product_bound + S pa_i_olte_supplied_Y_product = n) -> exists pa_p_olte_supplied_Y_product pa_r_olte_supplied_Y_product pa_s_olte_supplied_Y_product. ((((exists pa_h_olte_supplied_Y_product_factor. pa_h_olte_supplied_Y_product_factor + S (pa_p_olte_supplied_Y_product) = S ((S (pa_i_olte_supplied_Y_product)) * pa_c_olte_supplied_Y)) /\ exists pa_q_olte_supplied_Y_product_factor. pa_b_olte_supplied_Y = pa_q_olte_supplied_Y_product_factor * S ((S (pa_i_olte_supplied_Y_product)) * pa_c_olte_supplied_Y) + (pa_p_olte_supplied_Y_product))) /\ ((((exists pa_h_olte_supplied_Y_product_partial. pa_h_olte_supplied_Y_product_partial + S (pa_r_olte_supplied_Y_product) = S ((S (pa_i_olte_supplied_Y_product)) * pa_v_olte_supplied_Y_product)) /\ exists pa_q_olte_supplied_Y_product_partial. pa_u_olte_supplied_Y_product = pa_q_olte_supplied_Y_product_partial * S ((S (pa_i_olte_supplied_Y_product)) * pa_v_olte_supplied_Y_product) + (pa_r_olte_supplied_Y_product))) /\ ((((exists pa_h_olte_supplied_Y_product_successor. pa_h_olte_supplied_Y_product_successor + S (pa_s_olte_supplied_Y_product) = S ((S (S pa_i_olte_supplied_Y_product)) * pa_v_olte_supplied_Y_product)) /\ exists pa_q_olte_supplied_Y_product_successor. pa_u_olte_supplied_Y_product = pa_q_olte_supplied_Y_product_successor * S ((S (S pa_i_olte_supplied_Y_product)) * pa_v_olte_supplied_Y_product) + (pa_s_olte_supplied_Y_product))) /\ pa_s_olte_supplied_Y_product = pa_r_olte_supplied_Y_product * pa_p_olte_supplied_Y_product)))))))) -> X = Y + D -> (((exists bpd_gap_pvs_supplied_result_selected_bound. bpd_gap_pvs_supplied_result_selected_bound + (a + b) = (D)) /\ (exists bpvi_result_pvs_supplied_result_selected. ((exists bpvi_b_pvs_supplied_result_selected_power bpvi_c_pvs_supplied_result_selected_power. ((forall bpvi_i_pvs_supplied_result_selected_power. (exists bpvi_repeat_gap_pvs_supplied_result_selected_power. bpvi_repeat_gap_pvs_supplied_result_selected_power + S bpvi_i_pvs_supplied_result_selected_power = a + b) -> (((exists bpvi_h_pvs_supplied_result_selected_power_repeat. bpvi_h_pvs_supplied_result_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_result_selected_power)) * bpvi_c_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_repeat. bpvi_b_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_repeat * S ((S (bpvi_i_pvs_supplied_result_selected_power)) * bpvi_c_pvs_supplied_result_selected_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_result_selected_power bpvi_v_pvs_supplied_result_selected_power. ((((exists bpvi_h_pvs_supplied_result_selected_power_start. bpvi_h_pvs_supplied_result_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_start. bpvi_u_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_start * S ((S (0)) * bpvi_v_pvs_supplied_result_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_result_selected_power_terminal. bpvi_h_pvs_supplied_result_selected_power_terminal + S (bpvi_result_pvs_supplied_result_selected) = S ((S (a + b)) * bpvi_v_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_terminal. bpvi_u_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_terminal * S ((S (a + b)) * bpvi_v_pvs_supplied_result_selected_power) + (bpvi_result_pvs_supplied_result_selected))) /\ forall bpvi_j_pvs_supplied_result_selected_power. (exists bpvi_product_gap_pvs_supplied_result_selected_power. bpvi_product_gap_pvs_supplied_result_selected_power + S bpvi_j_pvs_supplied_result_selected_power = a + b) -> exists bpvi_factor_pvs_supplied_result_selected_power bpvi_partial_pvs_supplied_result_selected_power bpvi_successor_pvs_supplied_result_selected_power. ((((exists bpvi_h_pvs_supplied_result_selected_power_factor. bpvi_h_pvs_supplied_result_selected_power_factor + S (bpvi_factor_pvs_supplied_result_selected_power) = S ((S (bpvi_j_pvs_supplied_result_selected_power)) * bpvi_c_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_factor. bpvi_b_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_factor * S ((S (bpvi_j_pvs_supplied_result_selected_power)) * bpvi_c_pvs_supplied_result_selected_power) + (bpvi_factor_pvs_supplied_result_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_result_selected_power_partial. bpvi_h_pvs_supplied_result_selected_power_partial + S (bpvi_partial_pvs_supplied_result_selected_power) = S ((S (bpvi_j_pvs_supplied_result_selected_power)) * bpvi_v_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_partial. bpvi_u_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_partial * S ((S (bpvi_j_pvs_supplied_result_selected_power)) * bpvi_v_pvs_supplied_result_selected_power) + (bpvi_partial_pvs_supplied_result_selected_power))) /\ ((((exists bpvi_h_pvs_supplied_result_selected_power_successor. bpvi_h_pvs_supplied_result_selected_power_successor + S (bpvi_successor_pvs_supplied_result_selected_power) = S ((S (S bpvi_j_pvs_supplied_result_selected_power)) * bpvi_v_pvs_supplied_result_selected_power)) /\ exists bpvi_q_pvs_supplied_result_selected_power_successor. bpvi_u_pvs_supplied_result_selected_power = bpvi_q_pvs_supplied_result_selected_power_successor * S ((S (S bpvi_j_pvs_supplied_result_selected_power)) * bpvi_v_pvs_supplied_result_selected_power) + (bpvi_successor_pvs_supplied_result_selected_power))) /\ bpvi_successor_pvs_supplied_result_selected_power = bpvi_partial_pvs_supplied_result_selected_power * bpvi_factor_pvs_supplied_result_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_result_selected. D = bpvi_result_pvs_supplied_result_selected * bpvi_divisor_factor_pvs_supplied_result_selected))) /\ forall bpd_candidate_pvs_supplied_result. (exists bpd_gap_pvs_supplied_result_candidate_bound. bpd_gap_pvs_supplied_result_candidate_bound + (bpd_candidate_pvs_supplied_result) = (D)) -> (exists bpvi_result_pvs_supplied_result_candidate. ((exists bpvi_b_pvs_supplied_result_candidate_power bpvi_c_pvs_supplied_result_candidate_power. ((forall bpvi_i_pvs_supplied_result_candidate_power. (exists bpvi_repeat_gap_pvs_supplied_result_candidate_power. bpvi_repeat_gap_pvs_supplied_result_candidate_power + S bpvi_i_pvs_supplied_result_candidate_power = bpd_candidate_pvs_supplied_result) -> (((exists bpvi_h_pvs_supplied_result_candidate_power_repeat. bpvi_h_pvs_supplied_result_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_supplied_result_candidate_power)) * bpvi_c_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_repeat. bpvi_b_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_repeat * S ((S (bpvi_i_pvs_supplied_result_candidate_power)) * bpvi_c_pvs_supplied_result_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_supplied_result_candidate_power bpvi_v_pvs_supplied_result_candidate_power. ((((exists bpvi_h_pvs_supplied_result_candidate_power_start. bpvi_h_pvs_supplied_result_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_start. bpvi_u_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_start * S ((S (0)) * bpvi_v_pvs_supplied_result_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_supplied_result_candidate_power_terminal. bpvi_h_pvs_supplied_result_candidate_power_terminal + S (bpvi_result_pvs_supplied_result_candidate) = S ((S (bpd_candidate_pvs_supplied_result)) * bpvi_v_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_terminal. bpvi_u_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_terminal * S ((S (bpd_candidate_pvs_supplied_result)) * bpvi_v_pvs_supplied_result_candidate_power) + (bpvi_result_pvs_supplied_result_candidate))) /\ forall bpvi_j_pvs_supplied_result_candidate_power. (exists bpvi_product_gap_pvs_supplied_result_candidate_power. bpvi_product_gap_pvs_supplied_result_candidate_power + S bpvi_j_pvs_supplied_result_candidate_power = bpd_candidate_pvs_supplied_result) -> exists bpvi_factor_pvs_supplied_result_candidate_power bpvi_partial_pvs_supplied_result_candidate_power bpvi_successor_pvs_supplied_result_candidate_power. ((((exists bpvi_h_pvs_supplied_result_candidate_power_factor. bpvi_h_pvs_supplied_result_candidate_power_factor + S (bpvi_factor_pvs_supplied_result_candidate_power) = S ((S (bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_c_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_factor. bpvi_b_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_factor * S ((S (bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_c_pvs_supplied_result_candidate_power) + (bpvi_factor_pvs_supplied_result_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_result_candidate_power_partial. bpvi_h_pvs_supplied_result_candidate_power_partial + S (bpvi_partial_pvs_supplied_result_candidate_power) = S ((S (bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_v_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_partial. bpvi_u_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_partial * S ((S (bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_v_pvs_supplied_result_candidate_power) + (bpvi_partial_pvs_supplied_result_candidate_power))) /\ ((((exists bpvi_h_pvs_supplied_result_candidate_power_successor. bpvi_h_pvs_supplied_result_candidate_power_successor + S (bpvi_successor_pvs_supplied_result_candidate_power) = S ((S (S bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_v_pvs_supplied_result_candidate_power)) /\ exists bpvi_q_pvs_supplied_result_candidate_power_successor. bpvi_u_pvs_supplied_result_candidate_power = bpvi_q_pvs_supplied_result_candidate_power_successor * S ((S (S bpvi_j_pvs_supplied_result_candidate_power)) * bpvi_v_pvs_supplied_result_candidate_power) + (bpvi_successor_pvs_supplied_result_candidate_power))) /\ bpvi_successor_pvs_supplied_result_candidate_power = bpvi_partial_pvs_supplied_result_candidate_power * bpvi_factor_pvs_supplied_result_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_supplied_result_candidate. D = bpvi_result_pvs_supplied_result_candidate * bpvi_divisor_factor_pvs_supplied_result_candidate)) -> (exists bpd_gap_pvs_supplied_result_maximal. bpd_gap_pvs_supplied_result_maximal + (bpd_candidate_pvs_supplied_result) = (a + b)))