prime_valuation_support_append_full_power

forall n u p k P pb pc eb ec vb vc l. ~(n = 0) -> (~((p) = 1) /\ forall pvs_left_extend_prime pvs_right_extend_prime. (p) = pvs_left_extend_prime * pvs_right_extend_prime -> pvs_left_extend_prime = 1 \/ pvs_right_extend_prime = 1) -> ~(k = 0) -> (((exists bpd_gap_pvs_extend_valuation_selected_bound. bpd_gap_pvs_extend_valuation_selected_bound + (k) = (n)) /\ (exists bpvi_result_pvs_extend_valuation_selected. ((exists bpvi_b_pvs_extend_valuation_selected_power bpvi_c_pvs_extend_valuation_selected_power. ((forall bpvi_i_pvs_extend_valuation_selected_power. (exists bpvi_repeat_gap_pvs_extend_valuation_selected_power. bpvi_repeat_gap_pvs_extend_valuation_selected_power + S bpvi_i_pvs_extend_valuation_selected_power = k) -> (((exists bpvi_h_pvs_extend_valuation_selected_power_repeat. bpvi_h_pvs_extend_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_extend_valuation_selected_power)) * bpvi_c_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_repeat. bpvi_b_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_repeat * S ((S (bpvi_i_pvs_extend_valuation_selected_power)) * bpvi_c_pvs_extend_valuation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_extend_valuation_selected_power bpvi_v_pvs_extend_valuation_selected_power. ((((exists bpvi_h_pvs_extend_valuation_selected_power_start. bpvi_h_pvs_extend_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_start. bpvi_u_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_start * S ((S (0)) * bpvi_v_pvs_extend_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_valuation_selected_power_terminal. bpvi_h_pvs_extend_valuation_selected_power_terminal + S (bpvi_result_pvs_extend_valuation_selected) = S ((S (k)) * bpvi_v_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_terminal. bpvi_u_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_terminal * S ((S (k)) * bpvi_v_pvs_extend_valuation_selected_power) + (bpvi_result_pvs_extend_valuation_selected))) /\ forall bpvi_j_pvs_extend_valuation_selected_power. (exists bpvi_product_gap_pvs_extend_valuation_selected_power. bpvi_product_gap_pvs_extend_valuation_selected_power + S bpvi_j_pvs_extend_valuation_selected_power = k) -> exists bpvi_factor_pvs_extend_valuation_selected_power bpvi_partial_pvs_extend_valuation_selected_power bpvi_successor_pvs_extend_valuation_selected_power. ((((exists bpvi_h_pvs_extend_valuation_selected_power_factor. bpvi_h_pvs_extend_valuation_selected_power_factor + S (bpvi_factor_pvs_extend_valuation_selected_power) = S ((S (bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_c_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_factor. bpvi_b_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_factor * S ((S (bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_c_pvs_extend_valuation_selected_power) + (bpvi_factor_pvs_extend_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_valuation_selected_power_partial. bpvi_h_pvs_extend_valuation_selected_power_partial + S (bpvi_partial_pvs_extend_valuation_selected_power) = S ((S (bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_v_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_partial. bpvi_u_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_partial * S ((S (bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_v_pvs_extend_valuation_selected_power) + (bpvi_partial_pvs_extend_valuation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_valuation_selected_power_successor. bpvi_h_pvs_extend_valuation_selected_power_successor + S (bpvi_successor_pvs_extend_valuation_selected_power) = S ((S (S bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_v_pvs_extend_valuation_selected_power)) /\ exists bpvi_q_pvs_extend_valuation_selected_power_successor. bpvi_u_pvs_extend_valuation_selected_power = bpvi_q_pvs_extend_valuation_selected_power_successor * S ((S (S bpvi_j_pvs_extend_valuation_selected_power)) * bpvi_v_pvs_extend_valuation_selected_power) + (bpvi_successor_pvs_extend_valuation_selected_power))) /\ bpvi_successor_pvs_extend_valuation_selected_power = bpvi_partial_pvs_extend_valuation_selected_power * bpvi_factor_pvs_extend_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_valuation_selected. n = bpvi_result_pvs_extend_valuation_selected * bpvi_divisor_factor_pvs_extend_valuation_selected))) /\ forall bpd_candidate_pvs_extend_valuation. (exists bpd_gap_pvs_extend_valuation_candidate_bound. bpd_gap_pvs_extend_valuation_candidate_bound + (bpd_candidate_pvs_extend_valuation) = (n)) -> (exists bpvi_result_pvs_extend_valuation_candidate. ((exists bpvi_b_pvs_extend_valuation_candidate_power bpvi_c_pvs_extend_valuation_candidate_power. ((forall bpvi_i_pvs_extend_valuation_candidate_power. (exists bpvi_repeat_gap_pvs_extend_valuation_candidate_power. bpvi_repeat_gap_pvs_extend_valuation_candidate_power + S bpvi_i_pvs_extend_valuation_candidate_power = bpd_candidate_pvs_extend_valuation) -> (((exists bpvi_h_pvs_extend_valuation_candidate_power_repeat. bpvi_h_pvs_extend_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_extend_valuation_candidate_power)) * bpvi_c_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_repeat. bpvi_b_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_repeat * S ((S (bpvi_i_pvs_extend_valuation_candidate_power)) * bpvi_c_pvs_extend_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_extend_valuation_candidate_power bpvi_v_pvs_extend_valuation_candidate_power. ((((exists bpvi_h_pvs_extend_valuation_candidate_power_start. bpvi_h_pvs_extend_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_start. bpvi_u_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_extend_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_valuation_candidate_power_terminal. bpvi_h_pvs_extend_valuation_candidate_power_terminal + S (bpvi_result_pvs_extend_valuation_candidate) = S ((S (bpd_candidate_pvs_extend_valuation)) * bpvi_v_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_terminal. bpvi_u_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_terminal * S ((S (bpd_candidate_pvs_extend_valuation)) * bpvi_v_pvs_extend_valuation_candidate_power) + (bpvi_result_pvs_extend_valuation_candidate))) /\ forall bpvi_j_pvs_extend_valuation_candidate_power. (exists bpvi_product_gap_pvs_extend_valuation_candidate_power. bpvi_product_gap_pvs_extend_valuation_candidate_power + S bpvi_j_pvs_extend_valuation_candidate_power = bpd_candidate_pvs_extend_valuation) -> exists bpvi_factor_pvs_extend_valuation_candidate_power bpvi_partial_pvs_extend_valuation_candidate_power bpvi_successor_pvs_extend_valuation_candidate_power. ((((exists bpvi_h_pvs_extend_valuation_candidate_power_factor. bpvi_h_pvs_extend_valuation_candidate_power_factor + S (bpvi_factor_pvs_extend_valuation_candidate_power) = S ((S (bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_c_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_factor. bpvi_b_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_factor * S ((S (bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_c_pvs_extend_valuation_candidate_power) + (bpvi_factor_pvs_extend_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_valuation_candidate_power_partial. bpvi_h_pvs_extend_valuation_candidate_power_partial + S (bpvi_partial_pvs_extend_valuation_candidate_power) = S ((S (bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_v_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_partial. bpvi_u_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_partial * S ((S (bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_v_pvs_extend_valuation_candidate_power) + (bpvi_partial_pvs_extend_valuation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_valuation_candidate_power_successor. bpvi_h_pvs_extend_valuation_candidate_power_successor + S (bpvi_successor_pvs_extend_valuation_candidate_power) = S ((S (S bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_v_pvs_extend_valuation_candidate_power)) /\ exists bpvi_q_pvs_extend_valuation_candidate_power_successor. bpvi_u_pvs_extend_valuation_candidate_power = bpvi_q_pvs_extend_valuation_candidate_power_successor * S ((S (S bpvi_j_pvs_extend_valuation_candidate_power)) * bpvi_v_pvs_extend_valuation_candidate_power) + (bpvi_successor_pvs_extend_valuation_candidate_power))) /\ bpvi_successor_pvs_extend_valuation_candidate_power = bpvi_partial_pvs_extend_valuation_candidate_power * bpvi_factor_pvs_extend_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_valuation_candidate. n = bpvi_result_pvs_extend_valuation_candidate * bpvi_divisor_factor_pvs_extend_valuation_candidate)) -> (exists bpd_gap_pvs_extend_valuation_maximal. bpd_gap_pvs_extend_valuation_maximal + (bpd_candidate_pvs_extend_valuation) = (k))) -> (exists pa_b_pvs_extend_power pa_c_pvs_extend_power. ((forall pa_i_pvs_extend_power_repeat. (exists pa_lt_pvs_extend_power_repeat_bound. pa_lt_pvs_extend_power_repeat_bound + S pa_i_pvs_extend_power_repeat = k) -> (((exists pa_h_pvs_extend_power_repeat_decoded. pa_h_pvs_extend_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_extend_power_repeat)) * pa_c_pvs_extend_power)) /\ exists pa_q_pvs_extend_power_repeat_decoded. pa_b_pvs_extend_power = pa_q_pvs_extend_power_repeat_decoded * S ((S (pa_i_pvs_extend_power_repeat)) * pa_c_pvs_extend_power) + (p)))) /\ (exists pa_u_pvs_extend_power_product pa_v_pvs_extend_power_product. ((((exists pa_h_pvs_extend_power_product_start. pa_h_pvs_extend_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_extend_power_product)) /\ exists pa_q_pvs_extend_power_product_start. pa_u_pvs_extend_power_product = pa_q_pvs_extend_power_product_start * S ((S (0)) * pa_v_pvs_extend_power_product) + (1))) /\ ((((exists pa_h_pvs_extend_power_product_terminal. pa_h_pvs_extend_power_product_terminal + S (P) = S ((S (k)) * pa_v_pvs_extend_power_product)) /\ exists pa_q_pvs_extend_power_product_terminal. pa_u_pvs_extend_power_product = pa_q_pvs_extend_power_product_terminal * S ((S (k)) * pa_v_pvs_extend_power_product) + (P))) /\ forall pa_i_pvs_extend_power_product. (exists pa_lt_pvs_extend_power_product_bound. pa_lt_pvs_extend_power_product_bound + S pa_i_pvs_extend_power_product = k) -> exists pa_p_pvs_extend_power_product pa_r_pvs_extend_power_product pa_s_pvs_extend_power_product. ((((exists pa_h_pvs_extend_power_product_factor. pa_h_pvs_extend_power_product_factor + S (pa_p_pvs_extend_power_product) = S ((S (pa_i_pvs_extend_power_product)) * pa_c_pvs_extend_power)) /\ exists pa_q_pvs_extend_power_product_factor. pa_b_pvs_extend_power = pa_q_pvs_extend_power_product_factor * S ((S (pa_i_pvs_extend_power_product)) * pa_c_pvs_extend_power) + (pa_p_pvs_extend_power_product))) /\ ((((exists pa_h_pvs_extend_power_product_partial. pa_h_pvs_extend_power_product_partial + S (pa_r_pvs_extend_power_product) = S ((S (pa_i_pvs_extend_power_product)) * pa_v_pvs_extend_power_product)) /\ exists pa_q_pvs_extend_power_product_partial. pa_u_pvs_extend_power_product = pa_q_pvs_extend_power_product_partial * S ((S (pa_i_pvs_extend_power_product)) * pa_v_pvs_extend_power_product) + (pa_r_pvs_extend_power_product))) /\ ((((exists pa_h_pvs_extend_power_product_successor. pa_h_pvs_extend_power_product_successor + S (pa_s_pvs_extend_power_product) = S ((S (S pa_i_pvs_extend_power_product)) * pa_v_pvs_extend_power_product)) /\ exists pa_q_pvs_extend_power_product_successor. pa_u_pvs_extend_power_product = pa_q_pvs_extend_power_product_successor * S ((S (S pa_i_pvs_extend_power_product)) * pa_v_pvs_extend_power_product) + (pa_s_pvs_extend_power_product))) /\ pa_s_pvs_extend_power_product = pa_r_pvs_extend_power_product * pa_p_pvs_extend_power_product)))))))) -> ~(exists pvs_factor_extend_fresh. (u) = (p) * pvs_factor_extend_fresh) -> n = P * u -> (((~((u) = 0)) /\ (((forall pfp_i_pvs_extend_sourcedistinct pfp_j_pvs_extend_sourcedistinct pfp_a_pvs_extend_sourcedistinct. (exists pfp_gap_pvs_extend_sourcedistinctfirst. pfp_gap_pvs_extend_sourcedistinctfirst + S (pfp_i_pvs_extend_sourcedistinct) = (l)) -> (exists pfp_gap_pvs_extend_sourcedistinctsecond. pfp_gap_pvs_extend_sourcedistinctsecond + S (pfp_j_pvs_extend_sourcedistinct) = (l)) -> (((exists ff_h_pfp_pvs_extend_sourcedistinctleft. ff_h_pfp_pvs_extend_sourcedistinctleft + S (pfp_a_pvs_extend_sourcedistinct) = S ((S (pfp_i_pvs_extend_sourcedistinct)) * pc)) /\ exists ff_q_pfp_pvs_extend_sourcedistinctleft. pb = ff_q_pfp_pvs_extend_sourcedistinctleft * S ((S (pfp_i_pvs_extend_sourcedistinct)) * pc) + (pfp_a_pvs_extend_sourcedistinct))) -> (((exists ff_h_pfp_pvs_extend_sourcedistinctright. ff_h_pfp_pvs_extend_sourcedistinctright + S (pfp_a_pvs_extend_sourcedistinct) = S ((S (pfp_j_pvs_extend_sourcedistinct)) * pc)) /\ exists ff_q_pfp_pvs_extend_sourcedistinctright. pb = ff_q_pfp_pvs_extend_sourcedistinctright * S ((S (pfp_j_pvs_extend_sourcedistinct)) * pc) + (pfp_a_pvs_extend_sourcedistinct))) -> pfp_i_pvs_extend_sourcedistinct = pfp_j_pvs_extend_sourcedistinct) /\ (((forall pvs_index_extend_sourceentries. (exists pvs_gap_extend_sourceentriesindex. pvs_gap_extend_sourceentriesindex + S (pvs_index_extend_sourceentries) = (l)) -> exists pvs_prime_extend_sourceentries pvs_exponent_extend_sourceentries pvs_power_extend_sourceentries. (((((exists ff_h_pvs_extend_sourceentriesprime. ff_h_pvs_extend_sourceentriesprime + S (pvs_prime_extend_sourceentries) = S ((S (pvs_index_extend_sourceentries)) * pc)) /\ exists ff_q_pvs_extend_sourceentriesprime. pb = ff_q_pvs_extend_sourceentriesprime * S ((S (pvs_index_extend_sourceentries)) * pc) + (pvs_prime_extend_sourceentries))) /\ (((((exists ff_h_pvs_extend_sourceentriesexponent. ff_h_pvs_extend_sourceentriesexponent + S (pvs_exponent_extend_sourceentries) = S ((S (pvs_index_extend_sourceentries)) * ec)) /\ exists ff_q_pvs_extend_sourceentriesexponent. eb = ff_q_pvs_extend_sourceentriesexponent * S ((S (pvs_index_extend_sourceentries)) * ec) + (pvs_exponent_extend_sourceentries))) /\ (((((exists ff_h_pvs_extend_sourceentriespower. ff_h_pvs_extend_sourceentriespower + S (pvs_power_extend_sourceentries) = S ((S (pvs_index_extend_sourceentries)) * vc)) /\ exists ff_q_pvs_extend_sourceentriespower. vb = ff_q_pvs_extend_sourceentriespower * S ((S (pvs_index_extend_sourceentries)) * vc) + (pvs_power_extend_sourceentries))) /\ (((~((pvs_prime_extend_sourceentries) = 1) /\ forall pvs_left_extend_sourceentriesdomain pvs_right_extend_sourceentriesdomain. (pvs_prime_extend_sourceentries) = pvs_left_extend_sourceentriesdomain * pvs_right_extend_sourceentriesdomain -> pvs_left_extend_sourceentriesdomain = 1 \/ pvs_right_extend_sourceentriesdomain = 1) /\ (((~(pvs_exponent_extend_sourceentries = 0)) /\ (((((exists bpd_gap_pvs_extend_sourceentriesvaluation_selected_bound. bpd_gap_pvs_extend_sourceentriesvaluation_selected_bound + (pvs_exponent_extend_sourceentries) = (u)) /\ (exists bpvi_result_pvs_extend_sourceentriesvaluation_selected. ((exists bpvi_b_pvs_extend_sourceentriesvaluation_selected_power bpvi_c_pvs_extend_sourceentriesvaluation_selected_power. ((forall bpvi_i_pvs_extend_sourceentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_extend_sourceentriesvaluation_selected_power. bpvi_repeat_gap_pvs_extend_sourceentriesvaluation_selected_power + S bpvi_i_pvs_extend_sourceentriesvaluation_selected_power = pvs_exponent_extend_sourceentries) -> (((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_repeat. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_repeat + S (pvs_prime_extend_sourceentries) = S ((S (bpvi_i_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_repeat. bpvi_b_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_selected_power) + (pvs_prime_extend_sourceentries)))) /\ (exists bpvi_u_pvs_extend_sourceentriesvaluation_selected_power bpvi_v_pvs_extend_sourceentriesvaluation_selected_power. ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_start. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_start. bpvi_u_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_terminal. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_extend_sourceentriesvaluation_selected) = S ((S (pvs_exponent_extend_sourceentries)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_terminal. bpvi_u_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_extend_sourceentries)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power) + (bpvi_result_pvs_extend_sourceentriesvaluation_selected))) /\ forall bpvi_j_pvs_extend_sourceentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_extend_sourceentriesvaluation_selected_power. bpvi_product_gap_pvs_extend_sourceentriesvaluation_selected_power + S bpvi_j_pvs_extend_sourceentriesvaluation_selected_power = pvs_exponent_extend_sourceentries) -> exists bpvi_factor_pvs_extend_sourceentriesvaluation_selected_power bpvi_partial_pvs_extend_sourceentriesvaluation_selected_power bpvi_successor_pvs_extend_sourceentriesvaluation_selected_power. ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_factor. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_extend_sourceentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_factor. bpvi_b_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_selected_power) + (bpvi_factor_pvs_extend_sourceentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_partial. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_extend_sourceentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_partial. bpvi_u_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power) + (bpvi_partial_pvs_extend_sourceentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_successor. bpvi_h_pvs_extend_sourceentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_extend_sourceentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_successor. bpvi_u_pvs_extend_sourceentriesvaluation_selected_power = bpvi_q_pvs_extend_sourceentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_extend_sourceentriesvaluation_selected_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_selected_power) + (bpvi_successor_pvs_extend_sourceentriesvaluation_selected_power))) /\ bpvi_successor_pvs_extend_sourceentriesvaluation_selected_power = bpvi_partial_pvs_extend_sourceentriesvaluation_selected_power * bpvi_factor_pvs_extend_sourceentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_sourceentriesvaluation_selected. u = bpvi_result_pvs_extend_sourceentriesvaluation_selected * bpvi_divisor_factor_pvs_extend_sourceentriesvaluation_selected))) /\ forall bpd_candidate_pvs_extend_sourceentriesvaluation. (exists bpd_gap_pvs_extend_sourceentriesvaluation_candidate_bound. bpd_gap_pvs_extend_sourceentriesvaluation_candidate_bound + (bpd_candidate_pvs_extend_sourceentriesvaluation) = (u)) -> (exists bpvi_result_pvs_extend_sourceentriesvaluation_candidate. ((exists bpvi_b_pvs_extend_sourceentriesvaluation_candidate_power bpvi_c_pvs_extend_sourceentriesvaluation_candidate_power. ((forall bpvi_i_pvs_extend_sourceentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_extend_sourceentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_extend_sourceentriesvaluation_candidate_power + S bpvi_i_pvs_extend_sourceentriesvaluation_candidate_power = bpd_candidate_pvs_extend_sourceentriesvaluation) -> (((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_repeat. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_repeat + S (pvs_prime_extend_sourceentries) = S ((S (bpvi_i_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_repeat. bpvi_b_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_candidate_power) + (pvs_prime_extend_sourceentries)))) /\ (exists bpvi_u_pvs_extend_sourceentriesvaluation_candidate_power bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_start. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_start. bpvi_u_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_terminal. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_extend_sourceentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_extend_sourceentriesvaluation)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_terminal. bpvi_u_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_extend_sourceentriesvaluation)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power) + (bpvi_result_pvs_extend_sourceentriesvaluation_candidate))) /\ forall bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_extend_sourceentriesvaluation_candidate_power. bpvi_product_gap_pvs_extend_sourceentriesvaluation_candidate_power + S bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power = bpd_candidate_pvs_extend_sourceentriesvaluation) -> exists bpvi_factor_pvs_extend_sourceentriesvaluation_candidate_power bpvi_partial_pvs_extend_sourceentriesvaluation_candidate_power bpvi_successor_pvs_extend_sourceentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_factor. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_extend_sourceentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_factor. bpvi_b_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_sourceentriesvaluation_candidate_power) + (bpvi_factor_pvs_extend_sourceentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_partial. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_extend_sourceentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_partial. bpvi_u_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power) + (bpvi_partial_pvs_extend_sourceentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_successor. bpvi_h_pvs_extend_sourceentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_extend_sourceentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_successor. bpvi_u_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_q_pvs_extend_sourceentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_extend_sourceentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_sourceentriesvaluation_candidate_power) + (bpvi_successor_pvs_extend_sourceentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_extend_sourceentriesvaluation_candidate_power = bpvi_partial_pvs_extend_sourceentriesvaluation_candidate_power * bpvi_factor_pvs_extend_sourceentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_sourceentriesvaluation_candidate. u = bpvi_result_pvs_extend_sourceentriesvaluation_candidate * bpvi_divisor_factor_pvs_extend_sourceentriesvaluation_candidate)) -> (exists bpd_gap_pvs_extend_sourceentriesvaluation_maximal. bpd_gap_pvs_extend_sourceentriesvaluation_maximal + (bpd_candidate_pvs_extend_sourceentriesvaluation) = (pvs_exponent_extend_sourceentries))) /\ (exists pa_b_pvs_extend_sourceentriesvalue pa_c_pvs_extend_sourceentriesvalue. ((forall pa_i_pvs_extend_sourceentriesvalue_repeat. (exists pa_lt_pvs_extend_sourceentriesvalue_repeat_bound. pa_lt_pvs_extend_sourceentriesvalue_repeat_bound + S pa_i_pvs_extend_sourceentriesvalue_repeat = pvs_exponent_extend_sourceentries) -> (((exists pa_h_pvs_extend_sourceentriesvalue_repeat_decoded. pa_h_pvs_extend_sourceentriesvalue_repeat_decoded + S (pvs_prime_extend_sourceentries) = S ((S (pa_i_pvs_extend_sourceentriesvalue_repeat)) * pa_c_pvs_extend_sourceentriesvalue)) /\ exists pa_q_pvs_extend_sourceentriesvalue_repeat_decoded. pa_b_pvs_extend_sourceentriesvalue = pa_q_pvs_extend_sourceentriesvalue_repeat_decoded * S ((S (pa_i_pvs_extend_sourceentriesvalue_repeat)) * pa_c_pvs_extend_sourceentriesvalue) + (pvs_prime_extend_sourceentries)))) /\ (exists pa_u_pvs_extend_sourceentriesvalue_product pa_v_pvs_extend_sourceentriesvalue_product. ((((exists pa_h_pvs_extend_sourceentriesvalue_product_start. pa_h_pvs_extend_sourceentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_extend_sourceentriesvalue_product)) /\ exists pa_q_pvs_extend_sourceentriesvalue_product_start. pa_u_pvs_extend_sourceentriesvalue_product = pa_q_pvs_extend_sourceentriesvalue_product_start * S ((S (0)) * pa_v_pvs_extend_sourceentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_extend_sourceentriesvalue_product_terminal. pa_h_pvs_extend_sourceentriesvalue_product_terminal + S (pvs_power_extend_sourceentries) = S ((S (pvs_exponent_extend_sourceentries)) * pa_v_pvs_extend_sourceentriesvalue_product)) /\ exists pa_q_pvs_extend_sourceentriesvalue_product_terminal. pa_u_pvs_extend_sourceentriesvalue_product = pa_q_pvs_extend_sourceentriesvalue_product_terminal * S ((S (pvs_exponent_extend_sourceentries)) * pa_v_pvs_extend_sourceentriesvalue_product) + (pvs_power_extend_sourceentries))) /\ forall pa_i_pvs_extend_sourceentriesvalue_product. (exists pa_lt_pvs_extend_sourceentriesvalue_product_bound. pa_lt_pvs_extend_sourceentriesvalue_product_bound + S pa_i_pvs_extend_sourceentriesvalue_product = pvs_exponent_extend_sourceentries) -> exists pa_p_pvs_extend_sourceentriesvalue_product pa_r_pvs_extend_sourceentriesvalue_product pa_s_pvs_extend_sourceentriesvalue_product. ((((exists pa_h_pvs_extend_sourceentriesvalue_product_factor. pa_h_pvs_extend_sourceentriesvalue_product_factor + S (pa_p_pvs_extend_sourceentriesvalue_product) = S ((S (pa_i_pvs_extend_sourceentriesvalue_product)) * pa_c_pvs_extend_sourceentriesvalue)) /\ exists pa_q_pvs_extend_sourceentriesvalue_product_factor. pa_b_pvs_extend_sourceentriesvalue = pa_q_pvs_extend_sourceentriesvalue_product_factor * S ((S (pa_i_pvs_extend_sourceentriesvalue_product)) * pa_c_pvs_extend_sourceentriesvalue) + (pa_p_pvs_extend_sourceentriesvalue_product))) /\ ((((exists pa_h_pvs_extend_sourceentriesvalue_product_partial. pa_h_pvs_extend_sourceentriesvalue_product_partial + S (pa_r_pvs_extend_sourceentriesvalue_product) = S ((S (pa_i_pvs_extend_sourceentriesvalue_product)) * pa_v_pvs_extend_sourceentriesvalue_product)) /\ exists pa_q_pvs_extend_sourceentriesvalue_product_partial. pa_u_pvs_extend_sourceentriesvalue_product = pa_q_pvs_extend_sourceentriesvalue_product_partial * S ((S (pa_i_pvs_extend_sourceentriesvalue_product)) * pa_v_pvs_extend_sourceentriesvalue_product) + (pa_r_pvs_extend_sourceentriesvalue_product))) /\ ((((exists pa_h_pvs_extend_sourceentriesvalue_product_successor. pa_h_pvs_extend_sourceentriesvalue_product_successor + S (pa_s_pvs_extend_sourceentriesvalue_product) = S ((S (S pa_i_pvs_extend_sourceentriesvalue_product)) * pa_v_pvs_extend_sourceentriesvalue_product)) /\ exists pa_q_pvs_extend_sourceentriesvalue_product_successor. pa_u_pvs_extend_sourceentriesvalue_product = pa_q_pvs_extend_sourceentriesvalue_product_successor * S ((S (S pa_i_pvs_extend_sourceentriesvalue_product)) * pa_v_pvs_extend_sourceentriesvalue_product) + (pa_s_pvs_extend_sourceentriesvalue_product))) /\ pa_s_pvs_extend_sourceentriesvalue_product = pa_r_pvs_extend_sourceentriesvalue_product * pa_p_pvs_extend_sourceentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_extend_sourcecover. (~((pvs_divisor_extend_sourcecover) = 1) /\ forall pvs_left_extend_sourcecoverprime pvs_right_extend_sourcecoverprime. (pvs_divisor_extend_sourcecover) = pvs_left_extend_sourcecoverprime * pvs_right_extend_sourcecoverprime -> pvs_left_extend_sourcecoverprime = 1 \/ pvs_right_extend_sourcecoverprime = 1) -> (exists pvs_factor_extend_sourcecoverdivides. (u) = (pvs_divisor_extend_sourcecover) * pvs_factor_extend_sourcecoverdivides) -> exists pvs_position_extend_sourcecover. (exists pvs_gap_extend_sourcecoverbound. pvs_gap_extend_sourcecoverbound + S (pvs_position_extend_sourcecover) = (l)) /\ (((exists ff_h_pvs_extend_sourcecoverentry. ff_h_pvs_extend_sourcecoverentry + S (pvs_divisor_extend_sourcecover) = S ((S (pvs_position_extend_sourcecover)) * pc)) /\ exists ff_q_pvs_extend_sourcecoverentry. pb = ff_q_pvs_extend_sourcecoverentry * S ((S (pvs_position_extend_sourcecover)) * pc) + (pvs_divisor_extend_sourcecover)))) /\ (exists ff_u_pvs_extend_sourceproduct ff_v_pvs_extend_sourceproduct. ((((exists ff_h_pvs_extend_sourceproduct_start. ff_h_pvs_extend_sourceproduct_start + S (1) = S ((S (0)) * ff_v_pvs_extend_sourceproduct)) /\ exists ff_q_pvs_extend_sourceproduct_start. ff_u_pvs_extend_sourceproduct = ff_q_pvs_extend_sourceproduct_start * S ((S (0)) * ff_v_pvs_extend_sourceproduct) + (1))) /\ ((((exists ff_h_pvs_extend_sourceproduct_terminal. ff_h_pvs_extend_sourceproduct_terminal + S (u) = S ((S (l)) * ff_v_pvs_extend_sourceproduct)) /\ exists ff_q_pvs_extend_sourceproduct_terminal. ff_u_pvs_extend_sourceproduct = ff_q_pvs_extend_sourceproduct_terminal * S ((S (l)) * ff_v_pvs_extend_sourceproduct) + (u))) /\ forall ff_i_pvs_extend_sourceproduct. (exists ff_lt_pvs_extend_sourceproduct_bound. ff_lt_pvs_extend_sourceproduct_bound + S ff_i_pvs_extend_sourceproduct = l) -> exists ff_p_pvs_extend_sourceproduct ff_r_pvs_extend_sourceproduct ff_s_pvs_extend_sourceproduct. ((((exists ff_h_pvs_extend_sourceproduct_factor. ff_h_pvs_extend_sourceproduct_factor + S (ff_p_pvs_extend_sourceproduct) = S ((S (ff_i_pvs_extend_sourceproduct)) * vc)) /\ exists ff_q_pvs_extend_sourceproduct_factor. vb = ff_q_pvs_extend_sourceproduct_factor * S ((S (ff_i_pvs_extend_sourceproduct)) * vc) + (ff_p_pvs_extend_sourceproduct))) /\ ((((exists ff_h_pvs_extend_sourceproduct_partial. ff_h_pvs_extend_sourceproduct_partial + S (ff_r_pvs_extend_sourceproduct) = S ((S (ff_i_pvs_extend_sourceproduct)) * ff_v_pvs_extend_sourceproduct)) /\ exists ff_q_pvs_extend_sourceproduct_partial. ff_u_pvs_extend_sourceproduct = ff_q_pvs_extend_sourceproduct_partial * S ((S (ff_i_pvs_extend_sourceproduct)) * ff_v_pvs_extend_sourceproduct) + (ff_r_pvs_extend_sourceproduct))) /\ ((((exists ff_h_pvs_extend_sourceproduct_successor. ff_h_pvs_extend_sourceproduct_successor + S (ff_s_pvs_extend_sourceproduct) = S ((S (S ff_i_pvs_extend_sourceproduct)) * ff_v_pvs_extend_sourceproduct)) /\ exists ff_q_pvs_extend_sourceproduct_successor. ff_u_pvs_extend_sourceproduct = ff_q_pvs_extend_sourceproduct_successor * S ((S (S ff_i_pvs_extend_sourceproduct)) * ff_v_pvs_extend_sourceproduct) + (ff_s_pvs_extend_sourceproduct))) /\ ff_s_pvs_extend_sourceproduct = ff_r_pvs_extend_sourceproduct * ff_p_pvs_extend_sourceproduct)))))))))))))) -> exists qb qc fb fc wb wc. (((~((n) = 0)) /\ (((forall pfp_i_pvs_extend_targetdistinct pfp_j_pvs_extend_targetdistinct pfp_a_pvs_extend_targetdistinct. (exists pfp_gap_pvs_extend_targetdistinctfirst. pfp_gap_pvs_extend_targetdistinctfirst + S (pfp_i_pvs_extend_targetdistinct) = (S l)) -> (exists pfp_gap_pvs_extend_targetdistinctsecond. pfp_gap_pvs_extend_targetdistinctsecond + S (pfp_j_pvs_extend_targetdistinct) = (S l)) -> (((exists ff_h_pfp_pvs_extend_targetdistinctleft. ff_h_pfp_pvs_extend_targetdistinctleft + S (pfp_a_pvs_extend_targetdistinct) = S ((S (pfp_i_pvs_extend_targetdistinct)) * qc)) /\ exists ff_q_pfp_pvs_extend_targetdistinctleft. qb = ff_q_pfp_pvs_extend_targetdistinctleft * S ((S (pfp_i_pvs_extend_targetdistinct)) * qc) + (pfp_a_pvs_extend_targetdistinct))) -> (((exists ff_h_pfp_pvs_extend_targetdistinctright. ff_h_pfp_pvs_extend_targetdistinctright + S (pfp_a_pvs_extend_targetdistinct) = S ((S (pfp_j_pvs_extend_targetdistinct)) * qc)) /\ exists ff_q_pfp_pvs_extend_targetdistinctright. qb = ff_q_pfp_pvs_extend_targetdistinctright * S ((S (pfp_j_pvs_extend_targetdistinct)) * qc) + (pfp_a_pvs_extend_targetdistinct))) -> pfp_i_pvs_extend_targetdistinct = pfp_j_pvs_extend_targetdistinct) /\ (((forall pvs_index_extend_targetentries. (exists pvs_gap_extend_targetentriesindex. pvs_gap_extend_targetentriesindex + S (pvs_index_extend_targetentries) = (S l)) -> exists pvs_prime_extend_targetentries pvs_exponent_extend_targetentries pvs_power_extend_targetentries. (((((exists ff_h_pvs_extend_targetentriesprime. ff_h_pvs_extend_targetentriesprime + S (pvs_prime_extend_targetentries) = S ((S (pvs_index_extend_targetentries)) * qc)) /\ exists ff_q_pvs_extend_targetentriesprime. qb = ff_q_pvs_extend_targetentriesprime * S ((S (pvs_index_extend_targetentries)) * qc) + (pvs_prime_extend_targetentries))) /\ (((((exists ff_h_pvs_extend_targetentriesexponent. ff_h_pvs_extend_targetentriesexponent + S (pvs_exponent_extend_targetentries) = S ((S (pvs_index_extend_targetentries)) * fc)) /\ exists ff_q_pvs_extend_targetentriesexponent. fb = ff_q_pvs_extend_targetentriesexponent * S ((S (pvs_index_extend_targetentries)) * fc) + (pvs_exponent_extend_targetentries))) /\ (((((exists ff_h_pvs_extend_targetentriespower. ff_h_pvs_extend_targetentriespower + S (pvs_power_extend_targetentries) = S ((S (pvs_index_extend_targetentries)) * wc)) /\ exists ff_q_pvs_extend_targetentriespower. wb = ff_q_pvs_extend_targetentriespower * S ((S (pvs_index_extend_targetentries)) * wc) + (pvs_power_extend_targetentries))) /\ (((~((pvs_prime_extend_targetentries) = 1) /\ forall pvs_left_extend_targetentriesdomain pvs_right_extend_targetentriesdomain. (pvs_prime_extend_targetentries) = pvs_left_extend_targetentriesdomain * pvs_right_extend_targetentriesdomain -> pvs_left_extend_targetentriesdomain = 1 \/ pvs_right_extend_targetentriesdomain = 1) /\ (((~(pvs_exponent_extend_targetentries = 0)) /\ (((((exists bpd_gap_pvs_extend_targetentriesvaluation_selected_bound. bpd_gap_pvs_extend_targetentriesvaluation_selected_bound + (pvs_exponent_extend_targetentries) = (n)) /\ (exists bpvi_result_pvs_extend_targetentriesvaluation_selected. ((exists bpvi_b_pvs_extend_targetentriesvaluation_selected_power bpvi_c_pvs_extend_targetentriesvaluation_selected_power. ((forall bpvi_i_pvs_extend_targetentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_extend_targetentriesvaluation_selected_power. bpvi_repeat_gap_pvs_extend_targetentriesvaluation_selected_power + S bpvi_i_pvs_extend_targetentriesvaluation_selected_power = pvs_exponent_extend_targetentries) -> (((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_repeat. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_repeat + S (pvs_prime_extend_targetentries) = S ((S (bpvi_i_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_c_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_repeat. bpvi_b_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_c_pvs_extend_targetentriesvaluation_selected_power) + (pvs_prime_extend_targetentries)))) /\ (exists bpvi_u_pvs_extend_targetentriesvaluation_selected_power bpvi_v_pvs_extend_targetentriesvaluation_selected_power. ((((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_start. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_start. bpvi_u_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_terminal. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_extend_targetentriesvaluation_selected) = S ((S (pvs_exponent_extend_targetentries)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_terminal. bpvi_u_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_extend_targetentries)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power) + (bpvi_result_pvs_extend_targetentriesvaluation_selected))) /\ forall bpvi_j_pvs_extend_targetentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_extend_targetentriesvaluation_selected_power. bpvi_product_gap_pvs_extend_targetentriesvaluation_selected_power + S bpvi_j_pvs_extend_targetentriesvaluation_selected_power = pvs_exponent_extend_targetentries) -> exists bpvi_factor_pvs_extend_targetentriesvaluation_selected_power bpvi_partial_pvs_extend_targetentriesvaluation_selected_power bpvi_successor_pvs_extend_targetentriesvaluation_selected_power. ((((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_factor. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_extend_targetentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_c_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_factor. bpvi_b_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_c_pvs_extend_targetentriesvaluation_selected_power) + (bpvi_factor_pvs_extend_targetentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_partial. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_extend_targetentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_partial. bpvi_u_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power) + (bpvi_partial_pvs_extend_targetentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_selected_power_successor. bpvi_h_pvs_extend_targetentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_extend_targetentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_selected_power_successor. bpvi_u_pvs_extend_targetentriesvaluation_selected_power = bpvi_q_pvs_extend_targetentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_extend_targetentriesvaluation_selected_power)) * bpvi_v_pvs_extend_targetentriesvaluation_selected_power) + (bpvi_successor_pvs_extend_targetentriesvaluation_selected_power))) /\ bpvi_successor_pvs_extend_targetentriesvaluation_selected_power = bpvi_partial_pvs_extend_targetentriesvaluation_selected_power * bpvi_factor_pvs_extend_targetentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_targetentriesvaluation_selected. n = bpvi_result_pvs_extend_targetentriesvaluation_selected * bpvi_divisor_factor_pvs_extend_targetentriesvaluation_selected))) /\ forall bpd_candidate_pvs_extend_targetentriesvaluation. (exists bpd_gap_pvs_extend_targetentriesvaluation_candidate_bound. bpd_gap_pvs_extend_targetentriesvaluation_candidate_bound + (bpd_candidate_pvs_extend_targetentriesvaluation) = (n)) -> (exists bpvi_result_pvs_extend_targetentriesvaluation_candidate. ((exists bpvi_b_pvs_extend_targetentriesvaluation_candidate_power bpvi_c_pvs_extend_targetentriesvaluation_candidate_power. ((forall bpvi_i_pvs_extend_targetentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_extend_targetentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_extend_targetentriesvaluation_candidate_power + S bpvi_i_pvs_extend_targetentriesvaluation_candidate_power = bpd_candidate_pvs_extend_targetentriesvaluation) -> (((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_repeat. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_repeat + S (pvs_prime_extend_targetentries) = S ((S (bpvi_i_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_repeat. bpvi_b_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_targetentriesvaluation_candidate_power) + (pvs_prime_extend_targetentries)))) /\ (exists bpvi_u_pvs_extend_targetentriesvaluation_candidate_power bpvi_v_pvs_extend_targetentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_start. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_start. bpvi_u_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_terminal. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_extend_targetentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_extend_targetentriesvaluation)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_terminal. bpvi_u_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_extend_targetentriesvaluation)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power) + (bpvi_result_pvs_extend_targetentriesvaluation_candidate))) /\ forall bpvi_j_pvs_extend_targetentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_extend_targetentriesvaluation_candidate_power. bpvi_product_gap_pvs_extend_targetentriesvaluation_candidate_power + S bpvi_j_pvs_extend_targetentriesvaluation_candidate_power = bpd_candidate_pvs_extend_targetentriesvaluation) -> exists bpvi_factor_pvs_extend_targetentriesvaluation_candidate_power bpvi_partial_pvs_extend_targetentriesvaluation_candidate_power bpvi_successor_pvs_extend_targetentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_factor. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_extend_targetentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_factor. bpvi_b_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_c_pvs_extend_targetentriesvaluation_candidate_power) + (bpvi_factor_pvs_extend_targetentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_partial. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_extend_targetentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_partial. bpvi_u_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power) + (bpvi_partial_pvs_extend_targetentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_successor. bpvi_h_pvs_extend_targetentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_extend_targetentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_successor. bpvi_u_pvs_extend_targetentriesvaluation_candidate_power = bpvi_q_pvs_extend_targetentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_extend_targetentriesvaluation_candidate_power)) * bpvi_v_pvs_extend_targetentriesvaluation_candidate_power) + (bpvi_successor_pvs_extend_targetentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_extend_targetentriesvaluation_candidate_power = bpvi_partial_pvs_extend_targetentriesvaluation_candidate_power * bpvi_factor_pvs_extend_targetentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_extend_targetentriesvaluation_candidate. n = bpvi_result_pvs_extend_targetentriesvaluation_candidate * bpvi_divisor_factor_pvs_extend_targetentriesvaluation_candidate)) -> (exists bpd_gap_pvs_extend_targetentriesvaluation_maximal. bpd_gap_pvs_extend_targetentriesvaluation_maximal + (bpd_candidate_pvs_extend_targetentriesvaluation) = (pvs_exponent_extend_targetentries))) /\ (exists pa_b_pvs_extend_targetentriesvalue pa_c_pvs_extend_targetentriesvalue. ((forall pa_i_pvs_extend_targetentriesvalue_repeat. (exists pa_lt_pvs_extend_targetentriesvalue_repeat_bound. pa_lt_pvs_extend_targetentriesvalue_repeat_bound + S pa_i_pvs_extend_targetentriesvalue_repeat = pvs_exponent_extend_targetentries) -> (((exists pa_h_pvs_extend_targetentriesvalue_repeat_decoded. pa_h_pvs_extend_targetentriesvalue_repeat_decoded + S (pvs_prime_extend_targetentries) = S ((S (pa_i_pvs_extend_targetentriesvalue_repeat)) * pa_c_pvs_extend_targetentriesvalue)) /\ exists pa_q_pvs_extend_targetentriesvalue_repeat_decoded. pa_b_pvs_extend_targetentriesvalue = pa_q_pvs_extend_targetentriesvalue_repeat_decoded * S ((S (pa_i_pvs_extend_targetentriesvalue_repeat)) * pa_c_pvs_extend_targetentriesvalue) + (pvs_prime_extend_targetentries)))) /\ (exists pa_u_pvs_extend_targetentriesvalue_product pa_v_pvs_extend_targetentriesvalue_product. ((((exists pa_h_pvs_extend_targetentriesvalue_product_start. pa_h_pvs_extend_targetentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_extend_targetentriesvalue_product)) /\ exists pa_q_pvs_extend_targetentriesvalue_product_start. pa_u_pvs_extend_targetentriesvalue_product = pa_q_pvs_extend_targetentriesvalue_product_start * S ((S (0)) * pa_v_pvs_extend_targetentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_extend_targetentriesvalue_product_terminal. pa_h_pvs_extend_targetentriesvalue_product_terminal + S (pvs_power_extend_targetentries) = S ((S (pvs_exponent_extend_targetentries)) * pa_v_pvs_extend_targetentriesvalue_product)) /\ exists pa_q_pvs_extend_targetentriesvalue_product_terminal. pa_u_pvs_extend_targetentriesvalue_product = pa_q_pvs_extend_targetentriesvalue_product_terminal * S ((S (pvs_exponent_extend_targetentries)) * pa_v_pvs_extend_targetentriesvalue_product) + (pvs_power_extend_targetentries))) /\ forall pa_i_pvs_extend_targetentriesvalue_product. (exists pa_lt_pvs_extend_targetentriesvalue_product_bound. pa_lt_pvs_extend_targetentriesvalue_product_bound + S pa_i_pvs_extend_targetentriesvalue_product = pvs_exponent_extend_targetentries) -> exists pa_p_pvs_extend_targetentriesvalue_product pa_r_pvs_extend_targetentriesvalue_product pa_s_pvs_extend_targetentriesvalue_product. ((((exists pa_h_pvs_extend_targetentriesvalue_product_factor. pa_h_pvs_extend_targetentriesvalue_product_factor + S (pa_p_pvs_extend_targetentriesvalue_product) = S ((S (pa_i_pvs_extend_targetentriesvalue_product)) * pa_c_pvs_extend_targetentriesvalue)) /\ exists pa_q_pvs_extend_targetentriesvalue_product_factor. pa_b_pvs_extend_targetentriesvalue = pa_q_pvs_extend_targetentriesvalue_product_factor * S ((S (pa_i_pvs_extend_targetentriesvalue_product)) * pa_c_pvs_extend_targetentriesvalue) + (pa_p_pvs_extend_targetentriesvalue_product))) /\ ((((exists pa_h_pvs_extend_targetentriesvalue_product_partial. pa_h_pvs_extend_targetentriesvalue_product_partial + S (pa_r_pvs_extend_targetentriesvalue_product) = S ((S (pa_i_pvs_extend_targetentriesvalue_product)) * pa_v_pvs_extend_targetentriesvalue_product)) /\ exists pa_q_pvs_extend_targetentriesvalue_product_partial. pa_u_pvs_extend_targetentriesvalue_product = pa_q_pvs_extend_targetentriesvalue_product_partial * S ((S (pa_i_pvs_extend_targetentriesvalue_product)) * pa_v_pvs_extend_targetentriesvalue_product) + (pa_r_pvs_extend_targetentriesvalue_product))) /\ ((((exists pa_h_pvs_extend_targetentriesvalue_product_successor. pa_h_pvs_extend_targetentriesvalue_product_successor + S (pa_s_pvs_extend_targetentriesvalue_product) = S ((S (S pa_i_pvs_extend_targetentriesvalue_product)) * pa_v_pvs_extend_targetentriesvalue_product)) /\ exists pa_q_pvs_extend_targetentriesvalue_product_successor. pa_u_pvs_extend_targetentriesvalue_product = pa_q_pvs_extend_targetentriesvalue_product_successor * S ((S (S pa_i_pvs_extend_targetentriesvalue_product)) * pa_v_pvs_extend_targetentriesvalue_product) + (pa_s_pvs_extend_targetentriesvalue_product))) /\ pa_s_pvs_extend_targetentriesvalue_product = pa_r_pvs_extend_targetentriesvalue_product * pa_p_pvs_extend_targetentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_extend_targetcover. (~((pvs_divisor_extend_targetcover) = 1) /\ forall pvs_left_extend_targetcoverprime pvs_right_extend_targetcoverprime. (pvs_divisor_extend_targetcover) = pvs_left_extend_targetcoverprime * pvs_right_extend_targetcoverprime -> pvs_left_extend_targetcoverprime = 1 \/ pvs_right_extend_targetcoverprime = 1) -> (exists pvs_factor_extend_targetcoverdivides. (n) = (pvs_divisor_extend_targetcover) * pvs_factor_extend_targetcoverdivides) -> exists pvs_position_extend_targetcover. (exists pvs_gap_extend_targetcoverbound. pvs_gap_extend_targetcoverbound + S (pvs_position_extend_targetcover) = (S l)) /\ (((exists ff_h_pvs_extend_targetcoverentry. ff_h_pvs_extend_targetcoverentry + S (pvs_divisor_extend_targetcover) = S ((S (pvs_position_extend_targetcover)) * qc)) /\ exists ff_q_pvs_extend_targetcoverentry. qb = ff_q_pvs_extend_targetcoverentry * S ((S (pvs_position_extend_targetcover)) * qc) + (pvs_divisor_extend_targetcover)))) /\ (exists ff_u_pvs_extend_targetproduct ff_v_pvs_extend_targetproduct. ((((exists ff_h_pvs_extend_targetproduct_start. ff_h_pvs_extend_targetproduct_start + S (1) = S ((S (0)) * ff_v_pvs_extend_targetproduct)) /\ exists ff_q_pvs_extend_targetproduct_start. ff_u_pvs_extend_targetproduct = ff_q_pvs_extend_targetproduct_start * S ((S (0)) * ff_v_pvs_extend_targetproduct) + (1))) /\ ((((exists ff_h_pvs_extend_targetproduct_terminal. ff_h_pvs_extend_targetproduct_terminal + S (n) = S ((S (S l)) * ff_v_pvs_extend_targetproduct)) /\ exists ff_q_pvs_extend_targetproduct_terminal. ff_u_pvs_extend_targetproduct = ff_q_pvs_extend_targetproduct_terminal * S ((S (S l)) * ff_v_pvs_extend_targetproduct) + (n))) /\ forall ff_i_pvs_extend_targetproduct. (exists ff_lt_pvs_extend_targetproduct_bound. ff_lt_pvs_extend_targetproduct_bound + S ff_i_pvs_extend_targetproduct = S l) -> exists ff_p_pvs_extend_targetproduct ff_r_pvs_extend_targetproduct ff_s_pvs_extend_targetproduct. ((((exists ff_h_pvs_extend_targetproduct_factor. ff_h_pvs_extend_targetproduct_factor + S (ff_p_pvs_extend_targetproduct) = S ((S (ff_i_pvs_extend_targetproduct)) * wc)) /\ exists ff_q_pvs_extend_targetproduct_factor. wb = ff_q_pvs_extend_targetproduct_factor * S ((S (ff_i_pvs_extend_targetproduct)) * wc) + (ff_p_pvs_extend_targetproduct))) /\ ((((exists ff_h_pvs_extend_targetproduct_partial. ff_h_pvs_extend_targetproduct_partial + S (ff_r_pvs_extend_targetproduct) = S ((S (ff_i_pvs_extend_targetproduct)) * ff_v_pvs_extend_targetproduct)) /\ exists ff_q_pvs_extend_targetproduct_partial. ff_u_pvs_extend_targetproduct = ff_q_pvs_extend_targetproduct_partial * S ((S (ff_i_pvs_extend_targetproduct)) * ff_v_pvs_extend_targetproduct) + (ff_r_pvs_extend_targetproduct))) /\ ((((exists ff_h_pvs_extend_targetproduct_successor. ff_h_pvs_extend_targetproduct_successor + S (ff_s_pvs_extend_targetproduct) = S ((S (S ff_i_pvs_extend_targetproduct)) * ff_v_pvs_extend_targetproduct)) /\ exists ff_q_pvs_extend_targetproduct_successor. ff_u_pvs_extend_targetproduct = ff_q_pvs_extend_targetproduct_successor * S ((S (S ff_i_pvs_extend_targetproduct)) * ff_v_pvs_extend_targetproduct) + (ff_s_pvs_extend_targetproduct))) /\ ff_s_pvs_extend_targetproduct = ff_r_pvs_extend_targetproduct * ff_p_pvs_extend_targetproduct))))))))))))))