prime_exponent_entry_has_prime_valuation

Exact expanded first-order arithmetic statement

forall n pb pc eb ec vb vc l i e. (forall pvs_index_decoded_exponents. (exists pvs_gap_decoded_exponentsindex. pvs_gap_decoded_exponentsindex + S (pvs_index_decoded_exponents) = (l)) -> exists pvs_prime_decoded_exponents pvs_exponent_decoded_exponents pvs_power_decoded_exponents. (((((exists ff_h_pvs_decoded_exponentsprime. ff_h_pvs_decoded_exponentsprime + S (pvs_prime_decoded_exponents) = S ((S (pvs_index_decoded_exponents)) * pc)) /\ exists ff_q_pvs_decoded_exponentsprime. pb = ff_q_pvs_decoded_exponentsprime * S ((S (pvs_index_decoded_exponents)) * pc) + (pvs_prime_decoded_exponents))) /\ (((((exists ff_h_pvs_decoded_exponentsexponent. ff_h_pvs_decoded_exponentsexponent + S (pvs_exponent_decoded_exponents) = S ((S (pvs_index_decoded_exponents)) * ec)) /\ exists ff_q_pvs_decoded_exponentsexponent. eb = ff_q_pvs_decoded_exponentsexponent * S ((S (pvs_index_decoded_exponents)) * ec) + (pvs_exponent_decoded_exponents))) /\ (((((exists ff_h_pvs_decoded_exponentspower. ff_h_pvs_decoded_exponentspower + S (pvs_power_decoded_exponents) = S ((S (pvs_index_decoded_exponents)) * vc)) /\ exists ff_q_pvs_decoded_exponentspower. vb = ff_q_pvs_decoded_exponentspower * S ((S (pvs_index_decoded_exponents)) * vc) + (pvs_power_decoded_exponents))) /\ (((~((pvs_prime_decoded_exponents) = 1) /\ forall pvs_left_decoded_exponentsdomain pvs_right_decoded_exponentsdomain. (pvs_prime_decoded_exponents) = pvs_left_decoded_exponentsdomain * pvs_right_decoded_exponentsdomain -> pvs_left_decoded_exponentsdomain = 1 \/ pvs_right_decoded_exponentsdomain = 1) /\ (((~(pvs_exponent_decoded_exponents = 0)) /\ (((((exists bpd_gap_pvs_decoded_exponentsvaluation_selected_bound. bpd_gap_pvs_decoded_exponentsvaluation_selected_bound + (pvs_exponent_decoded_exponents) = (n)) /\ (exists bpvi_result_pvs_decoded_exponentsvaluation_selected. ((exists bpvi_b_pvs_decoded_exponentsvaluation_selected_power bpvi_c_pvs_decoded_exponentsvaluation_selected_power. ((forall bpvi_i_pvs_decoded_exponentsvaluation_selected_power. (exists bpvi_repeat_gap_pvs_decoded_exponentsvaluation_selected_power. bpvi_repeat_gap_pvs_decoded_exponentsvaluation_selected_power + S bpvi_i_pvs_decoded_exponentsvaluation_selected_power = pvs_exponent_decoded_exponents) -> (((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_repeat. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_repeat + S (pvs_prime_decoded_exponents) = S ((S (bpvi_i_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_c_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_repeat. bpvi_b_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_c_pvs_decoded_exponentsvaluation_selected_power) + (pvs_prime_decoded_exponents)))) /\ (exists bpvi_u_pvs_decoded_exponentsvaluation_selected_power bpvi_v_pvs_decoded_exponentsvaluation_selected_power. ((((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_start. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_start. bpvi_u_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_terminal. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_terminal + S (bpvi_result_pvs_decoded_exponentsvaluation_selected) = S ((S (pvs_exponent_decoded_exponents)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_terminal. bpvi_u_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_terminal * S ((S (pvs_exponent_decoded_exponents)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power) + (bpvi_result_pvs_decoded_exponentsvaluation_selected))) /\ forall bpvi_j_pvs_decoded_exponentsvaluation_selected_power. (exists bpvi_product_gap_pvs_decoded_exponentsvaluation_selected_power. bpvi_product_gap_pvs_decoded_exponentsvaluation_selected_power + S bpvi_j_pvs_decoded_exponentsvaluation_selected_power = pvs_exponent_decoded_exponents) -> exists bpvi_factor_pvs_decoded_exponentsvaluation_selected_power bpvi_partial_pvs_decoded_exponentsvaluation_selected_power bpvi_successor_pvs_decoded_exponentsvaluation_selected_power. ((((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_factor. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_factor + S (bpvi_factor_pvs_decoded_exponentsvaluation_selected_power) = S ((S (bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_c_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_factor. bpvi_b_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_factor * S ((S (bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_c_pvs_decoded_exponentsvaluation_selected_power) + (bpvi_factor_pvs_decoded_exponentsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_partial. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_partial + S (bpvi_partial_pvs_decoded_exponentsvaluation_selected_power) = S ((S (bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_partial. bpvi_u_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_partial * S ((S (bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power) + (bpvi_partial_pvs_decoded_exponentsvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_selected_power_successor. bpvi_h_pvs_decoded_exponentsvaluation_selected_power_successor + S (bpvi_successor_pvs_decoded_exponentsvaluation_selected_power) = S ((S (S bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_selected_power_successor. bpvi_u_pvs_decoded_exponentsvaluation_selected_power = bpvi_q_pvs_decoded_exponentsvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_decoded_exponentsvaluation_selected_power)) * bpvi_v_pvs_decoded_exponentsvaluation_selected_power) + (bpvi_successor_pvs_decoded_exponentsvaluation_selected_power))) /\ bpvi_successor_pvs_decoded_exponentsvaluation_selected_power = bpvi_partial_pvs_decoded_exponentsvaluation_selected_power * bpvi_factor_pvs_decoded_exponentsvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_decoded_exponentsvaluation_selected. n = bpvi_result_pvs_decoded_exponentsvaluation_selected * bpvi_divisor_factor_pvs_decoded_exponentsvaluation_selected))) /\ forall bpd_candidate_pvs_decoded_exponentsvaluation. (exists bpd_gap_pvs_decoded_exponentsvaluation_candidate_bound. bpd_gap_pvs_decoded_exponentsvaluation_candidate_bound + (bpd_candidate_pvs_decoded_exponentsvaluation) = (n)) -> (exists bpvi_result_pvs_decoded_exponentsvaluation_candidate. ((exists bpvi_b_pvs_decoded_exponentsvaluation_candidate_power bpvi_c_pvs_decoded_exponentsvaluation_candidate_power. ((forall bpvi_i_pvs_decoded_exponentsvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_decoded_exponentsvaluation_candidate_power. bpvi_repeat_gap_pvs_decoded_exponentsvaluation_candidate_power + S bpvi_i_pvs_decoded_exponentsvaluation_candidate_power = bpd_candidate_pvs_decoded_exponentsvaluation) -> (((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_repeat. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_repeat + S (pvs_prime_decoded_exponents) = S ((S (bpvi_i_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_c_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_repeat. bpvi_b_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_c_pvs_decoded_exponentsvaluation_candidate_power) + (pvs_prime_decoded_exponents)))) /\ (exists bpvi_u_pvs_decoded_exponentsvaluation_candidate_power bpvi_v_pvs_decoded_exponentsvaluation_candidate_power. ((((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_start. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_start. bpvi_u_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_terminal. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_terminal + S (bpvi_result_pvs_decoded_exponentsvaluation_candidate) = S ((S (bpd_candidate_pvs_decoded_exponentsvaluation)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_terminal. bpvi_u_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_decoded_exponentsvaluation)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power) + (bpvi_result_pvs_decoded_exponentsvaluation_candidate))) /\ forall bpvi_j_pvs_decoded_exponentsvaluation_candidate_power. (exists bpvi_product_gap_pvs_decoded_exponentsvaluation_candidate_power. bpvi_product_gap_pvs_decoded_exponentsvaluation_candidate_power + S bpvi_j_pvs_decoded_exponentsvaluation_candidate_power = bpd_candidate_pvs_decoded_exponentsvaluation) -> exists bpvi_factor_pvs_decoded_exponentsvaluation_candidate_power bpvi_partial_pvs_decoded_exponentsvaluation_candidate_power bpvi_successor_pvs_decoded_exponentsvaluation_candidate_power. ((((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_factor. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_factor + S (bpvi_factor_pvs_decoded_exponentsvaluation_candidate_power) = S ((S (bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_c_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_factor. bpvi_b_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_c_pvs_decoded_exponentsvaluation_candidate_power) + (bpvi_factor_pvs_decoded_exponentsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_partial. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_partial + S (bpvi_partial_pvs_decoded_exponentsvaluation_candidate_power) = S ((S (bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_partial. bpvi_u_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power) + (bpvi_partial_pvs_decoded_exponentsvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_successor. bpvi_h_pvs_decoded_exponentsvaluation_candidate_power_successor + S (bpvi_successor_pvs_decoded_exponentsvaluation_candidate_power) = S ((S (S bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power)) /\ exists bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_successor. bpvi_u_pvs_decoded_exponentsvaluation_candidate_power = bpvi_q_pvs_decoded_exponentsvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_decoded_exponentsvaluation_candidate_power)) * bpvi_v_pvs_decoded_exponentsvaluation_candidate_power) + (bpvi_successor_pvs_decoded_exponentsvaluation_candidate_power))) /\ bpvi_successor_pvs_decoded_exponentsvaluation_candidate_power = bpvi_partial_pvs_decoded_exponentsvaluation_candidate_power * bpvi_factor_pvs_decoded_exponentsvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_decoded_exponentsvaluation_candidate. n = bpvi_result_pvs_decoded_exponentsvaluation_candidate * bpvi_divisor_factor_pvs_decoded_exponentsvaluation_candidate)) -> (exists bpd_gap_pvs_decoded_exponentsvaluation_maximal. bpd_gap_pvs_decoded_exponentsvaluation_maximal + (bpd_candidate_pvs_decoded_exponentsvaluation) = (pvs_exponent_decoded_exponents))) /\ (exists pa_b_pvs_decoded_exponentsvalue pa_c_pvs_decoded_exponentsvalue. ((forall pa_i_pvs_decoded_exponentsvalue_repeat. (exists pa_lt_pvs_decoded_exponentsvalue_repeat_bound. pa_lt_pvs_decoded_exponentsvalue_repeat_bound + S pa_i_pvs_decoded_exponentsvalue_repeat = pvs_exponent_decoded_exponents) -> (((exists pa_h_pvs_decoded_exponentsvalue_repeat_decoded. pa_h_pvs_decoded_exponentsvalue_repeat_decoded + S (pvs_prime_decoded_exponents) = S ((S (pa_i_pvs_decoded_exponentsvalue_repeat)) * pa_c_pvs_decoded_exponentsvalue)) /\ exists pa_q_pvs_decoded_exponentsvalue_repeat_decoded. pa_b_pvs_decoded_exponentsvalue = pa_q_pvs_decoded_exponentsvalue_repeat_decoded * S ((S (pa_i_pvs_decoded_exponentsvalue_repeat)) * pa_c_pvs_decoded_exponentsvalue) + (pvs_prime_decoded_exponents)))) /\ (exists pa_u_pvs_decoded_exponentsvalue_product pa_v_pvs_decoded_exponentsvalue_product. ((((exists pa_h_pvs_decoded_exponentsvalue_product_start. pa_h_pvs_decoded_exponentsvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_decoded_exponentsvalue_product)) /\ exists pa_q_pvs_decoded_exponentsvalue_product_start. pa_u_pvs_decoded_exponentsvalue_product = pa_q_pvs_decoded_exponentsvalue_product_start * S ((S (0)) * pa_v_pvs_decoded_exponentsvalue_product) + (1))) /\ ((((exists pa_h_pvs_decoded_exponentsvalue_product_terminal. pa_h_pvs_decoded_exponentsvalue_product_terminal + S (pvs_power_decoded_exponents) = S ((S (pvs_exponent_decoded_exponents)) * pa_v_pvs_decoded_exponentsvalue_product)) /\ exists pa_q_pvs_decoded_exponentsvalue_product_terminal. pa_u_pvs_decoded_exponentsvalue_product = pa_q_pvs_decoded_exponentsvalue_product_terminal * S ((S (pvs_exponent_decoded_exponents)) * pa_v_pvs_decoded_exponentsvalue_product) + (pvs_power_decoded_exponents))) /\ forall pa_i_pvs_decoded_exponentsvalue_product. (exists pa_lt_pvs_decoded_exponentsvalue_product_bound. pa_lt_pvs_decoded_exponentsvalue_product_bound + S pa_i_pvs_decoded_exponentsvalue_product = pvs_exponent_decoded_exponents) -> exists pa_p_pvs_decoded_exponentsvalue_product pa_r_pvs_decoded_exponentsvalue_product pa_s_pvs_decoded_exponentsvalue_product. ((((exists pa_h_pvs_decoded_exponentsvalue_product_factor. pa_h_pvs_decoded_exponentsvalue_product_factor + S (pa_p_pvs_decoded_exponentsvalue_product) = S ((S (pa_i_pvs_decoded_exponentsvalue_product)) * pa_c_pvs_decoded_exponentsvalue)) /\ exists pa_q_pvs_decoded_exponentsvalue_product_factor. pa_b_pvs_decoded_exponentsvalue = pa_q_pvs_decoded_exponentsvalue_product_factor * S ((S (pa_i_pvs_decoded_exponentsvalue_product)) * pa_c_pvs_decoded_exponentsvalue) + (pa_p_pvs_decoded_exponentsvalue_product))) /\ ((((exists pa_h_pvs_decoded_exponentsvalue_product_partial. pa_h_pvs_decoded_exponentsvalue_product_partial + S (pa_r_pvs_decoded_exponentsvalue_product) = S ((S (pa_i_pvs_decoded_exponentsvalue_product)) * pa_v_pvs_decoded_exponentsvalue_product)) /\ exists pa_q_pvs_decoded_exponentsvalue_product_partial. pa_u_pvs_decoded_exponentsvalue_product = pa_q_pvs_decoded_exponentsvalue_product_partial * S ((S (pa_i_pvs_decoded_exponentsvalue_product)) * pa_v_pvs_decoded_exponentsvalue_product) + (pa_r_pvs_decoded_exponentsvalue_product))) /\ ((((exists pa_h_pvs_decoded_exponentsvalue_product_successor. pa_h_pvs_decoded_exponentsvalue_product_successor + S (pa_s_pvs_decoded_exponentsvalue_product) = S ((S (S pa_i_pvs_decoded_exponentsvalue_product)) * pa_v_pvs_decoded_exponentsvalue_product)) /\ exists pa_q_pvs_decoded_exponentsvalue_product_successor. pa_u_pvs_decoded_exponentsvalue_product = pa_q_pvs_decoded_exponentsvalue_product_successor * S ((S (S pa_i_pvs_decoded_exponentsvalue_product)) * pa_v_pvs_decoded_exponentsvalue_product) + (pa_s_pvs_decoded_exponentsvalue_product))) /\ pa_s_pvs_decoded_exponentsvalue_product = pa_r_pvs_decoded_exponentsvalue_product * pa_p_pvs_decoded_exponentsvalue_product))))))))))))))))))))) -> (exists pvs_gap_decoded_index. pvs_gap_decoded_index + S (i) = (l)) -> (((exists ff_h_pvs_decoded_exponent. ff_h_pvs_decoded_exponent + S (e) = S ((S (i)) * ec)) /\ exists ff_q_pvs_decoded_exponent. eb = ff_q_pvs_decoded_exponent * S ((S (i)) * ec) + (e))) -> exists p. (~((p) = 1) /\ forall pvs_left_decoded_prime pvs_right_decoded_prime. (p) = pvs_left_decoded_prime * pvs_right_decoded_prime -> pvs_left_decoded_prime = 1 \/ pvs_right_decoded_prime = 1) /\ (((exists bpd_gap_pvs_decoded_valuation_selected_bound. bpd_gap_pvs_decoded_valuation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_decoded_valuation_selected. ((exists bpvi_b_pvs_decoded_valuation_selected_power bpvi_c_pvs_decoded_valuation_selected_power. ((forall bpvi_i_pvs_decoded_valuation_selected_power. (exists bpvi_repeat_gap_pvs_decoded_valuation_selected_power. bpvi_repeat_gap_pvs_decoded_valuation_selected_power + S bpvi_i_pvs_decoded_valuation_selected_power = e) -> (((exists bpvi_h_pvs_decoded_valuation_selected_power_repeat. bpvi_h_pvs_decoded_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_decoded_valuation_selected_power)) * bpvi_c_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_repeat. bpvi_b_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_repeat * S ((S (bpvi_i_pvs_decoded_valuation_selected_power)) * bpvi_c_pvs_decoded_valuation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_decoded_valuation_selected_power bpvi_v_pvs_decoded_valuation_selected_power. ((((exists bpvi_h_pvs_decoded_valuation_selected_power_start. bpvi_h_pvs_decoded_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_start. bpvi_u_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_start * S ((S (0)) * bpvi_v_pvs_decoded_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_decoded_valuation_selected_power_terminal. bpvi_h_pvs_decoded_valuation_selected_power_terminal + S (bpvi_result_pvs_decoded_valuation_selected) = S ((S (e)) * bpvi_v_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_terminal. bpvi_u_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_decoded_valuation_selected_power) + (bpvi_result_pvs_decoded_valuation_selected))) /\ forall bpvi_j_pvs_decoded_valuation_selected_power. (exists bpvi_product_gap_pvs_decoded_valuation_selected_power. bpvi_product_gap_pvs_decoded_valuation_selected_power + S bpvi_j_pvs_decoded_valuation_selected_power = e) -> exists bpvi_factor_pvs_decoded_valuation_selected_power bpvi_partial_pvs_decoded_valuation_selected_power bpvi_successor_pvs_decoded_valuation_selected_power. ((((exists bpvi_h_pvs_decoded_valuation_selected_power_factor. bpvi_h_pvs_decoded_valuation_selected_power_factor + S (bpvi_factor_pvs_decoded_valuation_selected_power) = S ((S (bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_c_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_factor. bpvi_b_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_factor * S ((S (bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_c_pvs_decoded_valuation_selected_power) + (bpvi_factor_pvs_decoded_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_decoded_valuation_selected_power_partial. bpvi_h_pvs_decoded_valuation_selected_power_partial + S (bpvi_partial_pvs_decoded_valuation_selected_power) = S ((S (bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_v_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_partial. bpvi_u_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_partial * S ((S (bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_v_pvs_decoded_valuation_selected_power) + (bpvi_partial_pvs_decoded_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_decoded_valuation_selected_power_successor. bpvi_h_pvs_decoded_valuation_selected_power_successor + S (bpvi_successor_pvs_decoded_valuation_selected_power) = S ((S (S bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_v_pvs_decoded_valuation_selected_power)) /\ exists bpvi_q_pvs_decoded_valuation_selected_power_successor. bpvi_u_pvs_decoded_valuation_selected_power = bpvi_q_pvs_decoded_valuation_selected_power_successor * S ((S (S bpvi_j_pvs_decoded_valuation_selected_power)) * bpvi_v_pvs_decoded_valuation_selected_power) + (bpvi_successor_pvs_decoded_valuation_selected_power))) /\ bpvi_successor_pvs_decoded_valuation_selected_power = bpvi_partial_pvs_decoded_valuation_selected_power * bpvi_factor_pvs_decoded_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_decoded_valuation_selected. n = bpvi_result_pvs_decoded_valuation_selected * bpvi_divisor_factor_pvs_decoded_valuation_selected))) /\ forall bpd_candidate_pvs_decoded_valuation. (exists bpd_gap_pvs_decoded_valuation_candidate_bound. bpd_gap_pvs_decoded_valuation_candidate_bound + (bpd_candidate_pvs_decoded_valuation) = (n)) -> (exists bpvi_result_pvs_decoded_valuation_candidate. ((exists bpvi_b_pvs_decoded_valuation_candidate_power bpvi_c_pvs_decoded_valuation_candidate_power. ((forall bpvi_i_pvs_decoded_valuation_candidate_power. (exists bpvi_repeat_gap_pvs_decoded_valuation_candidate_power. bpvi_repeat_gap_pvs_decoded_valuation_candidate_power + S bpvi_i_pvs_decoded_valuation_candidate_power = bpd_candidate_pvs_decoded_valuation) -> (((exists bpvi_h_pvs_decoded_valuation_candidate_power_repeat. bpvi_h_pvs_decoded_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_decoded_valuation_candidate_power)) * bpvi_c_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_repeat. bpvi_b_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_repeat * S ((S (bpvi_i_pvs_decoded_valuation_candidate_power)) * bpvi_c_pvs_decoded_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_decoded_valuation_candidate_power bpvi_v_pvs_decoded_valuation_candidate_power. ((((exists bpvi_h_pvs_decoded_valuation_candidate_power_start. bpvi_h_pvs_decoded_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_start. bpvi_u_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_decoded_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_decoded_valuation_candidate_power_terminal. bpvi_h_pvs_decoded_valuation_candidate_power_terminal + S (bpvi_result_pvs_decoded_valuation_candidate) = S ((S (bpd_candidate_pvs_decoded_valuation)) * bpvi_v_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_terminal. bpvi_u_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_terminal * S ((S (bpd_candidate_pvs_decoded_valuation)) * bpvi_v_pvs_decoded_valuation_candidate_power) + (bpvi_result_pvs_decoded_valuation_candidate))) /\ forall bpvi_j_pvs_decoded_valuation_candidate_power. (exists bpvi_product_gap_pvs_decoded_valuation_candidate_power. bpvi_product_gap_pvs_decoded_valuation_candidate_power + S bpvi_j_pvs_decoded_valuation_candidate_power = bpd_candidate_pvs_decoded_valuation) -> exists bpvi_factor_pvs_decoded_valuation_candidate_power bpvi_partial_pvs_decoded_valuation_candidate_power bpvi_successor_pvs_decoded_valuation_candidate_power. ((((exists bpvi_h_pvs_decoded_valuation_candidate_power_factor. bpvi_h_pvs_decoded_valuation_candidate_power_factor + S (bpvi_factor_pvs_decoded_valuation_candidate_power) = S ((S (bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_c_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_factor. bpvi_b_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_factor * S ((S (bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_c_pvs_decoded_valuation_candidate_power) + (bpvi_factor_pvs_decoded_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_decoded_valuation_candidate_power_partial. bpvi_h_pvs_decoded_valuation_candidate_power_partial + S (bpvi_partial_pvs_decoded_valuation_candidate_power) = S ((S (bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_v_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_partial. bpvi_u_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_partial * S ((S (bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_v_pvs_decoded_valuation_candidate_power) + (bpvi_partial_pvs_decoded_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_decoded_valuation_candidate_power_successor. bpvi_h_pvs_decoded_valuation_candidate_power_successor + S (bpvi_successor_pvs_decoded_valuation_candidate_power) = S ((S (S bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_v_pvs_decoded_valuation_candidate_power)) /\ exists bpvi_q_pvs_decoded_valuation_candidate_power_successor. bpvi_u_pvs_decoded_valuation_candidate_power = bpvi_q_pvs_decoded_valuation_candidate_power_successor * S ((S (S bpvi_j_pvs_decoded_valuation_candidate_power)) * bpvi_v_pvs_decoded_valuation_candidate_power) + (bpvi_successor_pvs_decoded_valuation_candidate_power))) /\ bpvi_successor_pvs_decoded_valuation_candidate_power = bpvi_partial_pvs_decoded_valuation_candidate_power * bpvi_factor_pvs_decoded_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_decoded_valuation_candidate. n = bpvi_result_pvs_decoded_valuation_candidate * bpvi_divisor_factor_pvs_decoded_valuation_candidate)) -> (exists bpd_gap_pvs_decoded_valuation_maximal. bpd_gap_pvs_decoded_valuation_maximal + (bpd_candidate_pvs_decoded_valuation) = (e)))