prime_support_exponent_gcd_divisor_criterion

forall n pb pc eb ec vb vc l g k. (((~((n) = 0)) /\ (((forall pfp_i_pvs_criterion_supportdistinct pfp_j_pvs_criterion_supportdistinct pfp_a_pvs_criterion_supportdistinct. (exists pfp_gap_pvs_criterion_supportdistinctfirst. pfp_gap_pvs_criterion_supportdistinctfirst + S (pfp_i_pvs_criterion_supportdistinct) = (l)) -> (exists pfp_gap_pvs_criterion_supportdistinctsecond. pfp_gap_pvs_criterion_supportdistinctsecond + S (pfp_j_pvs_criterion_supportdistinct) = (l)) -> (((exists ff_h_pfp_pvs_criterion_supportdistinctleft. ff_h_pfp_pvs_criterion_supportdistinctleft + S (pfp_a_pvs_criterion_supportdistinct) = S ((S (pfp_i_pvs_criterion_supportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_criterion_supportdistinctleft. pb = ff_q_pfp_pvs_criterion_supportdistinctleft * S ((S (pfp_i_pvs_criterion_supportdistinct)) * pc) + (pfp_a_pvs_criterion_supportdistinct))) -> (((exists ff_h_pfp_pvs_criterion_supportdistinctright. ff_h_pfp_pvs_criterion_supportdistinctright + S (pfp_a_pvs_criterion_supportdistinct) = S ((S (pfp_j_pvs_criterion_supportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_criterion_supportdistinctright. pb = ff_q_pfp_pvs_criterion_supportdistinctright * S ((S (pfp_j_pvs_criterion_supportdistinct)) * pc) + (pfp_a_pvs_criterion_supportdistinct))) -> pfp_i_pvs_criterion_supportdistinct = pfp_j_pvs_criterion_supportdistinct) /\ (((forall pvs_index_criterion_supportentries. (exists pvs_gap_criterion_supportentriesindex. pvs_gap_criterion_supportentriesindex + S (pvs_index_criterion_supportentries) = (l)) -> exists pvs_prime_criterion_supportentries pvs_exponent_criterion_supportentries pvs_power_criterion_supportentries. (((((exists ff_h_pvs_criterion_supportentriesprime. ff_h_pvs_criterion_supportentriesprime + S (pvs_prime_criterion_supportentries) = S ((S (pvs_index_criterion_supportentries)) * pc)) /\ exists ff_q_pvs_criterion_supportentriesprime. pb = ff_q_pvs_criterion_supportentriesprime * S ((S (pvs_index_criterion_supportentries)) * pc) + (pvs_prime_criterion_supportentries))) /\ (((((exists ff_h_pvs_criterion_supportentriesexponent. ff_h_pvs_criterion_supportentriesexponent + S (pvs_exponent_criterion_supportentries) = S ((S (pvs_index_criterion_supportentries)) * ec)) /\ exists ff_q_pvs_criterion_supportentriesexponent. eb = ff_q_pvs_criterion_supportentriesexponent * S ((S (pvs_index_criterion_supportentries)) * ec) + (pvs_exponent_criterion_supportentries))) /\ (((((exists ff_h_pvs_criterion_supportentriespower. ff_h_pvs_criterion_supportentriespower + S (pvs_power_criterion_supportentries) = S ((S (pvs_index_criterion_supportentries)) * vc)) /\ exists ff_q_pvs_criterion_supportentriespower. vb = ff_q_pvs_criterion_supportentriespower * S ((S (pvs_index_criterion_supportentries)) * vc) + (pvs_power_criterion_supportentries))) /\ (((~((pvs_prime_criterion_supportentries) = 1) /\ forall pvs_left_criterion_supportentriesdomain pvs_right_criterion_supportentriesdomain. (pvs_prime_criterion_supportentries) = pvs_left_criterion_supportentriesdomain * pvs_right_criterion_supportentriesdomain -> pvs_left_criterion_supportentriesdomain = 1 \/ pvs_right_criterion_supportentriesdomain = 1) /\ (((~(pvs_exponent_criterion_supportentries = 0)) /\ (((((exists bpd_gap_pvs_criterion_supportentriesvaluation_selected_bound. bpd_gap_pvs_criterion_supportentriesvaluation_selected_bound + (pvs_exponent_criterion_supportentries) = (n)) /\ (exists bpvi_result_pvs_criterion_supportentriesvaluation_selected. ((exists bpvi_b_pvs_criterion_supportentriesvaluation_selected_power bpvi_c_pvs_criterion_supportentriesvaluation_selected_power. ((forall bpvi_i_pvs_criterion_supportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_criterion_supportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_criterion_supportentriesvaluation_selected_power + S bpvi_i_pvs_criterion_supportentriesvaluation_selected_power = pvs_exponent_criterion_supportentries) -> (((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_repeat. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_repeat + S (pvs_prime_criterion_supportentries) = S ((S (bpvi_i_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_repeat. bpvi_b_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_selected_power) + (pvs_prime_criterion_supportentries)))) /\ (exists bpvi_u_pvs_criterion_supportentriesvaluation_selected_power bpvi_v_pvs_criterion_supportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_start. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_start. bpvi_u_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_terminal. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_criterion_supportentriesvaluation_selected) = S ((S (pvs_exponent_criterion_supportentries)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_terminal. bpvi_u_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_criterion_supportentries)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power) + (bpvi_result_pvs_criterion_supportentriesvaluation_selected))) /\ forall bpvi_j_pvs_criterion_supportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_criterion_supportentriesvaluation_selected_power. bpvi_product_gap_pvs_criterion_supportentriesvaluation_selected_power + S bpvi_j_pvs_criterion_supportentriesvaluation_selected_power = pvs_exponent_criterion_supportentries) -> exists bpvi_factor_pvs_criterion_supportentriesvaluation_selected_power bpvi_partial_pvs_criterion_supportentriesvaluation_selected_power bpvi_successor_pvs_criterion_supportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_factor. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_criterion_supportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_factor. bpvi_b_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_selected_power) + (bpvi_factor_pvs_criterion_supportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_partial. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_criterion_supportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_partial. bpvi_u_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power) + (bpvi_partial_pvs_criterion_supportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_successor. bpvi_h_pvs_criterion_supportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_criterion_supportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_successor. bpvi_u_pvs_criterion_supportentriesvaluation_selected_power = bpvi_q_pvs_criterion_supportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_criterion_supportentriesvaluation_selected_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_selected_power) + (bpvi_successor_pvs_criterion_supportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_criterion_supportentriesvaluation_selected_power = bpvi_partial_pvs_criterion_supportentriesvaluation_selected_power * bpvi_factor_pvs_criterion_supportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_supportentriesvaluation_selected. n = bpvi_result_pvs_criterion_supportentriesvaluation_selected * bpvi_divisor_factor_pvs_criterion_supportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_criterion_supportentriesvaluation. (exists bpd_gap_pvs_criterion_supportentriesvaluation_candidate_bound. bpd_gap_pvs_criterion_supportentriesvaluation_candidate_bound + (bpd_candidate_pvs_criterion_supportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_criterion_supportentriesvaluation_candidate. ((exists bpvi_b_pvs_criterion_supportentriesvaluation_candidate_power bpvi_c_pvs_criterion_supportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_criterion_supportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_criterion_supportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_criterion_supportentriesvaluation_candidate_power + S bpvi_i_pvs_criterion_supportentriesvaluation_candidate_power = bpd_candidate_pvs_criterion_supportentriesvaluation) -> (((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_repeat + S (pvs_prime_criterion_supportentries) = S ((S (bpvi_i_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_candidate_power) + (pvs_prime_criterion_supportentries)))) /\ (exists bpvi_u_pvs_criterion_supportentriesvaluation_candidate_power bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_start. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_start. bpvi_u_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_criterion_supportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_criterion_supportentriesvaluation)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_criterion_supportentriesvaluation)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power) + (bpvi_result_pvs_criterion_supportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_criterion_supportentriesvaluation_candidate_power. bpvi_product_gap_pvs_criterion_supportentriesvaluation_candidate_power + S bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power = bpd_candidate_pvs_criterion_supportentriesvaluation) -> exists bpvi_factor_pvs_criterion_supportentriesvaluation_candidate_power bpvi_partial_pvs_criterion_supportentriesvaluation_candidate_power bpvi_successor_pvs_criterion_supportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_factor. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_criterion_supportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_factor. bpvi_b_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_c_pvs_criterion_supportentriesvaluation_candidate_power) + (bpvi_factor_pvs_criterion_supportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_partial. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_criterion_supportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_partial. bpvi_u_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power) + (bpvi_partial_pvs_criterion_supportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_successor. bpvi_h_pvs_criterion_supportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_criterion_supportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_successor. bpvi_u_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_q_pvs_criterion_supportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_criterion_supportentriesvaluation_candidate_power)) * bpvi_v_pvs_criterion_supportentriesvaluation_candidate_power) + (bpvi_successor_pvs_criterion_supportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_criterion_supportentriesvaluation_candidate_power = bpvi_partial_pvs_criterion_supportentriesvaluation_candidate_power * bpvi_factor_pvs_criterion_supportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_supportentriesvaluation_candidate. n = bpvi_result_pvs_criterion_supportentriesvaluation_candidate * bpvi_divisor_factor_pvs_criterion_supportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_criterion_supportentriesvaluation_maximal. bpd_gap_pvs_criterion_supportentriesvaluation_maximal + (bpd_candidate_pvs_criterion_supportentriesvaluation) = (pvs_exponent_criterion_supportentries))) /\ (exists pa_b_pvs_criterion_supportentriesvalue pa_c_pvs_criterion_supportentriesvalue. ((forall pa_i_pvs_criterion_supportentriesvalue_repeat. (exists pa_lt_pvs_criterion_supportentriesvalue_repeat_bound. pa_lt_pvs_criterion_supportentriesvalue_repeat_bound + S pa_i_pvs_criterion_supportentriesvalue_repeat = pvs_exponent_criterion_supportentries) -> (((exists pa_h_pvs_criterion_supportentriesvalue_repeat_decoded. pa_h_pvs_criterion_supportentriesvalue_repeat_decoded + S (pvs_prime_criterion_supportentries) = S ((S (pa_i_pvs_criterion_supportentriesvalue_repeat)) * pa_c_pvs_criterion_supportentriesvalue)) /\ exists pa_q_pvs_criterion_supportentriesvalue_repeat_decoded. pa_b_pvs_criterion_supportentriesvalue = pa_q_pvs_criterion_supportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_criterion_supportentriesvalue_repeat)) * pa_c_pvs_criterion_supportentriesvalue) + (pvs_prime_criterion_supportentries)))) /\ (exists pa_u_pvs_criterion_supportentriesvalue_product pa_v_pvs_criterion_supportentriesvalue_product. ((((exists pa_h_pvs_criterion_supportentriesvalue_product_start. pa_h_pvs_criterion_supportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_criterion_supportentriesvalue_product)) /\ exists pa_q_pvs_criterion_supportentriesvalue_product_start. pa_u_pvs_criterion_supportentriesvalue_product = pa_q_pvs_criterion_supportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_criterion_supportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_criterion_supportentriesvalue_product_terminal. pa_h_pvs_criterion_supportentriesvalue_product_terminal + S (pvs_power_criterion_supportentries) = S ((S (pvs_exponent_criterion_supportentries)) * pa_v_pvs_criterion_supportentriesvalue_product)) /\ exists pa_q_pvs_criterion_supportentriesvalue_product_terminal. pa_u_pvs_criterion_supportentriesvalue_product = pa_q_pvs_criterion_supportentriesvalue_product_terminal * S ((S (pvs_exponent_criterion_supportentries)) * pa_v_pvs_criterion_supportentriesvalue_product) + (pvs_power_criterion_supportentries))) /\ forall pa_i_pvs_criterion_supportentriesvalue_product. (exists pa_lt_pvs_criterion_supportentriesvalue_product_bound. pa_lt_pvs_criterion_supportentriesvalue_product_bound + S pa_i_pvs_criterion_supportentriesvalue_product = pvs_exponent_criterion_supportentries) -> exists pa_p_pvs_criterion_supportentriesvalue_product pa_r_pvs_criterion_supportentriesvalue_product pa_s_pvs_criterion_supportentriesvalue_product. ((((exists pa_h_pvs_criterion_supportentriesvalue_product_factor. pa_h_pvs_criterion_supportentriesvalue_product_factor + S (pa_p_pvs_criterion_supportentriesvalue_product) = S ((S (pa_i_pvs_criterion_supportentriesvalue_product)) * pa_c_pvs_criterion_supportentriesvalue)) /\ exists pa_q_pvs_criterion_supportentriesvalue_product_factor. pa_b_pvs_criterion_supportentriesvalue = pa_q_pvs_criterion_supportentriesvalue_product_factor * S ((S (pa_i_pvs_criterion_supportentriesvalue_product)) * pa_c_pvs_criterion_supportentriesvalue) + (pa_p_pvs_criterion_supportentriesvalue_product))) /\ ((((exists pa_h_pvs_criterion_supportentriesvalue_product_partial. pa_h_pvs_criterion_supportentriesvalue_product_partial + S (pa_r_pvs_criterion_supportentriesvalue_product) = S ((S (pa_i_pvs_criterion_supportentriesvalue_product)) * pa_v_pvs_criterion_supportentriesvalue_product)) /\ exists pa_q_pvs_criterion_supportentriesvalue_product_partial. pa_u_pvs_criterion_supportentriesvalue_product = pa_q_pvs_criterion_supportentriesvalue_product_partial * S ((S (pa_i_pvs_criterion_supportentriesvalue_product)) * pa_v_pvs_criterion_supportentriesvalue_product) + (pa_r_pvs_criterion_supportentriesvalue_product))) /\ ((((exists pa_h_pvs_criterion_supportentriesvalue_product_successor. pa_h_pvs_criterion_supportentriesvalue_product_successor + S (pa_s_pvs_criterion_supportentriesvalue_product) = S ((S (S pa_i_pvs_criterion_supportentriesvalue_product)) * pa_v_pvs_criterion_supportentriesvalue_product)) /\ exists pa_q_pvs_criterion_supportentriesvalue_product_successor. pa_u_pvs_criterion_supportentriesvalue_product = pa_q_pvs_criterion_supportentriesvalue_product_successor * S ((S (S pa_i_pvs_criterion_supportentriesvalue_product)) * pa_v_pvs_criterion_supportentriesvalue_product) + (pa_s_pvs_criterion_supportentriesvalue_product))) /\ pa_s_pvs_criterion_supportentriesvalue_product = pa_r_pvs_criterion_supportentriesvalue_product * pa_p_pvs_criterion_supportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_criterion_supportcover. (~((pvs_divisor_criterion_supportcover) = 1) /\ forall pvs_left_criterion_supportcoverprime pvs_right_criterion_supportcoverprime. (pvs_divisor_criterion_supportcover) = pvs_left_criterion_supportcoverprime * pvs_right_criterion_supportcoverprime -> pvs_left_criterion_supportcoverprime = 1 \/ pvs_right_criterion_supportcoverprime = 1) -> (exists pvs_factor_criterion_supportcoverdivides. (n) = (pvs_divisor_criterion_supportcover) * pvs_factor_criterion_supportcoverdivides) -> exists pvs_position_criterion_supportcover. (exists pvs_gap_criterion_supportcoverbound. pvs_gap_criterion_supportcoverbound + S (pvs_position_criterion_supportcover) = (l)) /\ (((exists ff_h_pvs_criterion_supportcoverentry. ff_h_pvs_criterion_supportcoverentry + S (pvs_divisor_criterion_supportcover) = S ((S (pvs_position_criterion_supportcover)) * pc)) /\ exists ff_q_pvs_criterion_supportcoverentry. pb = ff_q_pvs_criterion_supportcoverentry * S ((S (pvs_position_criterion_supportcover)) * pc) + (pvs_divisor_criterion_supportcover)))) /\ (exists ff_u_pvs_criterion_supportproduct ff_v_pvs_criterion_supportproduct. ((((exists ff_h_pvs_criterion_supportproduct_start. ff_h_pvs_criterion_supportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_criterion_supportproduct)) /\ exists ff_q_pvs_criterion_supportproduct_start. ff_u_pvs_criterion_supportproduct = ff_q_pvs_criterion_supportproduct_start * S ((S (0)) * ff_v_pvs_criterion_supportproduct) + (1))) /\ ((((exists ff_h_pvs_criterion_supportproduct_terminal. ff_h_pvs_criterion_supportproduct_terminal + S (n) = S ((S (l)) * ff_v_pvs_criterion_supportproduct)) /\ exists ff_q_pvs_criterion_supportproduct_terminal. ff_u_pvs_criterion_supportproduct = ff_q_pvs_criterion_supportproduct_terminal * S ((S (l)) * ff_v_pvs_criterion_supportproduct) + (n))) /\ forall ff_i_pvs_criterion_supportproduct. (exists ff_lt_pvs_criterion_supportproduct_bound. ff_lt_pvs_criterion_supportproduct_bound + S ff_i_pvs_criterion_supportproduct = l) -> exists ff_p_pvs_criterion_supportproduct ff_r_pvs_criterion_supportproduct ff_s_pvs_criterion_supportproduct. ((((exists ff_h_pvs_criterion_supportproduct_factor. ff_h_pvs_criterion_supportproduct_factor + S (ff_p_pvs_criterion_supportproduct) = S ((S (ff_i_pvs_criterion_supportproduct)) * vc)) /\ exists ff_q_pvs_criterion_supportproduct_factor. vb = ff_q_pvs_criterion_supportproduct_factor * S ((S (ff_i_pvs_criterion_supportproduct)) * vc) + (ff_p_pvs_criterion_supportproduct))) /\ ((((exists ff_h_pvs_criterion_supportproduct_partial. ff_h_pvs_criterion_supportproduct_partial + S (ff_r_pvs_criterion_supportproduct) = S ((S (ff_i_pvs_criterion_supportproduct)) * ff_v_pvs_criterion_supportproduct)) /\ exists ff_q_pvs_criterion_supportproduct_partial. ff_u_pvs_criterion_supportproduct = ff_q_pvs_criterion_supportproduct_partial * S ((S (ff_i_pvs_criterion_supportproduct)) * ff_v_pvs_criterion_supportproduct) + (ff_r_pvs_criterion_supportproduct))) /\ ((((exists ff_h_pvs_criterion_supportproduct_successor. ff_h_pvs_criterion_supportproduct_successor + S (ff_s_pvs_criterion_supportproduct) = S ((S (S ff_i_pvs_criterion_supportproduct)) * ff_v_pvs_criterion_supportproduct)) /\ exists ff_q_pvs_criterion_supportproduct_successor. ff_u_pvs_criterion_supportproduct = ff_q_pvs_criterion_supportproduct_successor * S ((S (S ff_i_pvs_criterion_supportproduct)) * ff_v_pvs_criterion_supportproduct) + (ff_s_pvs_criterion_supportproduct))) /\ ff_s_pvs_criterion_supportproduct = ff_r_pvs_criterion_supportproduct * ff_p_pvs_criterion_supportproduct)))))))))))))) -> (((forall ppf_index_criterion_gcdcommon ppf_entry_criterion_gcdcommon. (exists pvs_gap_criterion_gcdcommonbound. pvs_gap_criterion_gcdcommonbound + S (ppf_index_criterion_gcdcommon) = (l)) -> (((exists ff_h_pvs_criterion_gcdcommonentry. ff_h_pvs_criterion_gcdcommonentry + S (ppf_entry_criterion_gcdcommon) = S ((S (ppf_index_criterion_gcdcommon)) * ec)) /\ exists ff_q_pvs_criterion_gcdcommonentry. eb = ff_q_pvs_criterion_gcdcommonentry * S ((S (ppf_index_criterion_gcdcommon)) * ec) + (ppf_entry_criterion_gcdcommon))) -> (exists pvs_factor_criterion_gcdcommondivisor. (ppf_entry_criterion_gcdcommon) = (g) * pvs_factor_criterion_gcdcommondivisor)) /\ (forall ppf_common_criterion_gcd. (forall ppf_index_criterion_gcdother ppf_entry_criterion_gcdother. (exists pvs_gap_criterion_gcdotherbound. pvs_gap_criterion_gcdotherbound + S (ppf_index_criterion_gcdother) = (l)) -> (((exists ff_h_pvs_criterion_gcdotherentry. ff_h_pvs_criterion_gcdotherentry + S (ppf_entry_criterion_gcdother) = S ((S (ppf_index_criterion_gcdother)) * ec)) /\ exists ff_q_pvs_criterion_gcdotherentry. eb = ff_q_pvs_criterion_gcdotherentry * S ((S (ppf_index_criterion_gcdother)) * ec) + (ppf_entry_criterion_gcdother))) -> (exists pvs_factor_criterion_gcdotherdivisor. (ppf_entry_criterion_gcdother) = (ppf_common_criterion_gcd) * pvs_factor_criterion_gcdotherdivisor)) -> (exists pvs_factor_criterion_gcdgreatest. (g) = (ppf_common_criterion_gcd) * pvs_factor_criterion_gcdgreatest)))) -> ((exists pvs_factor_criterion_divisor_first. (g) = (k) * pvs_factor_criterion_divisor_first) -> (forall ppf_prime_criterion_all_first ppf_exponent_criterion_all_first. (~((ppf_prime_criterion_all_first) = 1) /\ forall pvs_left_criterion_all_firstdomain pvs_right_criterion_all_firstdomain. (ppf_prime_criterion_all_first) = pvs_left_criterion_all_firstdomain * pvs_right_criterion_all_firstdomain -> pvs_left_criterion_all_firstdomain = 1 \/ pvs_right_criterion_all_firstdomain = 1) -> (((exists bpd_gap_pvs_criterion_all_firstvaluation_selected_bound. bpd_gap_pvs_criterion_all_firstvaluation_selected_bound + (ppf_exponent_criterion_all_first) = (n)) /\ (exists bpvi_result_pvs_criterion_all_firstvaluation_selected. ((exists bpvi_b_pvs_criterion_all_firstvaluation_selected_power bpvi_c_pvs_criterion_all_firstvaluation_selected_power. ((forall bpvi_i_pvs_criterion_all_firstvaluation_selected_power. (exists bpvi_repeat_gap_pvs_criterion_all_firstvaluation_selected_power. bpvi_repeat_gap_pvs_criterion_all_firstvaluation_selected_power + S bpvi_i_pvs_criterion_all_firstvaluation_selected_power = ppf_exponent_criterion_all_first) -> (((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_repeat. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_repeat + S (ppf_prime_criterion_all_first) = S ((S (bpvi_i_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_c_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_repeat. bpvi_b_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_c_pvs_criterion_all_firstvaluation_selected_power) + (ppf_prime_criterion_all_first)))) /\ (exists bpvi_u_pvs_criterion_all_firstvaluation_selected_power bpvi_v_pvs_criterion_all_firstvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_start. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_start. bpvi_u_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_terminal. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_terminal + S (bpvi_result_pvs_criterion_all_firstvaluation_selected) = S ((S (ppf_exponent_criterion_all_first)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_terminal. bpvi_u_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_terminal * S ((S (ppf_exponent_criterion_all_first)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power) + (bpvi_result_pvs_criterion_all_firstvaluation_selected))) /\ forall bpvi_j_pvs_criterion_all_firstvaluation_selected_power. (exists bpvi_product_gap_pvs_criterion_all_firstvaluation_selected_power. bpvi_product_gap_pvs_criterion_all_firstvaluation_selected_power + S bpvi_j_pvs_criterion_all_firstvaluation_selected_power = ppf_exponent_criterion_all_first) -> exists bpvi_factor_pvs_criterion_all_firstvaluation_selected_power bpvi_partial_pvs_criterion_all_firstvaluation_selected_power bpvi_successor_pvs_criterion_all_firstvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_factor. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_factor + S (bpvi_factor_pvs_criterion_all_firstvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_c_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_factor. bpvi_b_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_factor * S ((S (bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_c_pvs_criterion_all_firstvaluation_selected_power) + (bpvi_factor_pvs_criterion_all_firstvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_partial. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_partial + S (bpvi_partial_pvs_criterion_all_firstvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_partial. bpvi_u_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_partial * S ((S (bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power) + (bpvi_partial_pvs_criterion_all_firstvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_selected_power_successor. bpvi_h_pvs_criterion_all_firstvaluation_selected_power_successor + S (bpvi_successor_pvs_criterion_all_firstvaluation_selected_power) = S ((S (S bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_selected_power_successor. bpvi_u_pvs_criterion_all_firstvaluation_selected_power = bpvi_q_pvs_criterion_all_firstvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_criterion_all_firstvaluation_selected_power)) * bpvi_v_pvs_criterion_all_firstvaluation_selected_power) + (bpvi_successor_pvs_criterion_all_firstvaluation_selected_power))) /\ bpvi_successor_pvs_criterion_all_firstvaluation_selected_power = bpvi_partial_pvs_criterion_all_firstvaluation_selected_power * bpvi_factor_pvs_criterion_all_firstvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_all_firstvaluation_selected. n = bpvi_result_pvs_criterion_all_firstvaluation_selected * bpvi_divisor_factor_pvs_criterion_all_firstvaluation_selected))) /\ forall bpd_candidate_pvs_criterion_all_firstvaluation. (exists bpd_gap_pvs_criterion_all_firstvaluation_candidate_bound. bpd_gap_pvs_criterion_all_firstvaluation_candidate_bound + (bpd_candidate_pvs_criterion_all_firstvaluation) = (n)) -> (exists bpvi_result_pvs_criterion_all_firstvaluation_candidate. ((exists bpvi_b_pvs_criterion_all_firstvaluation_candidate_power bpvi_c_pvs_criterion_all_firstvaluation_candidate_power. ((forall bpvi_i_pvs_criterion_all_firstvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_criterion_all_firstvaluation_candidate_power. bpvi_repeat_gap_pvs_criterion_all_firstvaluation_candidate_power + S bpvi_i_pvs_criterion_all_firstvaluation_candidate_power = bpd_candidate_pvs_criterion_all_firstvaluation) -> (((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_repeat. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_repeat + S (ppf_prime_criterion_all_first) = S ((S (bpvi_i_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_repeat. bpvi_b_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_firstvaluation_candidate_power) + (ppf_prime_criterion_all_first)))) /\ (exists bpvi_u_pvs_criterion_all_firstvaluation_candidate_power bpvi_v_pvs_criterion_all_firstvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_start. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_start. bpvi_u_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_terminal. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_terminal + S (bpvi_result_pvs_criterion_all_firstvaluation_candidate) = S ((S (bpd_candidate_pvs_criterion_all_firstvaluation)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_terminal. bpvi_u_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_criterion_all_firstvaluation)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power) + (bpvi_result_pvs_criterion_all_firstvaluation_candidate))) /\ forall bpvi_j_pvs_criterion_all_firstvaluation_candidate_power. (exists bpvi_product_gap_pvs_criterion_all_firstvaluation_candidate_power. bpvi_product_gap_pvs_criterion_all_firstvaluation_candidate_power + S bpvi_j_pvs_criterion_all_firstvaluation_candidate_power = bpd_candidate_pvs_criterion_all_firstvaluation) -> exists bpvi_factor_pvs_criterion_all_firstvaluation_candidate_power bpvi_partial_pvs_criterion_all_firstvaluation_candidate_power bpvi_successor_pvs_criterion_all_firstvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_factor. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_factor + S (bpvi_factor_pvs_criterion_all_firstvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_factor. bpvi_b_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_firstvaluation_candidate_power) + (bpvi_factor_pvs_criterion_all_firstvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_partial. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_partial + S (bpvi_partial_pvs_criterion_all_firstvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_partial. bpvi_u_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power) + (bpvi_partial_pvs_criterion_all_firstvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_successor. bpvi_h_pvs_criterion_all_firstvaluation_candidate_power_successor + S (bpvi_successor_pvs_criterion_all_firstvaluation_candidate_power) = S ((S (S bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_successor. bpvi_u_pvs_criterion_all_firstvaluation_candidate_power = bpvi_q_pvs_criterion_all_firstvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_criterion_all_firstvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_firstvaluation_candidate_power) + (bpvi_successor_pvs_criterion_all_firstvaluation_candidate_power))) /\ bpvi_successor_pvs_criterion_all_firstvaluation_candidate_power = bpvi_partial_pvs_criterion_all_firstvaluation_candidate_power * bpvi_factor_pvs_criterion_all_firstvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_all_firstvaluation_candidate. n = bpvi_result_pvs_criterion_all_firstvaluation_candidate * bpvi_divisor_factor_pvs_criterion_all_firstvaluation_candidate)) -> (exists bpd_gap_pvs_criterion_all_firstvaluation_maximal. bpd_gap_pvs_criterion_all_firstvaluation_maximal + (bpd_candidate_pvs_criterion_all_firstvaluation) = (ppf_exponent_criterion_all_first))) -> (exists pvs_factor_criterion_all_firstdivides. (ppf_exponent_criterion_all_first) = (k) * pvs_factor_criterion_all_firstdivides))) /\ ((forall ppf_prime_criterion_all_second ppf_exponent_criterion_all_second. (~((ppf_prime_criterion_all_second) = 1) /\ forall pvs_left_criterion_all_seconddomain pvs_right_criterion_all_seconddomain. (ppf_prime_criterion_all_second) = pvs_left_criterion_all_seconddomain * pvs_right_criterion_all_seconddomain -> pvs_left_criterion_all_seconddomain = 1 \/ pvs_right_criterion_all_seconddomain = 1) -> (((exists bpd_gap_pvs_criterion_all_secondvaluation_selected_bound. bpd_gap_pvs_criterion_all_secondvaluation_selected_bound + (ppf_exponent_criterion_all_second) = (n)) /\ (exists bpvi_result_pvs_criterion_all_secondvaluation_selected. ((exists bpvi_b_pvs_criterion_all_secondvaluation_selected_power bpvi_c_pvs_criterion_all_secondvaluation_selected_power. ((forall bpvi_i_pvs_criterion_all_secondvaluation_selected_power. (exists bpvi_repeat_gap_pvs_criterion_all_secondvaluation_selected_power. bpvi_repeat_gap_pvs_criterion_all_secondvaluation_selected_power + S bpvi_i_pvs_criterion_all_secondvaluation_selected_power = ppf_exponent_criterion_all_second) -> (((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_repeat. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_repeat + S (ppf_prime_criterion_all_second) = S ((S (bpvi_i_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_c_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_repeat. bpvi_b_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_c_pvs_criterion_all_secondvaluation_selected_power) + (ppf_prime_criterion_all_second)))) /\ (exists bpvi_u_pvs_criterion_all_secondvaluation_selected_power bpvi_v_pvs_criterion_all_secondvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_start. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_start. bpvi_u_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_terminal. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_terminal + S (bpvi_result_pvs_criterion_all_secondvaluation_selected) = S ((S (ppf_exponent_criterion_all_second)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_terminal. bpvi_u_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_terminal * S ((S (ppf_exponent_criterion_all_second)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power) + (bpvi_result_pvs_criterion_all_secondvaluation_selected))) /\ forall bpvi_j_pvs_criterion_all_secondvaluation_selected_power. (exists bpvi_product_gap_pvs_criterion_all_secondvaluation_selected_power. bpvi_product_gap_pvs_criterion_all_secondvaluation_selected_power + S bpvi_j_pvs_criterion_all_secondvaluation_selected_power = ppf_exponent_criterion_all_second) -> exists bpvi_factor_pvs_criterion_all_secondvaluation_selected_power bpvi_partial_pvs_criterion_all_secondvaluation_selected_power bpvi_successor_pvs_criterion_all_secondvaluation_selected_power. ((((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_factor. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_factor + S (bpvi_factor_pvs_criterion_all_secondvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_c_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_factor. bpvi_b_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_factor * S ((S (bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_c_pvs_criterion_all_secondvaluation_selected_power) + (bpvi_factor_pvs_criterion_all_secondvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_partial. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_partial + S (bpvi_partial_pvs_criterion_all_secondvaluation_selected_power) = S ((S (bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_partial. bpvi_u_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_partial * S ((S (bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power) + (bpvi_partial_pvs_criterion_all_secondvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_selected_power_successor. bpvi_h_pvs_criterion_all_secondvaluation_selected_power_successor + S (bpvi_successor_pvs_criterion_all_secondvaluation_selected_power) = S ((S (S bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_selected_power_successor. bpvi_u_pvs_criterion_all_secondvaluation_selected_power = bpvi_q_pvs_criterion_all_secondvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_criterion_all_secondvaluation_selected_power)) * bpvi_v_pvs_criterion_all_secondvaluation_selected_power) + (bpvi_successor_pvs_criterion_all_secondvaluation_selected_power))) /\ bpvi_successor_pvs_criterion_all_secondvaluation_selected_power = bpvi_partial_pvs_criterion_all_secondvaluation_selected_power * bpvi_factor_pvs_criterion_all_secondvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_all_secondvaluation_selected. n = bpvi_result_pvs_criterion_all_secondvaluation_selected * bpvi_divisor_factor_pvs_criterion_all_secondvaluation_selected))) /\ forall bpd_candidate_pvs_criterion_all_secondvaluation. (exists bpd_gap_pvs_criterion_all_secondvaluation_candidate_bound. bpd_gap_pvs_criterion_all_secondvaluation_candidate_bound + (bpd_candidate_pvs_criterion_all_secondvaluation) = (n)) -> (exists bpvi_result_pvs_criterion_all_secondvaluation_candidate. ((exists bpvi_b_pvs_criterion_all_secondvaluation_candidate_power bpvi_c_pvs_criterion_all_secondvaluation_candidate_power. ((forall bpvi_i_pvs_criterion_all_secondvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_criterion_all_secondvaluation_candidate_power. bpvi_repeat_gap_pvs_criterion_all_secondvaluation_candidate_power + S bpvi_i_pvs_criterion_all_secondvaluation_candidate_power = bpd_candidate_pvs_criterion_all_secondvaluation) -> (((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_repeat. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_repeat + S (ppf_prime_criterion_all_second) = S ((S (bpvi_i_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_repeat. bpvi_b_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_secondvaluation_candidate_power) + (ppf_prime_criterion_all_second)))) /\ (exists bpvi_u_pvs_criterion_all_secondvaluation_candidate_power bpvi_v_pvs_criterion_all_secondvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_start. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_start. bpvi_u_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_terminal. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_terminal + S (bpvi_result_pvs_criterion_all_secondvaluation_candidate) = S ((S (bpd_candidate_pvs_criterion_all_secondvaluation)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_terminal. bpvi_u_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_criterion_all_secondvaluation)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power) + (bpvi_result_pvs_criterion_all_secondvaluation_candidate))) /\ forall bpvi_j_pvs_criterion_all_secondvaluation_candidate_power. (exists bpvi_product_gap_pvs_criterion_all_secondvaluation_candidate_power. bpvi_product_gap_pvs_criterion_all_secondvaluation_candidate_power + S bpvi_j_pvs_criterion_all_secondvaluation_candidate_power = bpd_candidate_pvs_criterion_all_secondvaluation) -> exists bpvi_factor_pvs_criterion_all_secondvaluation_candidate_power bpvi_partial_pvs_criterion_all_secondvaluation_candidate_power bpvi_successor_pvs_criterion_all_secondvaluation_candidate_power. ((((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_factor. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_factor + S (bpvi_factor_pvs_criterion_all_secondvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_factor. bpvi_b_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_c_pvs_criterion_all_secondvaluation_candidate_power) + (bpvi_factor_pvs_criterion_all_secondvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_partial. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_partial + S (bpvi_partial_pvs_criterion_all_secondvaluation_candidate_power) = S ((S (bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_partial. bpvi_u_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power) + (bpvi_partial_pvs_criterion_all_secondvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_successor. bpvi_h_pvs_criterion_all_secondvaluation_candidate_power_successor + S (bpvi_successor_pvs_criterion_all_secondvaluation_candidate_power) = S ((S (S bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power)) /\ exists bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_successor. bpvi_u_pvs_criterion_all_secondvaluation_candidate_power = bpvi_q_pvs_criterion_all_secondvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_criterion_all_secondvaluation_candidate_power)) * bpvi_v_pvs_criterion_all_secondvaluation_candidate_power) + (bpvi_successor_pvs_criterion_all_secondvaluation_candidate_power))) /\ bpvi_successor_pvs_criterion_all_secondvaluation_candidate_power = bpvi_partial_pvs_criterion_all_secondvaluation_candidate_power * bpvi_factor_pvs_criterion_all_secondvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_criterion_all_secondvaluation_candidate. n = bpvi_result_pvs_criterion_all_secondvaluation_candidate * bpvi_divisor_factor_pvs_criterion_all_secondvaluation_candidate)) -> (exists bpd_gap_pvs_criterion_all_secondvaluation_maximal. bpd_gap_pvs_criterion_all_secondvaluation_maximal + (bpd_candidate_pvs_criterion_all_secondvaluation) = (ppf_exponent_criterion_all_second))) -> (exists pvs_factor_criterion_all_seconddivides. (ppf_exponent_criterion_all_second) = (k) * pvs_factor_criterion_all_seconddivides)) -> (exists pvs_factor_criterion_divisor_second. (g) = (k) * pvs_factor_criterion_divisor_second))