prime_valuation_divisibility_cofactor

Exact expanded first-order arithmetic statement

forall n k p e P u. (~((p) = 1) /\ forall pvs_left_cofactor_base pvs_right_cofactor_base. (p) = pvs_left_cofactor_base * pvs_right_cofactor_base -> pvs_left_cofactor_base = 1 \/ pvs_right_cofactor_base = 1) -> ~(u = 0) -> n = P * u -> (exists pa_b_pvs_cofactor_power pa_c_pvs_cofactor_power. ((forall pa_i_pvs_cofactor_power_repeat. (exists pa_lt_pvs_cofactor_power_repeat_bound. pa_lt_pvs_cofactor_power_repeat_bound + S pa_i_pvs_cofactor_power_repeat = e) -> (((exists pa_h_pvs_cofactor_power_repeat_decoded. pa_h_pvs_cofactor_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_cofactor_power_repeat)) * pa_c_pvs_cofactor_power)) /\ exists pa_q_pvs_cofactor_power_repeat_decoded. pa_b_pvs_cofactor_power = pa_q_pvs_cofactor_power_repeat_decoded * S ((S (pa_i_pvs_cofactor_power_repeat)) * pa_c_pvs_cofactor_power) + (p)))) /\ (exists pa_u_pvs_cofactor_power_product pa_v_pvs_cofactor_power_product. ((((exists pa_h_pvs_cofactor_power_product_start. pa_h_pvs_cofactor_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_cofactor_power_product)) /\ exists pa_q_pvs_cofactor_power_product_start. pa_u_pvs_cofactor_power_product = pa_q_pvs_cofactor_power_product_start * S ((S (0)) * pa_v_pvs_cofactor_power_product) + (1))) /\ ((((exists pa_h_pvs_cofactor_power_product_terminal. pa_h_pvs_cofactor_power_product_terminal + S (P) = S ((S (e)) * pa_v_pvs_cofactor_power_product)) /\ exists pa_q_pvs_cofactor_power_product_terminal. pa_u_pvs_cofactor_power_product = pa_q_pvs_cofactor_power_product_terminal * S ((S (e)) * pa_v_pvs_cofactor_power_product) + (P))) /\ forall pa_i_pvs_cofactor_power_product. (exists pa_lt_pvs_cofactor_power_product_bound. pa_lt_pvs_cofactor_power_product_bound + S pa_i_pvs_cofactor_power_product = e) -> exists pa_p_pvs_cofactor_power_product pa_r_pvs_cofactor_power_product pa_s_pvs_cofactor_power_product. ((((exists pa_h_pvs_cofactor_power_product_factor. pa_h_pvs_cofactor_power_product_factor + S (pa_p_pvs_cofactor_power_product) = S ((S (pa_i_pvs_cofactor_power_product)) * pa_c_pvs_cofactor_power)) /\ exists pa_q_pvs_cofactor_power_product_factor. pa_b_pvs_cofactor_power = pa_q_pvs_cofactor_power_product_factor * S ((S (pa_i_pvs_cofactor_power_product)) * pa_c_pvs_cofactor_power) + (pa_p_pvs_cofactor_power_product))) /\ ((((exists pa_h_pvs_cofactor_power_product_partial. pa_h_pvs_cofactor_power_product_partial + S (pa_r_pvs_cofactor_power_product) = S ((S (pa_i_pvs_cofactor_power_product)) * pa_v_pvs_cofactor_power_product)) /\ exists pa_q_pvs_cofactor_power_product_partial. pa_u_pvs_cofactor_power_product = pa_q_pvs_cofactor_power_product_partial * S ((S (pa_i_pvs_cofactor_power_product)) * pa_v_pvs_cofactor_power_product) + (pa_r_pvs_cofactor_power_product))) /\ ((((exists pa_h_pvs_cofactor_power_product_successor. pa_h_pvs_cofactor_power_product_successor + S (pa_s_pvs_cofactor_power_product) = S ((S (S pa_i_pvs_cofactor_power_product)) * pa_v_pvs_cofactor_power_product)) /\ exists pa_q_pvs_cofactor_power_product_successor. pa_u_pvs_cofactor_power_product = pa_q_pvs_cofactor_power_product_successor * S ((S (S pa_i_pvs_cofactor_power_product)) * pa_v_pvs_cofactor_power_product) + (pa_s_pvs_cofactor_power_product))) /\ pa_s_pvs_cofactor_power_product = pa_r_pvs_cofactor_power_product * pa_p_pvs_cofactor_power_product)))))))) -> ~(exists pvs_factor_cofactor_fresh. (u) = (p) * pvs_factor_cofactor_fresh) -> (forall ppf_prime_cofactor_source ppf_exponent_cofactor_source. (~((ppf_prime_cofactor_source) = 1) /\ forall pvs_left_cofactor_sourcedomain pvs_right_cofactor_sourcedomain. (ppf_prime_cofactor_source) = pvs_left_cofactor_sourcedomain * pvs_right_cofactor_sourcedomain -> pvs_left_cofactor_sourcedomain = 1 \/ pvs_right_cofactor_sourcedomain = 1) -> (((exists bpd_gap_pvs_cofactor_sourcevaluation_selected_bound. bpd_gap_pvs_cofactor_sourcevaluation_selected_bound + (ppf_exponent_cofactor_source) = (n)) /\ (exists bpvi_result_pvs_cofactor_sourcevaluation_selected. ((exists bpvi_b_pvs_cofactor_sourcevaluation_selected_power bpvi_c_pvs_cofactor_sourcevaluation_selected_power. ((forall bpvi_i_pvs_cofactor_sourcevaluation_selected_power. (exists bpvi_repeat_gap_pvs_cofactor_sourcevaluation_selected_power. bpvi_repeat_gap_pvs_cofactor_sourcevaluation_selected_power + S bpvi_i_pvs_cofactor_sourcevaluation_selected_power = ppf_exponent_cofactor_source) -> (((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_repeat. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_repeat + S (ppf_prime_cofactor_source) = S ((S (bpvi_i_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_c_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_repeat. bpvi_b_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_repeat * S ((S (bpvi_i_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_c_pvs_cofactor_sourcevaluation_selected_power) + (ppf_prime_cofactor_source)))) /\ (exists bpvi_u_pvs_cofactor_sourcevaluation_selected_power bpvi_v_pvs_cofactor_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_start. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_start. bpvi_u_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_terminal. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_terminal + S (bpvi_result_pvs_cofactor_sourcevaluation_selected) = S ((S (ppf_exponent_cofactor_source)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_terminal. bpvi_u_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_terminal * S ((S (ppf_exponent_cofactor_source)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power) + (bpvi_result_pvs_cofactor_sourcevaluation_selected))) /\ forall bpvi_j_pvs_cofactor_sourcevaluation_selected_power. (exists bpvi_product_gap_pvs_cofactor_sourcevaluation_selected_power. bpvi_product_gap_pvs_cofactor_sourcevaluation_selected_power + S bpvi_j_pvs_cofactor_sourcevaluation_selected_power = ppf_exponent_cofactor_source) -> exists bpvi_factor_pvs_cofactor_sourcevaluation_selected_power bpvi_partial_pvs_cofactor_sourcevaluation_selected_power bpvi_successor_pvs_cofactor_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_factor. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_factor + S (bpvi_factor_pvs_cofactor_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_c_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_factor. bpvi_b_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_factor * S ((S (bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_c_pvs_cofactor_sourcevaluation_selected_power) + (bpvi_factor_pvs_cofactor_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_partial. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_partial + S (bpvi_partial_pvs_cofactor_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_partial. bpvi_u_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_partial * S ((S (bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power) + (bpvi_partial_pvs_cofactor_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_selected_power_successor. bpvi_h_pvs_cofactor_sourcevaluation_selected_power_successor + S (bpvi_successor_pvs_cofactor_sourcevaluation_selected_power) = S ((S (S bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_selected_power_successor. bpvi_u_pvs_cofactor_sourcevaluation_selected_power = bpvi_q_pvs_cofactor_sourcevaluation_selected_power_successor * S ((S (S bpvi_j_pvs_cofactor_sourcevaluation_selected_power)) * bpvi_v_pvs_cofactor_sourcevaluation_selected_power) + (bpvi_successor_pvs_cofactor_sourcevaluation_selected_power))) /\ bpvi_successor_pvs_cofactor_sourcevaluation_selected_power = bpvi_partial_pvs_cofactor_sourcevaluation_selected_power * bpvi_factor_pvs_cofactor_sourcevaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_sourcevaluation_selected. n = bpvi_result_pvs_cofactor_sourcevaluation_selected * bpvi_divisor_factor_pvs_cofactor_sourcevaluation_selected))) /\ forall bpd_candidate_pvs_cofactor_sourcevaluation. (exists bpd_gap_pvs_cofactor_sourcevaluation_candidate_bound. bpd_gap_pvs_cofactor_sourcevaluation_candidate_bound + (bpd_candidate_pvs_cofactor_sourcevaluation) = (n)) -> (exists bpvi_result_pvs_cofactor_sourcevaluation_candidate. ((exists bpvi_b_pvs_cofactor_sourcevaluation_candidate_power bpvi_c_pvs_cofactor_sourcevaluation_candidate_power. ((forall bpvi_i_pvs_cofactor_sourcevaluation_candidate_power. (exists bpvi_repeat_gap_pvs_cofactor_sourcevaluation_candidate_power. bpvi_repeat_gap_pvs_cofactor_sourcevaluation_candidate_power + S bpvi_i_pvs_cofactor_sourcevaluation_candidate_power = bpd_candidate_pvs_cofactor_sourcevaluation) -> (((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_repeat. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_repeat + S (ppf_prime_cofactor_source) = S ((S (bpvi_i_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_c_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_repeat. bpvi_b_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_c_pvs_cofactor_sourcevaluation_candidate_power) + (ppf_prime_cofactor_source)))) /\ (exists bpvi_u_pvs_cofactor_sourcevaluation_candidate_power bpvi_v_pvs_cofactor_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_start. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_start. bpvi_u_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_terminal. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_terminal + S (bpvi_result_pvs_cofactor_sourcevaluation_candidate) = S ((S (bpd_candidate_pvs_cofactor_sourcevaluation)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_terminal. bpvi_u_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_cofactor_sourcevaluation)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power) + (bpvi_result_pvs_cofactor_sourcevaluation_candidate))) /\ forall bpvi_j_pvs_cofactor_sourcevaluation_candidate_power. (exists bpvi_product_gap_pvs_cofactor_sourcevaluation_candidate_power. bpvi_product_gap_pvs_cofactor_sourcevaluation_candidate_power + S bpvi_j_pvs_cofactor_sourcevaluation_candidate_power = bpd_candidate_pvs_cofactor_sourcevaluation) -> exists bpvi_factor_pvs_cofactor_sourcevaluation_candidate_power bpvi_partial_pvs_cofactor_sourcevaluation_candidate_power bpvi_successor_pvs_cofactor_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_factor. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_factor + S (bpvi_factor_pvs_cofactor_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_c_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_factor. bpvi_b_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_factor * S ((S (bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_c_pvs_cofactor_sourcevaluation_candidate_power) + (bpvi_factor_pvs_cofactor_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_partial. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_partial + S (bpvi_partial_pvs_cofactor_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_partial. bpvi_u_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_partial * S ((S (bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power) + (bpvi_partial_pvs_cofactor_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_successor. bpvi_h_pvs_cofactor_sourcevaluation_candidate_power_successor + S (bpvi_successor_pvs_cofactor_sourcevaluation_candidate_power) = S ((S (S bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_successor. bpvi_u_pvs_cofactor_sourcevaluation_candidate_power = bpvi_q_pvs_cofactor_sourcevaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_cofactor_sourcevaluation_candidate_power)) * bpvi_v_pvs_cofactor_sourcevaluation_candidate_power) + (bpvi_successor_pvs_cofactor_sourcevaluation_candidate_power))) /\ bpvi_successor_pvs_cofactor_sourcevaluation_candidate_power = bpvi_partial_pvs_cofactor_sourcevaluation_candidate_power * bpvi_factor_pvs_cofactor_sourcevaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_sourcevaluation_candidate. n = bpvi_result_pvs_cofactor_sourcevaluation_candidate * bpvi_divisor_factor_pvs_cofactor_sourcevaluation_candidate)) -> (exists bpd_gap_pvs_cofactor_sourcevaluation_maximal. bpd_gap_pvs_cofactor_sourcevaluation_maximal + (bpd_candidate_pvs_cofactor_sourcevaluation) = (ppf_exponent_cofactor_source))) -> (exists pvs_factor_cofactor_sourcedivides. (ppf_exponent_cofactor_source) = (k) * pvs_factor_cofactor_sourcedivides)) -> (forall ppf_prime_cofactor_target ppf_exponent_cofactor_target. (~((ppf_prime_cofactor_target) = 1) /\ forall pvs_left_cofactor_targetdomain pvs_right_cofactor_targetdomain. (ppf_prime_cofactor_target) = pvs_left_cofactor_targetdomain * pvs_right_cofactor_targetdomain -> pvs_left_cofactor_targetdomain = 1 \/ pvs_right_cofactor_targetdomain = 1) -> (((exists bpd_gap_pvs_cofactor_targetvaluation_selected_bound. bpd_gap_pvs_cofactor_targetvaluation_selected_bound + (ppf_exponent_cofactor_target) = (u)) /\ (exists bpvi_result_pvs_cofactor_targetvaluation_selected. ((exists bpvi_b_pvs_cofactor_targetvaluation_selected_power bpvi_c_pvs_cofactor_targetvaluation_selected_power. ((forall bpvi_i_pvs_cofactor_targetvaluation_selected_power. (exists bpvi_repeat_gap_pvs_cofactor_targetvaluation_selected_power. bpvi_repeat_gap_pvs_cofactor_targetvaluation_selected_power + S bpvi_i_pvs_cofactor_targetvaluation_selected_power = ppf_exponent_cofactor_target) -> (((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_repeat. bpvi_h_pvs_cofactor_targetvaluation_selected_power_repeat + S (ppf_prime_cofactor_target) = S ((S (bpvi_i_pvs_cofactor_targetvaluation_selected_power)) * bpvi_c_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_repeat. bpvi_b_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_cofactor_targetvaluation_selected_power)) * bpvi_c_pvs_cofactor_targetvaluation_selected_power) + (ppf_prime_cofactor_target)))) /\ (exists bpvi_u_pvs_cofactor_targetvaluation_selected_power bpvi_v_pvs_cofactor_targetvaluation_selected_power. ((((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_start. bpvi_h_pvs_cofactor_targetvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_start. bpvi_u_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_terminal. bpvi_h_pvs_cofactor_targetvaluation_selected_power_terminal + S (bpvi_result_pvs_cofactor_targetvaluation_selected) = S ((S (ppf_exponent_cofactor_target)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_terminal. bpvi_u_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_terminal * S ((S (ppf_exponent_cofactor_target)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power) + (bpvi_result_pvs_cofactor_targetvaluation_selected))) /\ forall bpvi_j_pvs_cofactor_targetvaluation_selected_power. (exists bpvi_product_gap_pvs_cofactor_targetvaluation_selected_power. bpvi_product_gap_pvs_cofactor_targetvaluation_selected_power + S bpvi_j_pvs_cofactor_targetvaluation_selected_power = ppf_exponent_cofactor_target) -> exists bpvi_factor_pvs_cofactor_targetvaluation_selected_power bpvi_partial_pvs_cofactor_targetvaluation_selected_power bpvi_successor_pvs_cofactor_targetvaluation_selected_power. ((((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_factor. bpvi_h_pvs_cofactor_targetvaluation_selected_power_factor + S (bpvi_factor_pvs_cofactor_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_c_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_factor. bpvi_b_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_factor * S ((S (bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_c_pvs_cofactor_targetvaluation_selected_power) + (bpvi_factor_pvs_cofactor_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_partial. bpvi_h_pvs_cofactor_targetvaluation_selected_power_partial + S (bpvi_partial_pvs_cofactor_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_partial. bpvi_u_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_partial * S ((S (bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power) + (bpvi_partial_pvs_cofactor_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_selected_power_successor. bpvi_h_pvs_cofactor_targetvaluation_selected_power_successor + S (bpvi_successor_pvs_cofactor_targetvaluation_selected_power) = S ((S (S bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_selected_power_successor. bpvi_u_pvs_cofactor_targetvaluation_selected_power = bpvi_q_pvs_cofactor_targetvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_cofactor_targetvaluation_selected_power)) * bpvi_v_pvs_cofactor_targetvaluation_selected_power) + (bpvi_successor_pvs_cofactor_targetvaluation_selected_power))) /\ bpvi_successor_pvs_cofactor_targetvaluation_selected_power = bpvi_partial_pvs_cofactor_targetvaluation_selected_power * bpvi_factor_pvs_cofactor_targetvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_targetvaluation_selected. u = bpvi_result_pvs_cofactor_targetvaluation_selected * bpvi_divisor_factor_pvs_cofactor_targetvaluation_selected))) /\ forall bpd_candidate_pvs_cofactor_targetvaluation. (exists bpd_gap_pvs_cofactor_targetvaluation_candidate_bound. bpd_gap_pvs_cofactor_targetvaluation_candidate_bound + (bpd_candidate_pvs_cofactor_targetvaluation) = (u)) -> (exists bpvi_result_pvs_cofactor_targetvaluation_candidate. ((exists bpvi_b_pvs_cofactor_targetvaluation_candidate_power bpvi_c_pvs_cofactor_targetvaluation_candidate_power. ((forall bpvi_i_pvs_cofactor_targetvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_cofactor_targetvaluation_candidate_power. bpvi_repeat_gap_pvs_cofactor_targetvaluation_candidate_power + S bpvi_i_pvs_cofactor_targetvaluation_candidate_power = bpd_candidate_pvs_cofactor_targetvaluation) -> (((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_repeat. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_repeat + S (ppf_prime_cofactor_target) = S ((S (bpvi_i_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_c_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_repeat. bpvi_b_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_c_pvs_cofactor_targetvaluation_candidate_power) + (ppf_prime_cofactor_target)))) /\ (exists bpvi_u_pvs_cofactor_targetvaluation_candidate_power bpvi_v_pvs_cofactor_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_start. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_start. bpvi_u_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_terminal. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_terminal + S (bpvi_result_pvs_cofactor_targetvaluation_candidate) = S ((S (bpd_candidate_pvs_cofactor_targetvaluation)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_terminal. bpvi_u_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_cofactor_targetvaluation)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power) + (bpvi_result_pvs_cofactor_targetvaluation_candidate))) /\ forall bpvi_j_pvs_cofactor_targetvaluation_candidate_power. (exists bpvi_product_gap_pvs_cofactor_targetvaluation_candidate_power. bpvi_product_gap_pvs_cofactor_targetvaluation_candidate_power + S bpvi_j_pvs_cofactor_targetvaluation_candidate_power = bpd_candidate_pvs_cofactor_targetvaluation) -> exists bpvi_factor_pvs_cofactor_targetvaluation_candidate_power bpvi_partial_pvs_cofactor_targetvaluation_candidate_power bpvi_successor_pvs_cofactor_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_factor. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_factor + S (bpvi_factor_pvs_cofactor_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_c_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_factor. bpvi_b_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_c_pvs_cofactor_targetvaluation_candidate_power) + (bpvi_factor_pvs_cofactor_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_partial. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_partial + S (bpvi_partial_pvs_cofactor_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_partial. bpvi_u_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power) + (bpvi_partial_pvs_cofactor_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_cofactor_targetvaluation_candidate_power_successor. bpvi_h_pvs_cofactor_targetvaluation_candidate_power_successor + S (bpvi_successor_pvs_cofactor_targetvaluation_candidate_power) = S ((S (S bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_cofactor_targetvaluation_candidate_power_successor. bpvi_u_pvs_cofactor_targetvaluation_candidate_power = bpvi_q_pvs_cofactor_targetvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_cofactor_targetvaluation_candidate_power)) * bpvi_v_pvs_cofactor_targetvaluation_candidate_power) + (bpvi_successor_pvs_cofactor_targetvaluation_candidate_power))) /\ bpvi_successor_pvs_cofactor_targetvaluation_candidate_power = bpvi_partial_pvs_cofactor_targetvaluation_candidate_power * bpvi_factor_pvs_cofactor_targetvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_cofactor_targetvaluation_candidate. u = bpvi_result_pvs_cofactor_targetvaluation_candidate * bpvi_divisor_factor_pvs_cofactor_targetvaluation_candidate)) -> (exists bpd_gap_pvs_cofactor_targetvaluation_maximal. bpd_gap_pvs_cofactor_targetvaluation_maximal + (bpd_candidate_pvs_cofactor_targetvaluation) = (ppf_exponent_cofactor_target))) -> (exists pvs_factor_cofactor_targetdivides. (ppf_exponent_cofactor_target) = (k) * pvs_factor_cofactor_targetdivides))